Step | Hyp | Ref
| Expression |
1 | | pmtrprfval 19354 |
. . 3
⊢
(pmTrsp‘{1, 2}) = (𝑝 ∈ {{1, 2}} ↦ (𝑧 ∈ {1, 2} ↦ if(𝑧 = 1, 2, 1))) |
2 | 1 | rneqi 5936 |
. 2
⊢ ran
(pmTrsp‘{1, 2}) = ran (𝑝 ∈ {{1, 2}} ↦ (𝑧 ∈ {1, 2} ↦ if(𝑧 = 1, 2, 1))) |
3 | | eqid 2732 |
. . . 4
⊢ (𝑝 ∈ {{1, 2}} ↦ (𝑧 ∈ {1, 2} ↦ if(𝑧 = 1, 2, 1))) = (𝑝 ∈ {{1, 2}} ↦ (𝑧 ∈ {1, 2} ↦ if(𝑧 = 1, 2, 1))) |
4 | 3 | rnmpt 5954 |
. . 3
⊢ ran
(𝑝 ∈ {{1, 2}} ↦
(𝑧 ∈ {1, 2} ↦
if(𝑧 = 1, 2, 1))) = {𝑡 ∣ ∃𝑝 ∈ {{1, 2}}𝑡 = (𝑧 ∈ {1, 2} ↦ if(𝑧 = 1, 2, 1))} |
5 | | 1ex 11209 |
. . . . . . . 8
⊢ 1 ∈
V |
6 | | id 22 |
. . . . . . . . . 10
⊢ (1 ∈
V → 1 ∈ V) |
7 | | 2nn 12284 |
. . . . . . . . . . 11
⊢ 2 ∈
ℕ |
8 | 7 | a1i 11 |
. . . . . . . . . 10
⊢ (1 ∈
V → 2 ∈ ℕ) |
9 | | iftrue 4534 |
. . . . . . . . . . 11
⊢ (𝑧 = 1 → if(𝑧 = 1, 2, 1) =
2) |
10 | 9 | adantl 482 |
. . . . . . . . . 10
⊢ ((1
∈ V ∧ 𝑧 = 1)
→ if(𝑧 = 1, 2, 1) =
2) |
11 | | 1ne2 12419 |
. . . . . . . . . . . . . 14
⊢ 1 ≠
2 |
12 | 11 | nesymi 2998 |
. . . . . . . . . . . . 13
⊢ ¬ 2
= 1 |
13 | | eqeq1 2736 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 2 → (𝑧 = 1 ↔ 2 = 1)) |
14 | 12, 13 | mtbiri 326 |
. . . . . . . . . . . 12
⊢ (𝑧 = 2 → ¬ 𝑧 = 1) |
15 | 14 | iffalsed 4539 |
. . . . . . . . . . 11
⊢ (𝑧 = 2 → if(𝑧 = 1, 2, 1) =
1) |
16 | 15 | adantl 482 |
. . . . . . . . . 10
⊢ ((1
∈ V ∧ 𝑧 = 2)
→ if(𝑧 = 1, 2, 1) =
1) |
17 | 6, 8, 8, 6, 10, 16 | fmptpr 7169 |
. . . . . . . . 9
⊢ (1 ∈
V → {⟨1, 2⟩, ⟨2, 1⟩} = (𝑧 ∈ {1, 2} ↦ if(𝑧 = 1, 2, 1))) |
18 | 17 | eqeq2d 2743 |
. . . . . . . 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 223 |
. . . . . 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 2802 |
. . . 4
⊢ {𝑡 ∣ ∃𝑝 ∈ {{1, 2}}𝑡 = (𝑧 ∈ {1, 2} ↦ if(𝑧 = 1, 2, 1))} = {𝑡 ∣ ∃𝑝 ∈ {{1, 2}}𝑡 = {⟨1, 2⟩, ⟨2,
1⟩}} |
23 | | prex 5432 |
. . . . . . . 8
⊢ {1, 2}
∈ V |
24 | 23 | snnz 4780 |
. . . . . . 7
⊢ {{1, 2}}
≠ ∅ |
25 | | r19.9rzv 4499 |
. . . . . . . 8
⊢ ({{1, 2}}
≠ ∅ → (𝑠 =
{⟨1, 2⟩, ⟨2, 1⟩} ↔ ∃𝑝 ∈ {{1, 2}}𝑠 = {⟨1, 2⟩, ⟨2,
1⟩})) |
26 | 25 | bicomd 222 |
. . . . . . 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 3478 |
. . . . . . 7
⊢ 𝑠 ∈ V |
29 | | eqeq1 2736 |
. . . . . . . 8
⊢ (𝑡 = 𝑠 → (𝑡 = {⟨1, 2⟩, ⟨2, 1⟩}
↔ 𝑠 = {⟨1,
2⟩, ⟨2, 1⟩})) |
30 | 29 | rexbidv 3178 |
. . . . . . 7
⊢ (𝑡 = 𝑠 → (∃𝑝 ∈ {{1, 2}}𝑡 = {⟨1, 2⟩, ⟨2, 1⟩}
↔ ∃𝑝 ∈ {{1,
2}}𝑠 = {⟨1, 2⟩,
⟨2, 1⟩})) |
31 | 28, 30 | elab 3668 |
. . . . . 6
⊢ (𝑠 ∈ {𝑡 ∣ ∃𝑝 ∈ {{1, 2}}𝑡 = {⟨1, 2⟩, ⟨2, 1⟩}}
↔ ∃𝑝 ∈ {{1,
2}}𝑠 = {⟨1, 2⟩,
⟨2, 1⟩}) |
32 | | velsn 4644 |
. . . . . 6
⊢ (𝑠 ∈ {{⟨1, 2⟩,
⟨2, 1⟩}} ↔ 𝑠
= {⟨1, 2⟩, ⟨2, 1⟩}) |
33 | 27, 31, 32 | 3bitr4i 302 |
. . . . 5
⊢ (𝑠 ∈ {𝑡 ∣ ∃𝑝 ∈ {{1, 2}}𝑡 = {⟨1, 2⟩, ⟨2, 1⟩}}
↔ 𝑠 ∈ {{⟨1,
2⟩, ⟨2, 1⟩}}) |
34 | 33 | eqriv 2729 |
. . . 4
⊢ {𝑡 ∣ ∃𝑝 ∈ {{1, 2}}𝑡 = {⟨1, 2⟩, ⟨2,
1⟩}} = {{⟨1, 2⟩, ⟨2, 1⟩}} |
35 | 22, 34 | eqtri 2760 |
. . 3
⊢ {𝑡 ∣ ∃𝑝 ∈ {{1, 2}}𝑡 = (𝑧 ∈ {1, 2} ↦ if(𝑧 = 1, 2, 1))} = {{⟨1, 2⟩, ⟨2,
1⟩}} |
36 | 4, 35 | eqtri 2760 |
. 2
⊢ ran
(𝑝 ∈ {{1, 2}} ↦
(𝑧 ∈ {1, 2} ↦
if(𝑧 = 1, 2, 1))) =
{{⟨1, 2⟩, ⟨2, 1⟩}} |
37 | 2, 36 | eqtri 2760 |
1
⊢ ran
(pmTrsp‘{1, 2}) = {{⟨1, 2⟩, ⟨2, 1⟩}} |