Step | Hyp | Ref
| Expression |
1 | | prex 4836 |
. . 3
⊢ {1, 2}
∈ V |
2 | | eqid 2610 |
. . . 4
⊢
(pmTrsp‘{1, 2}) = (pmTrsp‘{1, 2}) |
3 | 2 | pmtrfval 17693 |
. . 3
⊢ ({1, 2}
∈ V → (pmTrsp‘{1, 2}) = (𝑝 ∈ {𝑡 ∈ 𝒫 {1, 2} ∣ 𝑡 ≈ 2𝑜}
↦ (𝑧 ∈ {1, 2}
↦ if(𝑧 ∈ 𝑝, ∪
(𝑝 ∖ {𝑧}), 𝑧)))) |
4 | 1, 3 | ax-mp 5 |
. 2
⊢
(pmTrsp‘{1, 2}) = (𝑝 ∈ {𝑡 ∈ 𝒫 {1, 2} ∣ 𝑡 ≈ 2𝑜}
↦ (𝑧 ∈ {1, 2}
↦ if(𝑧 ∈ 𝑝, ∪
(𝑝 ∖ {𝑧}), 𝑧))) |
5 | | 1ex 9914 |
. . . . 5
⊢ 1 ∈
V |
6 | | 2nn0 11186 |
. . . . 5
⊢ 2 ∈
ℕ0 |
7 | | 1ne2 11117 |
. . . . 5
⊢ 1 ≠
2 |
8 | | pr2pwpr 13116 |
. . . . 5
⊢ ((1
∈ V ∧ 2 ∈ ℕ0 ∧ 1 ≠ 2) → {𝑡 ∈ 𝒫 {1, 2} ∣
𝑡 ≈
2𝑜} = {{1, 2}}) |
9 | 5, 6, 7, 8 | mp3an 1416 |
. . . 4
⊢ {𝑡 ∈ 𝒫 {1, 2} ∣
𝑡 ≈
2𝑜} = {{1, 2}} |
10 | | eqid 2610 |
. . . 4
⊢ (𝑧 ∈ {1, 2} ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧)) = (𝑧 ∈ {1, 2} ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧)) |
11 | 9, 10 | mpteq12i 4670 |
. . 3
⊢ (𝑝 ∈ {𝑡 ∈ 𝒫 {1, 2} ∣ 𝑡 ≈ 2𝑜}
↦ (𝑧 ∈ {1, 2}
↦ if(𝑧 ∈ 𝑝, ∪
(𝑝 ∖ {𝑧}), 𝑧))) = (𝑝 ∈ {{1, 2}} ↦ (𝑧 ∈ {1, 2} ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))) |
12 | | elsni 4142 |
. . . . . 6
⊢ (𝑝 ∈ {{1, 2}} → 𝑝 = {1, 2}) |
13 | | eleq2 2677 |
. . . . . . . . 9
⊢ (𝑝 = {1, 2} → (𝑧 ∈ 𝑝 ↔ 𝑧 ∈ {1, 2})) |
14 | 13 | biimpar 501 |
. . . . . . . 8
⊢ ((𝑝 = {1, 2} ∧ 𝑧 ∈ {1, 2}) → 𝑧 ∈ 𝑝) |
15 | 14 | iftrued 4044 |
. . . . . . 7
⊢ ((𝑝 = {1, 2} ∧ 𝑧 ∈ {1, 2}) → if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧) = ∪ (𝑝 ∖ {𝑧})) |
16 | | elpri 4145 |
. . . . . . . . 9
⊢ (𝑧 ∈ {1, 2} → (𝑧 = 1 ∨ 𝑧 = 2)) |
17 | | 2ex 10969 |
. . . . . . . . . . . . 13
⊢ 2 ∈
V |
18 | 17 | unisn 4387 |
. . . . . . . . . . . 12
⊢ ∪ {2} = 2 |
19 | | simpr 476 |
. . . . . . . . . . . . . . 15
⊢ ((𝑧 = 1 ∧ 𝑝 = {1, 2}) → 𝑝 = {1, 2}) |
20 | | sneq 4135 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 1 → {𝑧} = {1}) |
21 | 20 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝑧 = 1 ∧ 𝑝 = {1, 2}) → {𝑧} = {1}) |
22 | 19, 21 | difeq12d 3691 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 = 1 ∧ 𝑝 = {1, 2}) → (𝑝 ∖ {𝑧}) = ({1, 2} ∖ {1})) |
23 | | difprsn1 4271 |
. . . . . . . . . . . . . . 15
⊢ (1 ≠ 2
→ ({1, 2} ∖ {1}) = {2}) |
24 | 7, 23 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ ({1, 2}
∖ {1}) = {2} |
25 | 22, 24 | syl6eq 2660 |
. . . . . . . . . . . . 13
⊢ ((𝑧 = 1 ∧ 𝑝 = {1, 2}) → (𝑝 ∖ {𝑧}) = {2}) |
26 | 25 | unieqd 4382 |
. . . . . . . . . . . 12
⊢ ((𝑧 = 1 ∧ 𝑝 = {1, 2}) → ∪ (𝑝
∖ {𝑧}) = ∪ {2}) |
27 | | iftrue 4042 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 1 → if(𝑧 = 1, 2, 1) =
2) |
28 | 27 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑧 = 1 ∧ 𝑝 = {1, 2}) → if(𝑧 = 1, 2, 1) = 2) |
29 | 18, 26, 28 | 3eqtr4a 2670 |
. . . . . . . . . . 11
⊢ ((𝑧 = 1 ∧ 𝑝 = {1, 2}) → ∪ (𝑝
∖ {𝑧}) = if(𝑧 = 1, 2, 1)) |
30 | 29 | ex 449 |
. . . . . . . . . 10
⊢ (𝑧 = 1 → (𝑝 = {1, 2} → ∪
(𝑝 ∖ {𝑧}) = if(𝑧 = 1, 2, 1))) |
31 | 5 | unisn 4387 |
. . . . . . . . . . . 12
⊢ ∪ {1} = 1 |
32 | | simpr 476 |
. . . . . . . . . . . . . . 15
⊢ ((𝑧 = 2 ∧ 𝑝 = {1, 2}) → 𝑝 = {1, 2}) |
33 | | sneq 4135 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 2 → {𝑧} = {2}) |
34 | 33 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝑧 = 2 ∧ 𝑝 = {1, 2}) → {𝑧} = {2}) |
35 | 32, 34 | difeq12d 3691 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 = 2 ∧ 𝑝 = {1, 2}) → (𝑝 ∖ {𝑧}) = ({1, 2} ∖ {2})) |
36 | | difprsn2 4272 |
. . . . . . . . . . . . . . 15
⊢ (1 ≠ 2
→ ({1, 2} ∖ {2}) = {1}) |
37 | 7, 36 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ ({1, 2}
∖ {2}) = {1} |
38 | 35, 37 | syl6eq 2660 |
. . . . . . . . . . . . 13
⊢ ((𝑧 = 2 ∧ 𝑝 = {1, 2}) → (𝑝 ∖ {𝑧}) = {1}) |
39 | 38 | unieqd 4382 |
. . . . . . . . . . . 12
⊢ ((𝑧 = 2 ∧ 𝑝 = {1, 2}) → ∪ (𝑝
∖ {𝑧}) = ∪ {1}) |
40 | 7 | nesymi 2839 |
. . . . . . . . . . . . . . 15
⊢ ¬ 2
= 1 |
41 | | eqeq1 2614 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 2 → (𝑧 = 1 ↔ 2 = 1)) |
42 | 40, 41 | mtbiri 316 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 2 → ¬ 𝑧 = 1) |
43 | 42 | iffalsed 4047 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 2 → if(𝑧 = 1, 2, 1) =
1) |
44 | 43 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑧 = 2 ∧ 𝑝 = {1, 2}) → if(𝑧 = 1, 2, 1) = 1) |
45 | 31, 39, 44 | 3eqtr4a 2670 |
. . . . . . . . . . 11
⊢ ((𝑧 = 2 ∧ 𝑝 = {1, 2}) → ∪ (𝑝
∖ {𝑧}) = if(𝑧 = 1, 2, 1)) |
46 | 45 | ex 449 |
. . . . . . . . . 10
⊢ (𝑧 = 2 → (𝑝 = {1, 2} → ∪
(𝑝 ∖ {𝑧}) = if(𝑧 = 1, 2, 1))) |
47 | 30, 46 | jaoi 393 |
. . . . . . . . 9
⊢ ((𝑧 = 1 ∨ 𝑧 = 2) → (𝑝 = {1, 2} → ∪
(𝑝 ∖ {𝑧}) = if(𝑧 = 1, 2, 1))) |
48 | 16, 47 | syl 17 |
. . . . . . . 8
⊢ (𝑧 ∈ {1, 2} → (𝑝 = {1, 2} → ∪ (𝑝
∖ {𝑧}) = if(𝑧 = 1, 2, 1))) |
49 | 48 | impcom 445 |
. . . . . . 7
⊢ ((𝑝 = {1, 2} ∧ 𝑧 ∈ {1, 2}) → ∪ (𝑝
∖ {𝑧}) = if(𝑧 = 1, 2, 1)) |
50 | 15, 49 | eqtrd 2644 |
. . . . . 6
⊢ ((𝑝 = {1, 2} ∧ 𝑧 ∈ {1, 2}) → if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧) = if(𝑧 = 1, 2, 1)) |
51 | 12, 50 | sylan 487 |
. . . . 5
⊢ ((𝑝 ∈ {{1, 2}} ∧ 𝑧 ∈ {1, 2}) → if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧) = if(𝑧 = 1, 2, 1)) |
52 | 51 | mpteq2dva 4672 |
. . . 4
⊢ (𝑝 ∈ {{1, 2}} → (𝑧 ∈ {1, 2} ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧)) = (𝑧 ∈ {1, 2} ↦ if(𝑧 = 1, 2, 1))) |
53 | 52 | mpteq2ia 4668 |
. . 3
⊢ (𝑝 ∈ {{1, 2}} ↦ (𝑧 ∈ {1, 2} ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))) = (𝑝 ∈ {{1, 2}} ↦ (𝑧 ∈ {1, 2} ↦ if(𝑧 = 1, 2, 1))) |
54 | 11, 53 | eqtri 2632 |
. 2
⊢ (𝑝 ∈ {𝑡 ∈ 𝒫 {1, 2} ∣ 𝑡 ≈ 2𝑜}
↦ (𝑧 ∈ {1, 2}
↦ if(𝑧 ∈ 𝑝, ∪
(𝑝 ∖ {𝑧}), 𝑧))) = (𝑝 ∈ {{1, 2}} ↦ (𝑧 ∈ {1, 2} ↦ if(𝑧 = 1, 2, 1))) |
55 | 4, 54 | eqtri 2632 |
1
⊢
(pmTrsp‘{1, 2}) = (𝑝 ∈ {{1, 2}} ↦ (𝑧 ∈ {1, 2} ↦ if(𝑧 = 1, 2, 1))) |