Proof of Theorem suppssfv
Step | Hyp | Ref
| Expression |
1 | | eldifsni 4320 |
. . . . . . 7
⊢ ((𝐹‘𝐴) ∈ (V ∖ {𝑍}) → (𝐹‘𝐴) ≠ 𝑍) |
2 | | suppssfv.v |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝐴 ∈ 𝑉) |
3 | | elex 3212 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V) |
4 | 2, 3 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝐴 ∈ V) |
5 | 4 | adantll 750 |
. . . . . . . . . 10
⊢ ((((𝐷 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) ∧ 𝑥 ∈ 𝐷) → 𝐴 ∈ V) |
6 | 5 | adantr 481 |
. . . . . . . . 9
⊢
(((((𝐷 ∈ V
∧ 𝑍 ∈ V) ∧
𝜑) ∧ 𝑥 ∈ 𝐷) ∧ (𝐹‘𝐴) ≠ 𝑍) → 𝐴 ∈ V) |
7 | | suppssfv.f |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐹‘𝑌) = 𝑍) |
8 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 = 𝑌 → (𝐹‘𝐴) = (𝐹‘𝑌)) |
9 | 8 | eqeq1d 2624 |
. . . . . . . . . . . . . 14
⊢ (𝐴 = 𝑌 → ((𝐹‘𝐴) = 𝑍 ↔ (𝐹‘𝑌) = 𝑍)) |
10 | 7, 9 | syl5ibrcom 237 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴 = 𝑌 → (𝐹‘𝐴) = 𝑍)) |
11 | 10 | necon3d 2815 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐹‘𝐴) ≠ 𝑍 → 𝐴 ≠ 𝑌)) |
12 | 11 | adantl 482 |
. . . . . . . . . . 11
⊢ (((𝐷 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) → ((𝐹‘𝐴) ≠ 𝑍 → 𝐴 ≠ 𝑌)) |
13 | 12 | adantr 481 |
. . . . . . . . . 10
⊢ ((((𝐷 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) ∧ 𝑥 ∈ 𝐷) → ((𝐹‘𝐴) ≠ 𝑍 → 𝐴 ≠ 𝑌)) |
14 | 13 | imp 445 |
. . . . . . . . 9
⊢
(((((𝐷 ∈ V
∧ 𝑍 ∈ V) ∧
𝜑) ∧ 𝑥 ∈ 𝐷) ∧ (𝐹‘𝐴) ≠ 𝑍) → 𝐴 ≠ 𝑌) |
15 | | eldifsn 4317 |
. . . . . . . . 9
⊢ (𝐴 ∈ (V ∖ {𝑌}) ↔ (𝐴 ∈ V ∧ 𝐴 ≠ 𝑌)) |
16 | 6, 14, 15 | sylanbrc 698 |
. . . . . . . 8
⊢
(((((𝐷 ∈ V
∧ 𝑍 ∈ V) ∧
𝜑) ∧ 𝑥 ∈ 𝐷) ∧ (𝐹‘𝐴) ≠ 𝑍) → 𝐴 ∈ (V ∖ {𝑌})) |
17 | 16 | ex 450 |
. . . . . . 7
⊢ ((((𝐷 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) ∧ 𝑥 ∈ 𝐷) → ((𝐹‘𝐴) ≠ 𝑍 → 𝐴 ∈ (V ∖ {𝑌}))) |
18 | 1, 17 | syl5 34 |
. . . . . 6
⊢ ((((𝐷 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) ∧ 𝑥 ∈ 𝐷) → ((𝐹‘𝐴) ∈ (V ∖ {𝑍}) → 𝐴 ∈ (V ∖ {𝑌}))) |
19 | 18 | ss2rabdv 3683 |
. . . . 5
⊢ (((𝐷 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) → {𝑥 ∈ 𝐷 ∣ (𝐹‘𝐴) ∈ (V ∖ {𝑍})} ⊆ {𝑥 ∈ 𝐷 ∣ 𝐴 ∈ (V ∖ {𝑌})}) |
20 | | eqid 2622 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 ↦ (𝐹‘𝐴)) = (𝑥 ∈ 𝐷 ↦ (𝐹‘𝐴)) |
21 | | simpll 790 |
. . . . . 6
⊢ (((𝐷 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) → 𝐷 ∈ V) |
22 | | simplr 792 |
. . . . . 6
⊢ (((𝐷 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) → 𝑍 ∈ V) |
23 | 20, 21, 22 | mptsuppdifd 7317 |
. . . . 5
⊢ (((𝐷 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) → ((𝑥 ∈ 𝐷 ↦ (𝐹‘𝐴)) supp 𝑍) = {𝑥 ∈ 𝐷 ∣ (𝐹‘𝐴) ∈ (V ∖ {𝑍})}) |
24 | | eqid 2622 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 ↦ 𝐴) = (𝑥 ∈ 𝐷 ↦ 𝐴) |
25 | | suppssfv.y |
. . . . . . 7
⊢ (𝜑 → 𝑌 ∈ 𝑈) |
26 | 25 | adantl 482 |
. . . . . 6
⊢ (((𝐷 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) → 𝑌 ∈ 𝑈) |
27 | 24, 21, 26 | mptsuppdifd 7317 |
. . . . 5
⊢ (((𝐷 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) → ((𝑥 ∈ 𝐷 ↦ 𝐴) supp 𝑌) = {𝑥 ∈ 𝐷 ∣ 𝐴 ∈ (V ∖ {𝑌})}) |
28 | 19, 23, 27 | 3sstr4d 3648 |
. . . 4
⊢ (((𝐷 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) → ((𝑥 ∈ 𝐷 ↦ (𝐹‘𝐴)) supp 𝑍) ⊆ ((𝑥 ∈ 𝐷 ↦ 𝐴) supp 𝑌)) |
29 | | suppssfv.a |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ 𝐷 ↦ 𝐴) supp 𝑌) ⊆ 𝐿) |
30 | 29 | adantl 482 |
. . . 4
⊢ (((𝐷 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) → ((𝑥 ∈ 𝐷 ↦ 𝐴) supp 𝑌) ⊆ 𝐿) |
31 | 28, 30 | sstrd 3613 |
. . 3
⊢ (((𝐷 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) → ((𝑥 ∈ 𝐷 ↦ (𝐹‘𝐴)) supp 𝑍) ⊆ 𝐿) |
32 | 31 | ex 450 |
. 2
⊢ ((𝐷 ∈ V ∧ 𝑍 ∈ V) → (𝜑 → ((𝑥 ∈ 𝐷 ↦ (𝐹‘𝐴)) supp 𝑍) ⊆ 𝐿)) |
33 | | mptexg 6484 |
. . . . . . 7
⊢ (𝐷 ∈ V → (𝑥 ∈ 𝐷 ↦ (𝐹‘𝐴)) ∈ V) |
34 | | fvex 6201 |
. . . . . . . . . 10
⊢ (𝐹‘𝐴) ∈ V |
35 | 34 | rgenw 2924 |
. . . . . . . . 9
⊢
∀𝑥 ∈
𝐷 (𝐹‘𝐴) ∈ V |
36 | | dmmptg 5632 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
𝐷 (𝐹‘𝐴) ∈ V → dom (𝑥 ∈ 𝐷 ↦ (𝐹‘𝐴)) = 𝐷) |
37 | 35, 36 | ax-mp 5 |
. . . . . . . 8
⊢ dom
(𝑥 ∈ 𝐷 ↦ (𝐹‘𝐴)) = 𝐷 |
38 | | dmexg 7097 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐷 ↦ (𝐹‘𝐴)) ∈ V → dom (𝑥 ∈ 𝐷 ↦ (𝐹‘𝐴)) ∈ V) |
39 | 37, 38 | syl5eqelr 2706 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐷 ↦ (𝐹‘𝐴)) ∈ V → 𝐷 ∈ V) |
40 | 33, 39 | impbii 199 |
. . . . . 6
⊢ (𝐷 ∈ V ↔ (𝑥 ∈ 𝐷 ↦ (𝐹‘𝐴)) ∈ V) |
41 | 40 | anbi1i 731 |
. . . . 5
⊢ ((𝐷 ∈ V ∧ 𝑍 ∈ V) ↔ ((𝑥 ∈ 𝐷 ↦ (𝐹‘𝐴)) ∈ V ∧ 𝑍 ∈ V)) |
42 | | supp0prc 7298 |
. . . . 5
⊢ (¬
((𝑥 ∈ 𝐷 ↦ (𝐹‘𝐴)) ∈ V ∧ 𝑍 ∈ V) → ((𝑥 ∈ 𝐷 ↦ (𝐹‘𝐴)) supp 𝑍) = ∅) |
43 | 41, 42 | sylnbi 320 |
. . . 4
⊢ (¬
(𝐷 ∈ V ∧ 𝑍 ∈ V) → ((𝑥 ∈ 𝐷 ↦ (𝐹‘𝐴)) supp 𝑍) = ∅) |
44 | | 0ss 3972 |
. . . 4
⊢ ∅
⊆ 𝐿 |
45 | 43, 44 | syl6eqss 3655 |
. . 3
⊢ (¬
(𝐷 ∈ V ∧ 𝑍 ∈ V) → ((𝑥 ∈ 𝐷 ↦ (𝐹‘𝐴)) supp 𝑍) ⊆ 𝐿) |
46 | 45 | a1d 25 |
. 2
⊢ (¬
(𝐷 ∈ V ∧ 𝑍 ∈ V) → (𝜑 → ((𝑥 ∈ 𝐷 ↦ (𝐹‘𝐴)) supp 𝑍) ⊆ 𝐿)) |
47 | 32, 46 | pm2.61i 176 |
1
⊢ (𝜑 → ((𝑥 ∈ 𝐷 ↦ (𝐹‘𝐴)) supp 𝑍) ⊆ 𝐿) |