| Step | Hyp | Ref
| Expression |
| 1 | | fnpr2o 17602 |
. 2
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) →
{〈∅, 𝐴〉,
〈1o, 𝐵〉} Fn 2o) |
| 2 | | 0ex 5307 |
. . . . . . . 8
⊢ ∅
∈ V |
| 3 | 2 | prid1 4762 |
. . . . . . 7
⊢ ∅
∈ {∅, 1o} |
| 4 | | df2o3 8514 |
. . . . . . 7
⊢
2o = {∅, 1o} |
| 5 | 3, 4 | eleqtrri 2840 |
. . . . . 6
⊢ ∅
∈ 2o |
| 6 | | fndm 6671 |
. . . . . 6
⊢
({〈∅, 𝐴〉, 〈1o, 𝐵〉} Fn 2o →
dom {〈∅, 𝐴〉, 〈1o, 𝐵〉} =
2o) |
| 7 | 5, 6 | eleqtrrid 2848 |
. . . . 5
⊢
({〈∅, 𝐴〉, 〈1o, 𝐵〉} Fn 2o →
∅ ∈ dom {〈∅, 𝐴〉, 〈1o, 𝐵〉}) |
| 8 | 2 | eldm2 5912 |
. . . . 5
⊢ (∅
∈ dom {〈∅, 𝐴〉, 〈1o, 𝐵〉} ↔ ∃𝑘〈∅, 𝑘〉 ∈ {〈∅,
𝐴〉,
〈1o, 𝐵〉}) |
| 9 | 7, 8 | sylib 218 |
. . . 4
⊢
({〈∅, 𝐴〉, 〈1o, 𝐵〉} Fn 2o →
∃𝑘〈∅,
𝑘〉 ∈
{〈∅, 𝐴〉,
〈1o, 𝐵〉}) |
| 10 | | 1n0 8526 |
. . . . . . . . . . 11
⊢
1o ≠ ∅ |
| 11 | 10 | nesymi 2998 |
. . . . . . . . . 10
⊢ ¬
∅ = 1o |
| 12 | | vex 3484 |
. . . . . . . . . . 11
⊢ 𝑘 ∈ V |
| 13 | 2, 12 | opth1 5480 |
. . . . . . . . . 10
⊢
(〈∅, 𝑘〉 = 〈1o, 𝐵〉 → ∅ =
1o) |
| 14 | 11, 13 | mto 197 |
. . . . . . . . 9
⊢ ¬
〈∅, 𝑘〉 =
〈1o, 𝐵〉 |
| 15 | | elpri 4649 |
. . . . . . . . 9
⊢
(〈∅, 𝑘〉 ∈ {〈∅, 𝐴〉, 〈1o,
𝐵〉} →
(〈∅, 𝑘〉 =
〈∅, 𝐴〉 ∨
〈∅, 𝑘〉 =
〈1o, 𝐵〉)) |
| 16 | | orel2 891 |
. . . . . . . . 9
⊢ (¬
〈∅, 𝑘〉 =
〈1o, 𝐵〉 → ((〈∅, 𝑘〉 = 〈∅, 𝐴〉 ∨ 〈∅, 𝑘〉 = 〈1o,
𝐵〉) →
〈∅, 𝑘〉 =
〈∅, 𝐴〉)) |
| 17 | 14, 15, 16 | mpsyl 68 |
. . . . . . . 8
⊢
(〈∅, 𝑘〉 ∈ {〈∅, 𝐴〉, 〈1o,
𝐵〉} →
〈∅, 𝑘〉 =
〈∅, 𝐴〉) |
| 18 | 2, 12 | opth 5481 |
. . . . . . . 8
⊢
(〈∅, 𝑘〉 = 〈∅, 𝐴〉 ↔ (∅ = ∅ ∧ 𝑘 = 𝐴)) |
| 19 | 17, 18 | sylib 218 |
. . . . . . 7
⊢
(〈∅, 𝑘〉 ∈ {〈∅, 𝐴〉, 〈1o,
𝐵〉} → (∅ =
∅ ∧ 𝑘 = 𝐴)) |
| 20 | 19 | simprd 495 |
. . . . . 6
⊢
(〈∅, 𝑘〉 ∈ {〈∅, 𝐴〉, 〈1o,
𝐵〉} → 𝑘 = 𝐴) |
| 21 | 20 | eximi 1835 |
. . . . 5
⊢
(∃𝑘〈∅, 𝑘〉 ∈ {〈∅, 𝐴〉, 〈1o,
𝐵〉} →
∃𝑘 𝑘 = 𝐴) |
| 22 | | isset 3494 |
. . . . 5
⊢ (𝐴 ∈ V ↔ ∃𝑘 𝑘 = 𝐴) |
| 23 | 21, 22 | sylibr 234 |
. . . 4
⊢
(∃𝑘〈∅, 𝑘〉 ∈ {〈∅, 𝐴〉, 〈1o,
𝐵〉} → 𝐴 ∈ V) |
| 24 | 9, 23 | syl 17 |
. . 3
⊢
({〈∅, 𝐴〉, 〈1o, 𝐵〉} Fn 2o →
𝐴 ∈
V) |
| 25 | | 1oex 8516 |
. . . . . . . 8
⊢
1o ∈ V |
| 26 | 25 | prid2 4763 |
. . . . . . 7
⊢
1o ∈ {∅, 1o} |
| 27 | 26, 4 | eleqtrri 2840 |
. . . . . 6
⊢
1o ∈ 2o |
| 28 | 27, 6 | eleqtrrid 2848 |
. . . . 5
⊢
({〈∅, 𝐴〉, 〈1o, 𝐵〉} Fn 2o →
1o ∈ dom {〈∅, 𝐴〉, 〈1o, 𝐵〉}) |
| 29 | 25 | eldm2 5912 |
. . . . 5
⊢
(1o ∈ dom {〈∅, 𝐴〉, 〈1o, 𝐵〉} ↔ ∃𝑘〈1o, 𝑘〉 ∈ {〈∅,
𝐴〉,
〈1o, 𝐵〉}) |
| 30 | 28, 29 | sylib 218 |
. . . 4
⊢
({〈∅, 𝐴〉, 〈1o, 𝐵〉} Fn 2o →
∃𝑘〈1o, 𝑘〉 ∈ {〈∅, 𝐴〉, 〈1o,
𝐵〉}) |
| 31 | 10 | neii 2942 |
. . . . . . . . . 10
⊢ ¬
1o = ∅ |
| 32 | 25, 12 | opth1 5480 |
. . . . . . . . . 10
⊢
(〈1o, 𝑘〉 = 〈∅, 𝐴〉 → 1o =
∅) |
| 33 | 31, 32 | mto 197 |
. . . . . . . . 9
⊢ ¬
〈1o, 𝑘〉 = 〈∅, 𝐴〉 |
| 34 | | elpri 4649 |
. . . . . . . . . 10
⊢
(〈1o, 𝑘〉 ∈ {〈∅, 𝐴〉, 〈1o,
𝐵〉} →
(〈1o, 𝑘〉 = 〈∅, 𝐴〉 ∨ 〈1o, 𝑘〉 = 〈1o,
𝐵〉)) |
| 35 | 34 | orcomd 872 |
. . . . . . . . 9
⊢
(〈1o, 𝑘〉 ∈ {〈∅, 𝐴〉, 〈1o,
𝐵〉} →
(〈1o, 𝑘〉 = 〈1o, 𝐵〉 ∨ 〈1o,
𝑘〉 = 〈∅,
𝐴〉)) |
| 36 | | orel2 891 |
. . . . . . . . 9
⊢ (¬
〈1o, 𝑘〉 = 〈∅, 𝐴〉 → ((〈1o, 𝑘〉 = 〈1o,
𝐵〉 ∨
〈1o, 𝑘〉 = 〈∅, 𝐴〉) → 〈1o, 𝑘〉 = 〈1o,
𝐵〉)) |
| 37 | 33, 35, 36 | mpsyl 68 |
. . . . . . . 8
⊢
(〈1o, 𝑘〉 ∈ {〈∅, 𝐴〉, 〈1o,
𝐵〉} →
〈1o, 𝑘〉 = 〈1o, 𝐵〉) |
| 38 | 25, 12 | opth 5481 |
. . . . . . . 8
⊢
(〈1o, 𝑘〉 = 〈1o, 𝐵〉 ↔ (1o =
1o ∧ 𝑘 =
𝐵)) |
| 39 | 37, 38 | sylib 218 |
. . . . . . 7
⊢
(〈1o, 𝑘〉 ∈ {〈∅, 𝐴〉, 〈1o,
𝐵〉} →
(1o = 1o ∧ 𝑘 = 𝐵)) |
| 40 | 39 | simprd 495 |
. . . . . 6
⊢
(〈1o, 𝑘〉 ∈ {〈∅, 𝐴〉, 〈1o,
𝐵〉} → 𝑘 = 𝐵) |
| 41 | 40 | eximi 1835 |
. . . . 5
⊢
(∃𝑘〈1o, 𝑘〉 ∈ {〈∅, 𝐴〉, 〈1o,
𝐵〉} →
∃𝑘 𝑘 = 𝐵) |
| 42 | | isset 3494 |
. . . . 5
⊢ (𝐵 ∈ V ↔ ∃𝑘 𝑘 = 𝐵) |
| 43 | 41, 42 | sylibr 234 |
. . . 4
⊢
(∃𝑘〈1o, 𝑘〉 ∈ {〈∅, 𝐴〉, 〈1o,
𝐵〉} → 𝐵 ∈ V) |
| 44 | 30, 43 | syl 17 |
. . 3
⊢
({〈∅, 𝐴〉, 〈1o, 𝐵〉} Fn 2o →
𝐵 ∈
V) |
| 45 | 24, 44 | jca 511 |
. 2
⊢
({〈∅, 𝐴〉, 〈1o, 𝐵〉} Fn 2o →
(𝐴 ∈ V ∧ 𝐵 ∈ V)) |
| 46 | 1, 45 | impbii 209 |
1
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ↔
{〈∅, 𝐴〉,
〈1o, 𝐵〉} Fn 2o) |