Proof of Theorem suppssfv
Step | Hyp | Ref
| Expression |
1 | | eldifsni 4725 |
. . . . . . 7
⊢ ((𝐹‘𝐴) ∈ (V ∖ {𝑍}) → (𝐹‘𝐴) ≠ 𝑍) |
2 | | suppssfv.v |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝐴 ∈ 𝑉) |
3 | 2 | elexd 3451 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝐴 ∈ V) |
4 | 3 | ad4ant23 750 |
. . . . . . . . 9
⊢
(((((𝐷 ∈ V
∧ 𝑍 ∈ V) ∧
𝜑) ∧ 𝑥 ∈ 𝐷) ∧ (𝐹‘𝐴) ≠ 𝑍) → 𝐴 ∈ V) |
5 | | suppssfv.f |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐹‘𝑌) = 𝑍) |
6 | | fveqeq2 6785 |
. . . . . . . . . . . . 13
⊢ (𝐴 = 𝑌 → ((𝐹‘𝐴) = 𝑍 ↔ (𝐹‘𝑌) = 𝑍)) |
7 | 5, 6 | syl5ibrcom 246 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 = 𝑌 → (𝐹‘𝐴) = 𝑍)) |
8 | 7 | necon3d 2964 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐹‘𝐴) ≠ 𝑍 → 𝐴 ≠ 𝑌)) |
9 | 8 | ad2antlr 724 |
. . . . . . . . . 10
⊢ ((((𝐷 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) ∧ 𝑥 ∈ 𝐷) → ((𝐹‘𝐴) ≠ 𝑍 → 𝐴 ≠ 𝑌)) |
10 | 9 | imp 407 |
. . . . . . . . 9
⊢
(((((𝐷 ∈ V
∧ 𝑍 ∈ V) ∧
𝜑) ∧ 𝑥 ∈ 𝐷) ∧ (𝐹‘𝐴) ≠ 𝑍) → 𝐴 ≠ 𝑌) |
11 | | eldifsn 4722 |
. . . . . . . . 9
⊢ (𝐴 ∈ (V ∖ {𝑌}) ↔ (𝐴 ∈ V ∧ 𝐴 ≠ 𝑌)) |
12 | 4, 10, 11 | sylanbrc 583 |
. . . . . . . 8
⊢
(((((𝐷 ∈ V
∧ 𝑍 ∈ V) ∧
𝜑) ∧ 𝑥 ∈ 𝐷) ∧ (𝐹‘𝐴) ≠ 𝑍) → 𝐴 ∈ (V ∖ {𝑌})) |
13 | 12 | ex 413 |
. . . . . . 7
⊢ ((((𝐷 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) ∧ 𝑥 ∈ 𝐷) → ((𝐹‘𝐴) ≠ 𝑍 → 𝐴 ∈ (V ∖ {𝑌}))) |
14 | 1, 13 | syl5 34 |
. . . . . 6
⊢ ((((𝐷 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) ∧ 𝑥 ∈ 𝐷) → ((𝐹‘𝐴) ∈ (V ∖ {𝑍}) → 𝐴 ∈ (V ∖ {𝑌}))) |
15 | 14 | ss2rabdv 4010 |
. . . . 5
⊢ (((𝐷 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) → {𝑥 ∈ 𝐷 ∣ (𝐹‘𝐴) ∈ (V ∖ {𝑍})} ⊆ {𝑥 ∈ 𝐷 ∣ 𝐴 ∈ (V ∖ {𝑌})}) |
16 | | eqid 2738 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 ↦ (𝐹‘𝐴)) = (𝑥 ∈ 𝐷 ↦ (𝐹‘𝐴)) |
17 | | simpll 764 |
. . . . . 6
⊢ (((𝐷 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) → 𝐷 ∈ V) |
18 | | simplr 766 |
. . . . . 6
⊢ (((𝐷 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) → 𝑍 ∈ V) |
19 | 16, 17, 18 | mptsuppdifd 8000 |
. . . . 5
⊢ (((𝐷 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) → ((𝑥 ∈ 𝐷 ↦ (𝐹‘𝐴)) supp 𝑍) = {𝑥 ∈ 𝐷 ∣ (𝐹‘𝐴) ∈ (V ∖ {𝑍})}) |
20 | | eqid 2738 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 ↦ 𝐴) = (𝑥 ∈ 𝐷 ↦ 𝐴) |
21 | | suppssfv.y |
. . . . . . 7
⊢ (𝜑 → 𝑌 ∈ 𝑈) |
22 | 21 | adantl 482 |
. . . . . 6
⊢ (((𝐷 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) → 𝑌 ∈ 𝑈) |
23 | 20, 17, 22 | mptsuppdifd 8000 |
. . . . 5
⊢ (((𝐷 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) → ((𝑥 ∈ 𝐷 ↦ 𝐴) supp 𝑌) = {𝑥 ∈ 𝐷 ∣ 𝐴 ∈ (V ∖ {𝑌})}) |
24 | 15, 19, 23 | 3sstr4d 3969 |
. . . 4
⊢ (((𝐷 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) → ((𝑥 ∈ 𝐷 ↦ (𝐹‘𝐴)) supp 𝑍) ⊆ ((𝑥 ∈ 𝐷 ↦ 𝐴) supp 𝑌)) |
25 | | suppssfv.a |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ 𝐷 ↦ 𝐴) supp 𝑌) ⊆ 𝐿) |
26 | 25 | adantl 482 |
. . . 4
⊢ (((𝐷 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) → ((𝑥 ∈ 𝐷 ↦ 𝐴) supp 𝑌) ⊆ 𝐿) |
27 | 24, 26 | sstrd 3932 |
. . 3
⊢ (((𝐷 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) → ((𝑥 ∈ 𝐷 ↦ (𝐹‘𝐴)) supp 𝑍) ⊆ 𝐿) |
28 | 27 | ex 413 |
. 2
⊢ ((𝐷 ∈ V ∧ 𝑍 ∈ V) → (𝜑 → ((𝑥 ∈ 𝐷 ↦ (𝐹‘𝐴)) supp 𝑍) ⊆ 𝐿)) |
29 | | mptexg 7099 |
. . . . . . 7
⊢ (𝐷 ∈ V → (𝑥 ∈ 𝐷 ↦ (𝐹‘𝐴)) ∈ V) |
30 | | fvex 6789 |
. . . . . . . . . 10
⊢ (𝐹‘𝐴) ∈ V |
31 | 30 | rgenw 3076 |
. . . . . . . . 9
⊢
∀𝑥 ∈
𝐷 (𝐹‘𝐴) ∈ V |
32 | | dmmptg 6147 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
𝐷 (𝐹‘𝐴) ∈ V → dom (𝑥 ∈ 𝐷 ↦ (𝐹‘𝐴)) = 𝐷) |
33 | 31, 32 | ax-mp 5 |
. . . . . . . 8
⊢ dom
(𝑥 ∈ 𝐷 ↦ (𝐹‘𝐴)) = 𝐷 |
34 | | dmexg 7750 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐷 ↦ (𝐹‘𝐴)) ∈ V → dom (𝑥 ∈ 𝐷 ↦ (𝐹‘𝐴)) ∈ V) |
35 | 33, 34 | eqeltrrid 2844 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐷 ↦ (𝐹‘𝐴)) ∈ V → 𝐷 ∈ V) |
36 | 29, 35 | impbii 208 |
. . . . . 6
⊢ (𝐷 ∈ V ↔ (𝑥 ∈ 𝐷 ↦ (𝐹‘𝐴)) ∈ V) |
37 | 36 | anbi1i 624 |
. . . . 5
⊢ ((𝐷 ∈ V ∧ 𝑍 ∈ V) ↔ ((𝑥 ∈ 𝐷 ↦ (𝐹‘𝐴)) ∈ V ∧ 𝑍 ∈ V)) |
38 | | supp0prc 7978 |
. . . . 5
⊢ (¬
((𝑥 ∈ 𝐷 ↦ (𝐹‘𝐴)) ∈ V ∧ 𝑍 ∈ V) → ((𝑥 ∈ 𝐷 ↦ (𝐹‘𝐴)) supp 𝑍) = ∅) |
39 | 37, 38 | sylnbi 330 |
. . . 4
⊢ (¬
(𝐷 ∈ V ∧ 𝑍 ∈ V) → ((𝑥 ∈ 𝐷 ↦ (𝐹‘𝐴)) supp 𝑍) = ∅) |
40 | | 0ss 4332 |
. . . 4
⊢ ∅
⊆ 𝐿 |
41 | 39, 40 | eqsstrdi 3976 |
. . 3
⊢ (¬
(𝐷 ∈ V ∧ 𝑍 ∈ V) → ((𝑥 ∈ 𝐷 ↦ (𝐹‘𝐴)) supp 𝑍) ⊆ 𝐿) |
42 | 41 | a1d 25 |
. 2
⊢ (¬
(𝐷 ∈ V ∧ 𝑍 ∈ V) → (𝜑 → ((𝑥 ∈ 𝐷 ↦ (𝐹‘𝐴)) supp 𝑍) ⊆ 𝐿)) |
43 | 28, 42 | pm2.61i 182 |
1
⊢ (𝜑 → ((𝑥 ∈ 𝐷 ↦ (𝐹‘𝐴)) supp 𝑍) ⊆ 𝐿) |