Step | Hyp | Ref
| Expression |
1 | | breq2 4587 |
. 2
⊢ (𝑎 = 𝐴 → (1𝑜 ≺ 𝑎 ↔ 1𝑜
≺ 𝐴)) |
2 | | rexeq 3116 |
. . 3
⊢ (𝑎 = 𝐴 → (∃𝑦 ∈ 𝑎 ¬ 𝑥 = 𝑦 ↔ ∃𝑦 ∈ 𝐴 ¬ 𝑥 = 𝑦)) |
3 | 2 | rexeqbi1dv 3124 |
. 2
⊢ (𝑎 = 𝐴 → (∃𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑎 ¬ 𝑥 = 𝑦 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ¬ 𝑥 = 𝑦)) |
4 | | 1onn 7606 |
. . . 4
⊢
1𝑜 ∈ ω |
5 | | sucdom 8042 |
. . . 4
⊢
(1𝑜 ∈ ω → (1𝑜
≺ 𝑎 ↔ suc
1𝑜 ≼ 𝑎)) |
6 | 4, 5 | ax-mp 5 |
. . 3
⊢
(1𝑜 ≺ 𝑎 ↔ suc 1𝑜 ≼
𝑎) |
7 | | df-2o 7448 |
. . . 4
⊢
2𝑜 = suc 1𝑜 |
8 | 7 | breq1i 4590 |
. . 3
⊢
(2𝑜 ≼ 𝑎 ↔ suc 1𝑜 ≼
𝑎) |
9 | | 2dom 7915 |
. . . 4
⊢
(2𝑜 ≼ 𝑎 → ∃𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑎 ¬ 𝑥 = 𝑦) |
10 | | df2o3 7460 |
. . . . 5
⊢
2𝑜 = {∅,
1𝑜} |
11 | | vex 3176 |
. . . . . . . . . . . 12
⊢ 𝑥 ∈ V |
12 | | vex 3176 |
. . . . . . . . . . . 12
⊢ 𝑦 ∈ V |
13 | | 0ex 4718 |
. . . . . . . . . . . 12
⊢ ∅
∈ V |
14 | 4 | elexi 3186 |
. . . . . . . . . . . 12
⊢
1𝑜 ∈ V |
15 | 11, 12, 13, 14 | funpr 5858 |
. . . . . . . . . . 11
⊢ (𝑥 ≠ 𝑦 → Fun {〈𝑥, ∅〉, 〈𝑦,
1𝑜〉}) |
16 | | df-ne 2782 |
. . . . . . . . . . 11
⊢ (𝑥 ≠ 𝑦 ↔ ¬ 𝑥 = 𝑦) |
17 | | 1n0 7462 |
. . . . . . . . . . . . . . 15
⊢
1𝑜 ≠ ∅ |
18 | 17 | necomi 2836 |
. . . . . . . . . . . . . 14
⊢ ∅
≠ 1𝑜 |
19 | 13, 14, 11, 12 | fpr 6326 |
. . . . . . . . . . . . . 14
⊢ (∅
≠ 1𝑜 → {〈∅, 𝑥〉, 〈1𝑜, 𝑦〉}:{∅,
1𝑜}⟶{𝑥, 𝑦}) |
20 | 18, 19 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
{〈∅, 𝑥〉, 〈1𝑜, 𝑦〉}:{∅,
1𝑜}⟶{𝑥, 𝑦} |
21 | | df-f1 5809 |
. . . . . . . . . . . . 13
⊢
({〈∅, 𝑥〉, 〈1𝑜, 𝑦〉}:{∅,
1𝑜}–1-1→{𝑥, 𝑦} ↔ ({〈∅, 𝑥〉, 〈1𝑜, 𝑦〉}:{∅,
1𝑜}⟶{𝑥, 𝑦} ∧ Fun ◡{〈∅, 𝑥〉, 〈1𝑜, 𝑦〉})) |
22 | 20, 21 | mpbiran 955 |
. . . . . . . . . . . 12
⊢
({〈∅, 𝑥〉, 〈1𝑜, 𝑦〉}:{∅,
1𝑜}–1-1→{𝑥, 𝑦} ↔ Fun ◡{〈∅, 𝑥〉, 〈1𝑜, 𝑦〉}) |
23 | 13, 11 | cnvsn 5536 |
. . . . . . . . . . . . . . 15
⊢ ◡{〈∅, 𝑥〉} = {〈𝑥, ∅〉} |
24 | 14, 12 | cnvsn 5536 |
. . . . . . . . . . . . . . 15
⊢ ◡{〈1𝑜, 𝑦〉} = {〈𝑦,
1𝑜〉} |
25 | 23, 24 | uneq12i 3727 |
. . . . . . . . . . . . . 14
⊢ (◡{〈∅, 𝑥〉} ∪ ◡{〈1𝑜, 𝑦〉}) = ({〈𝑥, ∅〉} ∪
{〈𝑦,
1𝑜〉}) |
26 | | df-pr 4128 |
. . . . . . . . . . . . . . . 16
⊢
{〈∅, 𝑥〉, 〈1𝑜, 𝑦〉} = ({〈∅, 𝑥〉} ∪
{〈1𝑜, 𝑦〉}) |
27 | 26 | cnveqi 5219 |
. . . . . . . . . . . . . . 15
⊢ ◡{〈∅, 𝑥〉, 〈1𝑜, 𝑦〉} = ◡({〈∅, 𝑥〉} ∪ {〈1𝑜,
𝑦〉}) |
28 | | cnvun 5457 |
. . . . . . . . . . . . . . 15
⊢ ◡({〈∅, 𝑥〉} ∪ {〈1𝑜,
𝑦〉}) = (◡{〈∅, 𝑥〉} ∪ ◡{〈1𝑜, 𝑦〉}) |
29 | 27, 28 | eqtri 2632 |
. . . . . . . . . . . . . 14
⊢ ◡{〈∅, 𝑥〉, 〈1𝑜, 𝑦〉} = (◡{〈∅, 𝑥〉} ∪ ◡{〈1𝑜, 𝑦〉}) |
30 | | df-pr 4128 |
. . . . . . . . . . . . . 14
⊢
{〈𝑥,
∅〉, 〈𝑦,
1𝑜〉} = ({〈𝑥, ∅〉} ∪ {〈𝑦,
1𝑜〉}) |
31 | 25, 29, 30 | 3eqtr4i 2642 |
. . . . . . . . . . . . 13
⊢ ◡{〈∅, 𝑥〉, 〈1𝑜, 𝑦〉} = {〈𝑥, ∅〉, 〈𝑦,
1𝑜〉} |
32 | 31 | funeqi 5824 |
. . . . . . . . . . . 12
⊢ (Fun
◡{〈∅, 𝑥〉, 〈1𝑜, 𝑦〉} ↔ Fun {〈𝑥, ∅〉, 〈𝑦,
1𝑜〉}) |
33 | 22, 32 | bitr2i 264 |
. . . . . . . . . . 11
⊢ (Fun
{〈𝑥, ∅〉,
〈𝑦,
1𝑜〉} ↔ {〈∅, 𝑥〉, 〈1𝑜, 𝑦〉}:{∅,
1𝑜}–1-1→{𝑥, 𝑦}) |
34 | 15, 16, 33 | 3imtr3i 279 |
. . . . . . . . . 10
⊢ (¬
𝑥 = 𝑦 → {〈∅, 𝑥〉, 〈1𝑜, 𝑦〉}:{∅,
1𝑜}–1-1→{𝑥, 𝑦}) |
35 | | prssi 4293 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝑎 ∧ 𝑦 ∈ 𝑎) → {𝑥, 𝑦} ⊆ 𝑎) |
36 | | f1ss 6019 |
. . . . . . . . . 10
⊢
(({〈∅, 𝑥〉, 〈1𝑜, 𝑦〉}:{∅,
1𝑜}–1-1→{𝑥, 𝑦} ∧ {𝑥, 𝑦} ⊆ 𝑎) → {〈∅, 𝑥〉, 〈1𝑜, 𝑦〉}:{∅,
1𝑜}–1-1→𝑎) |
37 | 34, 35, 36 | syl2an 493 |
. . . . . . . . 9
⊢ ((¬
𝑥 = 𝑦 ∧ (𝑥 ∈ 𝑎 ∧ 𝑦 ∈ 𝑎)) → {〈∅, 𝑥〉, 〈1𝑜, 𝑦〉}:{∅,
1𝑜}–1-1→𝑎) |
38 | | prex 4836 |
. . . . . . . . . 10
⊢
{〈∅, 𝑥〉, 〈1𝑜, 𝑦〉} ∈
V |
39 | | f1eq1 6009 |
. . . . . . . . . 10
⊢ (𝑓 = {〈∅, 𝑥〉,
〈1𝑜, 𝑦〉} → (𝑓:{∅, 1𝑜}–1-1→𝑎 ↔ {〈∅, 𝑥〉, 〈1𝑜, 𝑦〉}:{∅,
1𝑜}–1-1→𝑎)) |
40 | 38, 39 | spcev 3273 |
. . . . . . . . 9
⊢
({〈∅, 𝑥〉, 〈1𝑜, 𝑦〉}:{∅,
1𝑜}–1-1→𝑎 → ∃𝑓 𝑓:{∅, 1𝑜}–1-1→𝑎) |
41 | 37, 40 | syl 17 |
. . . . . . . 8
⊢ ((¬
𝑥 = 𝑦 ∧ (𝑥 ∈ 𝑎 ∧ 𝑦 ∈ 𝑎)) → ∃𝑓 𝑓:{∅, 1𝑜}–1-1→𝑎) |
42 | | vex 3176 |
. . . . . . . . 9
⊢ 𝑎 ∈ V |
43 | 42 | brdom 7853 |
. . . . . . . 8
⊢
({∅, 1𝑜} ≼ 𝑎 ↔ ∃𝑓 𝑓:{∅, 1𝑜}–1-1→𝑎) |
44 | 41, 43 | sylibr 223 |
. . . . . . 7
⊢ ((¬
𝑥 = 𝑦 ∧ (𝑥 ∈ 𝑎 ∧ 𝑦 ∈ 𝑎)) → {∅, 1𝑜}
≼ 𝑎) |
45 | 44 | expcom 450 |
. . . . . 6
⊢ ((𝑥 ∈ 𝑎 ∧ 𝑦 ∈ 𝑎) → (¬ 𝑥 = 𝑦 → {∅, 1𝑜}
≼ 𝑎)) |
46 | 45 | rexlimivv 3018 |
. . . . 5
⊢
(∃𝑥 ∈
𝑎 ∃𝑦 ∈ 𝑎 ¬ 𝑥 = 𝑦 → {∅, 1𝑜}
≼ 𝑎) |
47 | 10, 46 | syl5eqbr 4618 |
. . . 4
⊢
(∃𝑥 ∈
𝑎 ∃𝑦 ∈ 𝑎 ¬ 𝑥 = 𝑦 → 2𝑜 ≼ 𝑎) |
48 | 9, 47 | impbii 198 |
. . 3
⊢
(2𝑜 ≼ 𝑎 ↔ ∃𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑎 ¬ 𝑥 = 𝑦) |
49 | 6, 8, 48 | 3bitr2i 287 |
. 2
⊢
(1𝑜 ≺ 𝑎 ↔ ∃𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑎 ¬ 𝑥 = 𝑦) |
50 | 1, 3, 49 | vtoclbg 3240 |
1
⊢ (𝐴 ∈ 𝑉 → (1𝑜 ≺ 𝐴 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ¬ 𝑥 = 𝑦)) |