Proof of Theorem extmptsuppeq
Step | Hyp | Ref
| Expression |
1 | | extmptsuppeq.a |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ⊆ 𝐵) |
2 | 1 | adantl 485 |
. . . . . . . 8
⊢ ((𝑍 ∈ V ∧ 𝜑) → 𝐴 ⊆ 𝐵) |
3 | 2 | sseld 3916 |
. . . . . . 7
⊢ ((𝑍 ∈ V ∧ 𝜑) → (𝑛 ∈ 𝐴 → 𝑛 ∈ 𝐵)) |
4 | 3 | anim1d 614 |
. . . . . 6
⊢ ((𝑍 ∈ V ∧ 𝜑) → ((𝑛 ∈ 𝐴 ∧ 𝑋 ∈ (V ∖ {𝑍})) → (𝑛 ∈ 𝐵 ∧ 𝑋 ∈ (V ∖ {𝑍})))) |
5 | | eldif 3893 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ (𝐵 ∖ 𝐴) ↔ (𝑛 ∈ 𝐵 ∧ ¬ 𝑛 ∈ 𝐴)) |
6 | | extmptsuppeq.z |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (𝐵 ∖ 𝐴)) → 𝑋 = 𝑍) |
7 | 6 | adantll 714 |
. . . . . . . . . . . . 13
⊢ (((𝑍 ∈ V ∧ 𝜑) ∧ 𝑛 ∈ (𝐵 ∖ 𝐴)) → 𝑋 = 𝑍) |
8 | 5, 7 | sylan2br 598 |
. . . . . . . . . . . 12
⊢ (((𝑍 ∈ V ∧ 𝜑) ∧ (𝑛 ∈ 𝐵 ∧ ¬ 𝑛 ∈ 𝐴)) → 𝑋 = 𝑍) |
9 | 8 | expr 460 |
. . . . . . . . . . 11
⊢ (((𝑍 ∈ V ∧ 𝜑) ∧ 𝑛 ∈ 𝐵) → (¬ 𝑛 ∈ 𝐴 → 𝑋 = 𝑍)) |
10 | | elsn2g 4595 |
. . . . . . . . . . . . 13
⊢ (𝑍 ∈ V → (𝑋 ∈ {𝑍} ↔ 𝑋 = 𝑍)) |
11 | | elndif 4059 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈ {𝑍} → ¬ 𝑋 ∈ (V ∖ {𝑍})) |
12 | 10, 11 | syl6bir 257 |
. . . . . . . . . . . 12
⊢ (𝑍 ∈ V → (𝑋 = 𝑍 → ¬ 𝑋 ∈ (V ∖ {𝑍}))) |
13 | 12 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝑍 ∈ V ∧ 𝜑) ∧ 𝑛 ∈ 𝐵) → (𝑋 = 𝑍 → ¬ 𝑋 ∈ (V ∖ {𝑍}))) |
14 | 9, 13 | syld 47 |
. . . . . . . . . 10
⊢ (((𝑍 ∈ V ∧ 𝜑) ∧ 𝑛 ∈ 𝐵) → (¬ 𝑛 ∈ 𝐴 → ¬ 𝑋 ∈ (V ∖ {𝑍}))) |
15 | 14 | con4d 115 |
. . . . . . . . 9
⊢ (((𝑍 ∈ V ∧ 𝜑) ∧ 𝑛 ∈ 𝐵) → (𝑋 ∈ (V ∖ {𝑍}) → 𝑛 ∈ 𝐴)) |
16 | 15 | impr 458 |
. . . . . . . 8
⊢ (((𝑍 ∈ V ∧ 𝜑) ∧ (𝑛 ∈ 𝐵 ∧ 𝑋 ∈ (V ∖ {𝑍}))) → 𝑛 ∈ 𝐴) |
17 | | simprr 773 |
. . . . . . . 8
⊢ (((𝑍 ∈ V ∧ 𝜑) ∧ (𝑛 ∈ 𝐵 ∧ 𝑋 ∈ (V ∖ {𝑍}))) → 𝑋 ∈ (V ∖ {𝑍})) |
18 | 16, 17 | jca 515 |
. . . . . . 7
⊢ (((𝑍 ∈ V ∧ 𝜑) ∧ (𝑛 ∈ 𝐵 ∧ 𝑋 ∈ (V ∖ {𝑍}))) → (𝑛 ∈ 𝐴 ∧ 𝑋 ∈ (V ∖ {𝑍}))) |
19 | 18 | ex 416 |
. . . . . 6
⊢ ((𝑍 ∈ V ∧ 𝜑) → ((𝑛 ∈ 𝐵 ∧ 𝑋 ∈ (V ∖ {𝑍})) → (𝑛 ∈ 𝐴 ∧ 𝑋 ∈ (V ∖ {𝑍})))) |
20 | 4, 19 | impbid 215 |
. . . . 5
⊢ ((𝑍 ∈ V ∧ 𝜑) → ((𝑛 ∈ 𝐴 ∧ 𝑋 ∈ (V ∖ {𝑍})) ↔ (𝑛 ∈ 𝐵 ∧ 𝑋 ∈ (V ∖ {𝑍})))) |
21 | 20 | rabbidva2 3401 |
. . . 4
⊢ ((𝑍 ∈ V ∧ 𝜑) → {𝑛 ∈ 𝐴 ∣ 𝑋 ∈ (V ∖ {𝑍})} = {𝑛 ∈ 𝐵 ∣ 𝑋 ∈ (V ∖ {𝑍})}) |
22 | | eqid 2739 |
. . . . 5
⊢ (𝑛 ∈ 𝐴 ↦ 𝑋) = (𝑛 ∈ 𝐴 ↦ 𝑋) |
23 | | extmptsuppeq.b |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ 𝑊) |
24 | 23, 1 | ssexd 5233 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ V) |
25 | 24 | adantl 485 |
. . . . 5
⊢ ((𝑍 ∈ V ∧ 𝜑) → 𝐴 ∈ V) |
26 | | simpl 486 |
. . . . 5
⊢ ((𝑍 ∈ V ∧ 𝜑) → 𝑍 ∈ V) |
27 | 22, 25, 26 | mptsuppdifd 7951 |
. . . 4
⊢ ((𝑍 ∈ V ∧ 𝜑) → ((𝑛 ∈ 𝐴 ↦ 𝑋) supp 𝑍) = {𝑛 ∈ 𝐴 ∣ 𝑋 ∈ (V ∖ {𝑍})}) |
28 | | eqid 2739 |
. . . . 5
⊢ (𝑛 ∈ 𝐵 ↦ 𝑋) = (𝑛 ∈ 𝐵 ↦ 𝑋) |
29 | 23 | adantl 485 |
. . . . 5
⊢ ((𝑍 ∈ V ∧ 𝜑) → 𝐵 ∈ 𝑊) |
30 | 28, 29, 26 | mptsuppdifd 7951 |
. . . 4
⊢ ((𝑍 ∈ V ∧ 𝜑) → ((𝑛 ∈ 𝐵 ↦ 𝑋) supp 𝑍) = {𝑛 ∈ 𝐵 ∣ 𝑋 ∈ (V ∖ {𝑍})}) |
31 | 21, 27, 30 | 3eqtr4d 2789 |
. . 3
⊢ ((𝑍 ∈ V ∧ 𝜑) → ((𝑛 ∈ 𝐴 ↦ 𝑋) supp 𝑍) = ((𝑛 ∈ 𝐵 ↦ 𝑋) supp 𝑍)) |
32 | 31 | ex 416 |
. 2
⊢ (𝑍 ∈ V → (𝜑 → ((𝑛 ∈ 𝐴 ↦ 𝑋) supp 𝑍) = ((𝑛 ∈ 𝐵 ↦ 𝑋) supp 𝑍))) |
33 | | simpr 488 |
. . . . 5
⊢ (((𝑛 ∈ 𝐴 ↦ 𝑋) ∈ V ∧ 𝑍 ∈ V) → 𝑍 ∈ V) |
34 | | supp0prc 7929 |
. . . . 5
⊢ (¬
((𝑛 ∈ 𝐴 ↦ 𝑋) ∈ V ∧ 𝑍 ∈ V) → ((𝑛 ∈ 𝐴 ↦ 𝑋) supp 𝑍) = ∅) |
35 | 33, 34 | nsyl5 162 |
. . . 4
⊢ (¬
𝑍 ∈ V → ((𝑛 ∈ 𝐴 ↦ 𝑋) supp 𝑍) = ∅) |
36 | | simpr 488 |
. . . . 5
⊢ (((𝑛 ∈ 𝐵 ↦ 𝑋) ∈ V ∧ 𝑍 ∈ V) → 𝑍 ∈ V) |
37 | | supp0prc 7929 |
. . . . 5
⊢ (¬
((𝑛 ∈ 𝐵 ↦ 𝑋) ∈ V ∧ 𝑍 ∈ V) → ((𝑛 ∈ 𝐵 ↦ 𝑋) supp 𝑍) = ∅) |
38 | 36, 37 | nsyl5 162 |
. . . 4
⊢ (¬
𝑍 ∈ V → ((𝑛 ∈ 𝐵 ↦ 𝑋) supp 𝑍) = ∅) |
39 | 35, 38 | eqtr4d 2782 |
. . 3
⊢ (¬
𝑍 ∈ V → ((𝑛 ∈ 𝐴 ↦ 𝑋) supp 𝑍) = ((𝑛 ∈ 𝐵 ↦ 𝑋) supp 𝑍)) |
40 | 39 | a1d 25 |
. 2
⊢ (¬
𝑍 ∈ V → (𝜑 → ((𝑛 ∈ 𝐴 ↦ 𝑋) supp 𝑍) = ((𝑛 ∈ 𝐵 ↦ 𝑋) supp 𝑍))) |
41 | 32, 40 | pm2.61i 185 |
1
⊢ (𝜑 → ((𝑛 ∈ 𝐴 ↦ 𝑋) supp 𝑍) = ((𝑛 ∈ 𝐵 ↦ 𝑋) supp 𝑍)) |