Step | Hyp | Ref
| Expression |
1 | | fnpr2o 17440 |
. 2
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) →
{⟨∅, 𝐴⟩,
⟨1o, 𝐵⟩} Fn 2o) |
2 | | 0ex 5265 |
. . . . . . . 8
⊢ ∅
∈ V |
3 | 2 | prid1 4724 |
. . . . . . 7
⊢ ∅
∈ {∅, 1o} |
4 | | df2o3 8421 |
. . . . . . 7
⊢
2o = {∅, 1o} |
5 | 3, 4 | eleqtrri 2837 |
. . . . . 6
⊢ ∅
∈ 2o |
6 | | fndm 6606 |
. . . . . 6
⊢
({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩} Fn 2o →
dom {⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩} =
2o) |
7 | 5, 6 | eleqtrrid 2845 |
. . . . 5
⊢
({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩} Fn 2o →
∅ ∈ dom {⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}) |
8 | 2 | eldm2 5858 |
. . . . 5
⊢ (∅
∈ dom {⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩} ↔ ∃𝑘⟨∅, 𝑘⟩ ∈ {⟨∅,
𝐴⟩,
⟨1o, 𝐵⟩}) |
9 | 7, 8 | sylib 217 |
. . . 4
⊢
({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩} Fn 2o →
∃𝑘⟨∅,
𝑘⟩ ∈
{⟨∅, 𝐴⟩,
⟨1o, 𝐵⟩}) |
10 | | 1n0 8435 |
. . . . . . . . . . 11
⊢
1o ≠ ∅ |
11 | 10 | nesymi 3002 |
. . . . . . . . . 10
⊢ ¬
∅ = 1o |
12 | | vex 3450 |
. . . . . . . . . . 11
⊢ 𝑘 ∈ V |
13 | 2, 12 | opth1 5433 |
. . . . . . . . . 10
⊢
(⟨∅, 𝑘⟩ = ⟨1o, 𝐵⟩ → ∅ =
1o) |
14 | 11, 13 | mto 196 |
. . . . . . . . 9
⊢ ¬
⟨∅, 𝑘⟩ =
⟨1o, 𝐵⟩ |
15 | | elpri 4609 |
. . . . . . . . 9
⊢
(⟨∅, 𝑘⟩ ∈ {⟨∅, 𝐴⟩, ⟨1o,
𝐵⟩} →
(⟨∅, 𝑘⟩ =
⟨∅, 𝐴⟩ ∨
⟨∅, 𝑘⟩ =
⟨1o, 𝐵⟩)) |
16 | | orel2 890 |
. . . . . . . . 9
⊢ (¬
⟨∅, 𝑘⟩ =
⟨1o, 𝐵⟩ → ((⟨∅, 𝑘⟩ = ⟨∅, 𝐴⟩ ∨ ⟨∅, 𝑘⟩ = ⟨1o,
𝐵⟩) →
⟨∅, 𝑘⟩ =
⟨∅, 𝐴⟩)) |
17 | 14, 15, 16 | mpsyl 68 |
. . . . . . . 8
⊢
(⟨∅, 𝑘⟩ ∈ {⟨∅, 𝐴⟩, ⟨1o,
𝐵⟩} →
⟨∅, 𝑘⟩ =
⟨∅, 𝐴⟩) |
18 | 2, 12 | opth 5434 |
. . . . . . . 8
⊢
(⟨∅, 𝑘⟩ = ⟨∅, 𝐴⟩ ↔ (∅ = ∅ ∧ 𝑘 = 𝐴)) |
19 | 17, 18 | sylib 217 |
. . . . . . 7
⊢
(⟨∅, 𝑘⟩ ∈ {⟨∅, 𝐴⟩, ⟨1o,
𝐵⟩} → (∅ =
∅ ∧ 𝑘 = 𝐴)) |
20 | 19 | simprd 497 |
. . . . . 6
⊢
(⟨∅, 𝑘⟩ ∈ {⟨∅, 𝐴⟩, ⟨1o,
𝐵⟩} → 𝑘 = 𝐴) |
21 | 20 | eximi 1838 |
. . . . 5
⊢
(∃𝑘⟨∅, 𝑘⟩ ∈ {⟨∅, 𝐴⟩, ⟨1o,
𝐵⟩} →
∃𝑘 𝑘 = 𝐴) |
22 | | isset 3459 |
. . . . 5
⊢ (𝐴 ∈ V ↔ ∃𝑘 𝑘 = 𝐴) |
23 | 21, 22 | sylibr 233 |
. . . 4
⊢
(∃𝑘⟨∅, 𝑘⟩ ∈ {⟨∅, 𝐴⟩, ⟨1o,
𝐵⟩} → 𝐴 ∈ V) |
24 | 9, 23 | syl 17 |
. . 3
⊢
({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩} Fn 2o →
𝐴 ∈
V) |
25 | | 1oex 8423 |
. . . . . . . 8
⊢
1o ∈ V |
26 | 25 | prid2 4725 |
. . . . . . 7
⊢
1o ∈ {∅, 1o} |
27 | 26, 4 | eleqtrri 2837 |
. . . . . 6
⊢
1o ∈ 2o |
28 | 27, 6 | eleqtrrid 2845 |
. . . . 5
⊢
({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩} Fn 2o →
1o ∈ dom {⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}) |
29 | 25 | eldm2 5858 |
. . . . 5
⊢
(1o ∈ dom {⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩} ↔ ∃𝑘⟨1o, 𝑘⟩ ∈ {⟨∅,
𝐴⟩,
⟨1o, 𝐵⟩}) |
30 | 28, 29 | sylib 217 |
. . . 4
⊢
({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩} Fn 2o →
∃𝑘⟨1o, 𝑘⟩ ∈ {⟨∅, 𝐴⟩, ⟨1o,
𝐵⟩}) |
31 | 10 | neii 2946 |
. . . . . . . . . 10
⊢ ¬
1o = ∅ |
32 | 25, 12 | opth1 5433 |
. . . . . . . . . 10
⊢
(⟨1o, 𝑘⟩ = ⟨∅, 𝐴⟩ → 1o =
∅) |
33 | 31, 32 | mto 196 |
. . . . . . . . 9
⊢ ¬
⟨1o, 𝑘⟩ = ⟨∅, 𝐴⟩ |
34 | | elpri 4609 |
. . . . . . . . . 10
⊢
(⟨1o, 𝑘⟩ ∈ {⟨∅, 𝐴⟩, ⟨1o,
𝐵⟩} →
(⟨1o, 𝑘⟩ = ⟨∅, 𝐴⟩ ∨ ⟨1o, 𝑘⟩ = ⟨1o,
𝐵⟩)) |
35 | 34 | orcomd 870 |
. . . . . . . . 9
⊢
(⟨1o, 𝑘⟩ ∈ {⟨∅, 𝐴⟩, ⟨1o,
𝐵⟩} →
(⟨1o, 𝑘⟩ = ⟨1o, 𝐵⟩ ∨ ⟨1o,
𝑘⟩ = ⟨∅,
𝐴⟩)) |
36 | | orel2 890 |
. . . . . . . . 9
⊢ (¬
⟨1o, 𝑘⟩ = ⟨∅, 𝐴⟩ → ((⟨1o, 𝑘⟩ = ⟨1o,
𝐵⟩ ∨
⟨1o, 𝑘⟩ = ⟨∅, 𝐴⟩) → ⟨1o, 𝑘⟩ = ⟨1o,
𝐵⟩)) |
37 | 33, 35, 36 | mpsyl 68 |
. . . . . . . 8
⊢
(⟨1o, 𝑘⟩ ∈ {⟨∅, 𝐴⟩, ⟨1o,
𝐵⟩} →
⟨1o, 𝑘⟩ = ⟨1o, 𝐵⟩) |
38 | 25, 12 | opth 5434 |
. . . . . . . 8
⊢
(⟨1o, 𝑘⟩ = ⟨1o, 𝐵⟩ ↔ (1o =
1o ∧ 𝑘 =
𝐵)) |
39 | 37, 38 | sylib 217 |
. . . . . . 7
⊢
(⟨1o, 𝑘⟩ ∈ {⟨∅, 𝐴⟩, ⟨1o,
𝐵⟩} →
(1o = 1o ∧ 𝑘 = 𝐵)) |
40 | 39 | simprd 497 |
. . . . . 6
⊢
(⟨1o, 𝑘⟩ ∈ {⟨∅, 𝐴⟩, ⟨1o,
𝐵⟩} → 𝑘 = 𝐵) |
41 | 40 | eximi 1838 |
. . . . 5
⊢
(∃𝑘⟨1o, 𝑘⟩ ∈ {⟨∅, 𝐴⟩, ⟨1o,
𝐵⟩} →
∃𝑘 𝑘 = 𝐵) |
42 | | isset 3459 |
. . . . 5
⊢ (𝐵 ∈ V ↔ ∃𝑘 𝑘 = 𝐵) |
43 | 41, 42 | sylibr 233 |
. . . 4
⊢
(∃𝑘⟨1o, 𝑘⟩ ∈ {⟨∅, 𝐴⟩, ⟨1o,
𝐵⟩} → 𝐵 ∈ V) |
44 | 30, 43 | syl 17 |
. . 3
⊢
({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩} Fn 2o →
𝐵 ∈
V) |
45 | 24, 44 | jca 513 |
. 2
⊢
({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩} Fn 2o →
(𝐴 ∈ V ∧ 𝐵 ∈ V)) |
46 | 1, 45 | impbii 208 |
1
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ↔
{⟨∅, 𝐴⟩,
⟨1o, 𝐵⟩} Fn 2o) |