| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | pmtrprfval 19505 | . . 3
⊢
(pmTrsp‘{1, 2}) = (𝑝 ∈ {{1, 2}} ↦ (𝑧 ∈ {1, 2} ↦ if(𝑧 = 1, 2, 1))) | 
| 2 | 1 | rneqi 5948 | . 2
⊢ ran
(pmTrsp‘{1, 2}) = ran (𝑝 ∈ {{1, 2}} ↦ (𝑧 ∈ {1, 2} ↦ if(𝑧 = 1, 2, 1))) | 
| 3 |  | eqid 2737 | . . . 4
⊢ (𝑝 ∈ {{1, 2}} ↦ (𝑧 ∈ {1, 2} ↦ if(𝑧 = 1, 2, 1))) = (𝑝 ∈ {{1, 2}} ↦ (𝑧 ∈ {1, 2} ↦ if(𝑧 = 1, 2, 1))) | 
| 4 | 3 | rnmpt 5968 | . . 3
⊢ ran
(𝑝 ∈ {{1, 2}} ↦
(𝑧 ∈ {1, 2} ↦
if(𝑧 = 1, 2, 1))) = {𝑡 ∣ ∃𝑝 ∈ {{1, 2}}𝑡 = (𝑧 ∈ {1, 2} ↦ if(𝑧 = 1, 2, 1))} | 
| 5 |  | 1ex 11257 | . . . . . . . 8
⊢ 1 ∈
V | 
| 6 |  | id 22 | . . . . . . . . . 10
⊢ (1 ∈
V → 1 ∈ V) | 
| 7 |  | 2nn 12339 | . . . . . . . . . . 11
⊢ 2 ∈
ℕ | 
| 8 | 7 | a1i 11 | . . . . . . . . . 10
⊢ (1 ∈
V → 2 ∈ ℕ) | 
| 9 |  | iftrue 4531 | . . . . . . . . . . 11
⊢ (𝑧 = 1 → if(𝑧 = 1, 2, 1) =
2) | 
| 10 | 9 | adantl 481 | . . . . . . . . . 10
⊢ ((1
∈ V ∧ 𝑧 = 1)
→ if(𝑧 = 1, 2, 1) =
2) | 
| 11 |  | 1ne2 12474 | . . . . . . . . . . . . . 14
⊢ 1 ≠
2 | 
| 12 | 11 | nesymi 2998 | . . . . . . . . . . . . 13
⊢  ¬ 2
= 1 | 
| 13 |  | eqeq1 2741 | . . . . . . . . . . . . 13
⊢ (𝑧 = 2 → (𝑧 = 1 ↔ 2 = 1)) | 
| 14 | 12, 13 | mtbiri 327 | . . . . . . . . . . . 12
⊢ (𝑧 = 2 → ¬ 𝑧 = 1) | 
| 15 | 14 | iffalsed 4536 | . . . . . . . . . . 11
⊢ (𝑧 = 2 → if(𝑧 = 1, 2, 1) =
1) | 
| 16 | 15 | adantl 481 | . . . . . . . . . 10
⊢ ((1
∈ V ∧ 𝑧 = 2)
→ if(𝑧 = 1, 2, 1) =
1) | 
| 17 | 6, 8, 8, 6, 10, 16 | fmptpr 7192 | . . . . . . . . 9
⊢ (1 ∈
V → {〈1, 2〉, 〈2, 1〉} = (𝑧 ∈ {1, 2} ↦ if(𝑧 = 1, 2, 1))) | 
| 18 | 17 | eqeq2d 2748 | . . . . . . . 8
⊢ (1 ∈
V → (𝑡 = {〈1,
2〉, 〈2, 1〉} ↔ 𝑡 = (𝑧 ∈ {1, 2} ↦ if(𝑧 = 1, 2, 1)))) | 
| 19 | 5, 18 | ax-mp 5 | . . . . . . 7
⊢ (𝑡 = {〈1, 2〉, 〈2,
1〉} ↔ 𝑡 = (𝑧 ∈ {1, 2} ↦ if(𝑧 = 1, 2, 1))) | 
| 20 | 19 | bicomi 224 | . . . . . 6
⊢ (𝑡 = (𝑧 ∈ {1, 2} ↦ if(𝑧 = 1, 2, 1)) ↔ 𝑡 = {〈1, 2〉, 〈2,
1〉}) | 
| 21 | 20 | rexbii 3094 | . . . . 5
⊢
(∃𝑝 ∈
{{1, 2}}𝑡 = (𝑧 ∈ {1, 2} ↦ if(𝑧 = 1, 2, 1)) ↔ ∃𝑝 ∈ {{1, 2}}𝑡 = {〈1, 2〉, 〈2,
1〉}) | 
| 22 | 21 | abbii 2809 | . . . 4
⊢ {𝑡 ∣ ∃𝑝 ∈ {{1, 2}}𝑡 = (𝑧 ∈ {1, 2} ↦ if(𝑧 = 1, 2, 1))} = {𝑡 ∣ ∃𝑝 ∈ {{1, 2}}𝑡 = {〈1, 2〉, 〈2,
1〉}} | 
| 23 |  | prex 5437 | . . . . . . . 8
⊢ {1, 2}
∈ V | 
| 24 | 23 | snnz 4776 | . . . . . . 7
⊢ {{1, 2}}
≠ ∅ | 
| 25 |  | r19.9rzv 4500 | . . . . . . . 8
⊢ ({{1, 2}}
≠ ∅ → (𝑠 =
{〈1, 2〉, 〈2, 1〉} ↔ ∃𝑝 ∈ {{1, 2}}𝑠 = {〈1, 2〉, 〈2,
1〉})) | 
| 26 | 25 | bicomd 223 | . . . . . . 7
⊢ ({{1, 2}}
≠ ∅ → (∃𝑝 ∈ {{1, 2}}𝑠 = {〈1, 2〉, 〈2, 1〉}
↔ 𝑠 = {〈1,
2〉, 〈2, 1〉})) | 
| 27 | 24, 26 | ax-mp 5 | . . . . . 6
⊢
(∃𝑝 ∈
{{1, 2}}𝑠 = {〈1,
2〉, 〈2, 1〉} ↔ 𝑠 = {〈1, 2〉, 〈2,
1〉}) | 
| 28 |  | vex 3484 | . . . . . . 7
⊢ 𝑠 ∈ V | 
| 29 |  | eqeq1 2741 | . . . . . . . 8
⊢ (𝑡 = 𝑠 → (𝑡 = {〈1, 2〉, 〈2, 1〉}
↔ 𝑠 = {〈1,
2〉, 〈2, 1〉})) | 
| 30 | 29 | rexbidv 3179 | . . . . . . 7
⊢ (𝑡 = 𝑠 → (∃𝑝 ∈ {{1, 2}}𝑡 = {〈1, 2〉, 〈2, 1〉}
↔ ∃𝑝 ∈ {{1,
2}}𝑠 = {〈1, 2〉,
〈2, 1〉})) | 
| 31 | 28, 30 | elab 3679 | . . . . . 6
⊢ (𝑠 ∈ {𝑡 ∣ ∃𝑝 ∈ {{1, 2}}𝑡 = {〈1, 2〉, 〈2, 1〉}}
↔ ∃𝑝 ∈ {{1,
2}}𝑠 = {〈1, 2〉,
〈2, 1〉}) | 
| 32 |  | velsn 4642 | . . . . . 6
⊢ (𝑠 ∈ {{〈1, 2〉,
〈2, 1〉}} ↔ 𝑠
= {〈1, 2〉, 〈2, 1〉}) | 
| 33 | 27, 31, 32 | 3bitr4i 303 | . . . . 5
⊢ (𝑠 ∈ {𝑡 ∣ ∃𝑝 ∈ {{1, 2}}𝑡 = {〈1, 2〉, 〈2, 1〉}}
↔ 𝑠 ∈ {{〈1,
2〉, 〈2, 1〉}}) | 
| 34 | 33 | eqriv 2734 | . . . 4
⊢ {𝑡 ∣ ∃𝑝 ∈ {{1, 2}}𝑡 = {〈1, 2〉, 〈2,
1〉}} = {{〈1, 2〉, 〈2, 1〉}} | 
| 35 | 22, 34 | eqtri 2765 | . . 3
⊢ {𝑡 ∣ ∃𝑝 ∈ {{1, 2}}𝑡 = (𝑧 ∈ {1, 2} ↦ if(𝑧 = 1, 2, 1))} = {{〈1, 2〉, 〈2,
1〉}} | 
| 36 | 4, 35 | eqtri 2765 | . 2
⊢ ran
(𝑝 ∈ {{1, 2}} ↦
(𝑧 ∈ {1, 2} ↦
if(𝑧 = 1, 2, 1))) =
{{〈1, 2〉, 〈2, 1〉}} | 
| 37 | 2, 36 | eqtri 2765 | 1
⊢ ran
(pmTrsp‘{1, 2}) = {{〈1, 2〉, 〈2, 1〉}} |