Step | Hyp | Ref
| Expression |
1 | | pmtrprfval 19274 |
. . 3
⊢
(pmTrsp‘{1, 2}) = (𝑝 ∈ {{1, 2}} ↦ (𝑧 ∈ {1, 2} ↦ if(𝑧 = 1, 2, 1))) |
2 | 1 | rneqi 5893 |
. 2
⊢ ran
(pmTrsp‘{1, 2}) = ran (𝑝 ∈ {{1, 2}} ↦ (𝑧 ∈ {1, 2} ↦ if(𝑧 = 1, 2, 1))) |
3 | | eqid 2733 |
. . . 4
⊢ (𝑝 ∈ {{1, 2}} ↦ (𝑧 ∈ {1, 2} ↦ if(𝑧 = 1, 2, 1))) = (𝑝 ∈ {{1, 2}} ↦ (𝑧 ∈ {1, 2} ↦ if(𝑧 = 1, 2, 1))) |
4 | 3 | rnmpt 5911 |
. . 3
⊢ ran
(𝑝 ∈ {{1, 2}} ↦
(𝑧 ∈ {1, 2} ↦
if(𝑧 = 1, 2, 1))) = {𝑡 ∣ ∃𝑝 ∈ {{1, 2}}𝑡 = (𝑧 ∈ {1, 2} ↦ if(𝑧 = 1, 2, 1))} |
5 | | 1ex 11156 |
. . . . . . . 8
⊢ 1 ∈
V |
6 | | id 22 |
. . . . . . . . . 10
⊢ (1 ∈
V → 1 ∈ V) |
7 | | 2nn 12231 |
. . . . . . . . . . 11
⊢ 2 ∈
ℕ |
8 | 7 | a1i 11 |
. . . . . . . . . 10
⊢ (1 ∈
V → 2 ∈ ℕ) |
9 | | iftrue 4493 |
. . . . . . . . . . 11
⊢ (𝑧 = 1 → if(𝑧 = 1, 2, 1) =
2) |
10 | 9 | adantl 483 |
. . . . . . . . . 10
⊢ ((1
∈ V ∧ 𝑧 = 1)
→ if(𝑧 = 1, 2, 1) =
2) |
11 | | 1ne2 12366 |
. . . . . . . . . . . . . 14
⊢ 1 ≠
2 |
12 | 11 | nesymi 2998 |
. . . . . . . . . . . . 13
⊢ ¬ 2
= 1 |
13 | | eqeq1 2737 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 2 → (𝑧 = 1 ↔ 2 = 1)) |
14 | 12, 13 | mtbiri 327 |
. . . . . . . . . . . 12
⊢ (𝑧 = 2 → ¬ 𝑧 = 1) |
15 | 14 | iffalsed 4498 |
. . . . . . . . . . 11
⊢ (𝑧 = 2 → if(𝑧 = 1, 2, 1) =
1) |
16 | 15 | adantl 483 |
. . . . . . . . . 10
⊢ ((1
∈ V ∧ 𝑧 = 2)
→ if(𝑧 = 1, 2, 1) =
1) |
17 | 6, 8, 8, 6, 10, 16 | fmptpr 7119 |
. . . . . . . . 9
⊢ (1 ∈
V → {⟨1, 2⟩, ⟨2, 1⟩} = (𝑧 ∈ {1, 2} ↦ if(𝑧 = 1, 2, 1))) |
18 | 17 | eqeq2d 2744 |
. . . . . . . 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 2803 |
. . . 4
⊢ {𝑡 ∣ ∃𝑝 ∈ {{1, 2}}𝑡 = (𝑧 ∈ {1, 2} ↦ if(𝑧 = 1, 2, 1))} = {𝑡 ∣ ∃𝑝 ∈ {{1, 2}}𝑡 = {⟨1, 2⟩, ⟨2,
1⟩}} |
23 | | prex 5390 |
. . . . . . . 8
⊢ {1, 2}
∈ V |
24 | 23 | snnz 4738 |
. . . . . . 7
⊢ {{1, 2}}
≠ ∅ |
25 | | r19.9rzv 4458 |
. . . . . . . 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 3448 |
. . . . . . 7
⊢ 𝑠 ∈ V |
29 | | eqeq1 2737 |
. . . . . . . 8
⊢ (𝑡 = 𝑠 → (𝑡 = {⟨1, 2⟩, ⟨2, 1⟩}
↔ 𝑠 = {⟨1,
2⟩, ⟨2, 1⟩})) |
30 | 29 | rexbidv 3172 |
. . . . . . 7
⊢ (𝑡 = 𝑠 → (∃𝑝 ∈ {{1, 2}}𝑡 = {⟨1, 2⟩, ⟨2, 1⟩}
↔ ∃𝑝 ∈ {{1,
2}}𝑠 = {⟨1, 2⟩,
⟨2, 1⟩})) |
31 | 28, 30 | elab 3631 |
. . . . . 6
⊢ (𝑠 ∈ {𝑡 ∣ ∃𝑝 ∈ {{1, 2}}𝑡 = {⟨1, 2⟩, ⟨2, 1⟩}}
↔ ∃𝑝 ∈ {{1,
2}}𝑠 = {⟨1, 2⟩,
⟨2, 1⟩}) |
32 | | velsn 4603 |
. . . . . 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 2730 |
. . . 4
⊢ {𝑡 ∣ ∃𝑝 ∈ {{1, 2}}𝑡 = {⟨1, 2⟩, ⟨2,
1⟩}} = {{⟨1, 2⟩, ⟨2, 1⟩}} |
35 | 22, 34 | eqtri 2761 |
. . 3
⊢ {𝑡 ∣ ∃𝑝 ∈ {{1, 2}}𝑡 = (𝑧 ∈ {1, 2} ↦ if(𝑧 = 1, 2, 1))} = {{⟨1, 2⟩, ⟨2,
1⟩}} |
36 | 4, 35 | eqtri 2761 |
. 2
⊢ ran
(𝑝 ∈ {{1, 2}} ↦
(𝑧 ∈ {1, 2} ↦
if(𝑧 = 1, 2, 1))) =
{{⟨1, 2⟩, ⟨2, 1⟩}} |
37 | 2, 36 | eqtri 2761 |
1
⊢ ran
(pmTrsp‘{1, 2}) = {{⟨1, 2⟩, ⟨2, 1⟩}} |