Step | Hyp | Ref
| Expression |
1 | | breq2 4657 |
. 2
⊢ (𝑎 = 𝐴 → (1𝑜 ≺ 𝑎 ↔ 1𝑜
≺ 𝐴)) |
2 | | rexeq 3139 |
. . 3
⊢ (𝑎 = 𝐴 → (∃𝑦 ∈ 𝑎 ¬ 𝑥 = 𝑦 ↔ ∃𝑦 ∈ 𝐴 ¬ 𝑥 = 𝑦)) |
3 | 2 | rexeqbi1dv 3147 |
. 2
⊢ (𝑎 = 𝐴 → (∃𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑎 ¬ 𝑥 = 𝑦 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ¬ 𝑥 = 𝑦)) |
4 | | 1onn 7719 |
. . . 4
⊢
1𝑜 ∈ ω |
5 | | sucdom 8157 |
. . . 4
⊢
(1𝑜 ∈ ω → (1𝑜
≺ 𝑎 ↔ suc
1𝑜 ≼ 𝑎)) |
6 | 4, 5 | ax-mp 5 |
. . 3
⊢
(1𝑜 ≺ 𝑎 ↔ suc 1𝑜 ≼
𝑎) |
7 | | df-2o 7561 |
. . . 4
⊢
2𝑜 = suc 1𝑜 |
8 | 7 | breq1i 4660 |
. . 3
⊢
(2𝑜 ≼ 𝑎 ↔ suc 1𝑜 ≼
𝑎) |
9 | | 2dom 8029 |
. . . 4
⊢
(2𝑜 ≼ 𝑎 → ∃𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑎 ¬ 𝑥 = 𝑦) |
10 | | df2o3 7573 |
. . . . 5
⊢
2𝑜 = {∅,
1𝑜} |
11 | | vex 3203 |
. . . . . . . . . . . 12
⊢ 𝑥 ∈ V |
12 | | vex 3203 |
. . . . . . . . . . . 12
⊢ 𝑦 ∈ V |
13 | | 0ex 4790 |
. . . . . . . . . . . 12
⊢ ∅
∈ V |
14 | 4 | elexi 3213 |
. . . . . . . . . . . 12
⊢
1𝑜 ∈ V |
15 | 11, 12, 13, 14 | funpr 5944 |
. . . . . . . . . . 11
⊢ (𝑥 ≠ 𝑦 → Fun {〈𝑥, ∅〉, 〈𝑦,
1𝑜〉}) |
16 | | df-ne 2795 |
. . . . . . . . . . 11
⊢ (𝑥 ≠ 𝑦 ↔ ¬ 𝑥 = 𝑦) |
17 | | 1n0 7575 |
. . . . . . . . . . . . . . 15
⊢
1𝑜 ≠ ∅ |
18 | 17 | necomi 2848 |
. . . . . . . . . . . . . 14
⊢ ∅
≠ 1𝑜 |
19 | 13, 14, 11, 12 | fpr 6421 |
. . . . . . . . . . . . . 14
⊢ (∅
≠ 1𝑜 → {〈∅, 𝑥〉, 〈1𝑜, 𝑦〉}:{∅,
1𝑜}⟶{𝑥, 𝑦}) |
20 | 18, 19 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
{〈∅, 𝑥〉, 〈1𝑜, 𝑦〉}:{∅,
1𝑜}⟶{𝑥, 𝑦} |
21 | | df-f1 5893 |
. . . . . . . . . . . . 13
⊢
({〈∅, 𝑥〉, 〈1𝑜, 𝑦〉}:{∅,
1𝑜}–1-1→{𝑥, 𝑦} ↔ ({〈∅, 𝑥〉, 〈1𝑜, 𝑦〉}:{∅,
1𝑜}⟶{𝑥, 𝑦} ∧ Fun ◡{〈∅, 𝑥〉, 〈1𝑜, 𝑦〉})) |
22 | 20, 21 | mpbiran 953 |
. . . . . . . . . . . 12
⊢
({〈∅, 𝑥〉, 〈1𝑜, 𝑦〉}:{∅,
1𝑜}–1-1→{𝑥, 𝑦} ↔ Fun ◡{〈∅, 𝑥〉, 〈1𝑜, 𝑦〉}) |
23 | 13, 11 | cnvsn 5618 |
. . . . . . . . . . . . . . 15
⊢ ◡{〈∅, 𝑥〉} = {〈𝑥, ∅〉} |
24 | 14, 12 | cnvsn 5618 |
. . . . . . . . . . . . . . 15
⊢ ◡{〈1𝑜, 𝑦〉} = {〈𝑦,
1𝑜〉} |
25 | 23, 24 | uneq12i 3765 |
. . . . . . . . . . . . . 14
⊢ (◡{〈∅, 𝑥〉} ∪ ◡{〈1𝑜, 𝑦〉}) = ({〈𝑥, ∅〉} ∪
{〈𝑦,
1𝑜〉}) |
26 | | df-pr 4180 |
. . . . . . . . . . . . . . . 16
⊢
{〈∅, 𝑥〉, 〈1𝑜, 𝑦〉} = ({〈∅, 𝑥〉} ∪
{〈1𝑜, 𝑦〉}) |
27 | 26 | cnveqi 5297 |
. . . . . . . . . . . . . . 15
⊢ ◡{〈∅, 𝑥〉, 〈1𝑜, 𝑦〉} = ◡({〈∅, 𝑥〉} ∪ {〈1𝑜,
𝑦〉}) |
28 | | cnvun 5538 |
. . . . . . . . . . . . . . 15
⊢ ◡({〈∅, 𝑥〉} ∪ {〈1𝑜,
𝑦〉}) = (◡{〈∅, 𝑥〉} ∪ ◡{〈1𝑜, 𝑦〉}) |
29 | 27, 28 | eqtri 2644 |
. . . . . . . . . . . . . 14
⊢ ◡{〈∅, 𝑥〉, 〈1𝑜, 𝑦〉} = (◡{〈∅, 𝑥〉} ∪ ◡{〈1𝑜, 𝑦〉}) |
30 | | df-pr 4180 |
. . . . . . . . . . . . . 14
⊢
{〈𝑥,
∅〉, 〈𝑦,
1𝑜〉} = ({〈𝑥, ∅〉} ∪ {〈𝑦,
1𝑜〉}) |
31 | 25, 29, 30 | 3eqtr4i 2654 |
. . . . . . . . . . . . 13
⊢ ◡{〈∅, 𝑥〉, 〈1𝑜, 𝑦〉} = {〈𝑥, ∅〉, 〈𝑦,
1𝑜〉} |
32 | 31 | funeqi 5909 |
. . . . . . . . . . . 12
⊢ (Fun
◡{〈∅, 𝑥〉, 〈1𝑜, 𝑦〉} ↔ Fun {〈𝑥, ∅〉, 〈𝑦,
1𝑜〉}) |
33 | 22, 32 | bitr2i 265 |
. . . . . . . . . . 11
⊢ (Fun
{〈𝑥, ∅〉,
〈𝑦,
1𝑜〉} ↔ {〈∅, 𝑥〉, 〈1𝑜, 𝑦〉}:{∅,
1𝑜}–1-1→{𝑥, 𝑦}) |
34 | 15, 16, 33 | 3imtr3i 280 |
. . . . . . . . . 10
⊢ (¬
𝑥 = 𝑦 → {〈∅, 𝑥〉, 〈1𝑜, 𝑦〉}:{∅,
1𝑜}–1-1→{𝑥, 𝑦}) |
35 | | prssi 4353 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝑎 ∧ 𝑦 ∈ 𝑎) → {𝑥, 𝑦} ⊆ 𝑎) |
36 | | f1ss 6106 |
. . . . . . . . . 10
⊢
(({〈∅, 𝑥〉, 〈1𝑜, 𝑦〉}:{∅,
1𝑜}–1-1→{𝑥, 𝑦} ∧ {𝑥, 𝑦} ⊆ 𝑎) → {〈∅, 𝑥〉, 〈1𝑜, 𝑦〉}:{∅,
1𝑜}–1-1→𝑎) |
37 | 34, 35, 36 | syl2an 494 |
. . . . . . . . 9
⊢ ((¬
𝑥 = 𝑦 ∧ (𝑥 ∈ 𝑎 ∧ 𝑦 ∈ 𝑎)) → {〈∅, 𝑥〉, 〈1𝑜, 𝑦〉}:{∅,
1𝑜}–1-1→𝑎) |
38 | | prex 4909 |
. . . . . . . . . 10
⊢
{〈∅, 𝑥〉, 〈1𝑜, 𝑦〉} ∈
V |
39 | | f1eq1 6096 |
. . . . . . . . . 10
⊢ (𝑓 = {〈∅, 𝑥〉,
〈1𝑜, 𝑦〉} → (𝑓:{∅, 1𝑜}–1-1→𝑎 ↔ {〈∅, 𝑥〉, 〈1𝑜, 𝑦〉}:{∅,
1𝑜}–1-1→𝑎)) |
40 | 38, 39 | spcev 3300 |
. . . . . . . . 9
⊢
({〈∅, 𝑥〉, 〈1𝑜, 𝑦〉}:{∅,
1𝑜}–1-1→𝑎 → ∃𝑓 𝑓:{∅, 1𝑜}–1-1→𝑎) |
41 | 37, 40 | syl 17 |
. . . . . . . 8
⊢ ((¬
𝑥 = 𝑦 ∧ (𝑥 ∈ 𝑎 ∧ 𝑦 ∈ 𝑎)) → ∃𝑓 𝑓:{∅, 1𝑜}–1-1→𝑎) |
42 | | vex 3203 |
. . . . . . . . 9
⊢ 𝑎 ∈ V |
43 | 42 | brdom 7967 |
. . . . . . . 8
⊢
({∅, 1𝑜} ≼ 𝑎 ↔ ∃𝑓 𝑓:{∅, 1𝑜}–1-1→𝑎) |
44 | 41, 43 | sylibr 224 |
. . . . . . 7
⊢ ((¬
𝑥 = 𝑦 ∧ (𝑥 ∈ 𝑎 ∧ 𝑦 ∈ 𝑎)) → {∅, 1𝑜}
≼ 𝑎) |
45 | 44 | expcom 451 |
. . . . . 6
⊢ ((𝑥 ∈ 𝑎 ∧ 𝑦 ∈ 𝑎) → (¬ 𝑥 = 𝑦 → {∅, 1𝑜}
≼ 𝑎)) |
46 | 45 | rexlimivv 3036 |
. . . . 5
⊢
(∃𝑥 ∈
𝑎 ∃𝑦 ∈ 𝑎 ¬ 𝑥 = 𝑦 → {∅, 1𝑜}
≼ 𝑎) |
47 | 10, 46 | syl5eqbr 4688 |
. . . 4
⊢
(∃𝑥 ∈
𝑎 ∃𝑦 ∈ 𝑎 ¬ 𝑥 = 𝑦 → 2𝑜 ≼ 𝑎) |
48 | 9, 47 | impbii 199 |
. . 3
⊢
(2𝑜 ≼ 𝑎 ↔ ∃𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑎 ¬ 𝑥 = 𝑦) |
49 | 6, 8, 48 | 3bitr2i 288 |
. 2
⊢
(1𝑜 ≺ 𝑎 ↔ ∃𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑎 ¬ 𝑥 = 𝑦) |
50 | 1, 3, 49 | vtoclbg 3267 |
1
⊢ (𝐴 ∈ 𝑉 → (1𝑜 ≺ 𝐴 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ¬ 𝑥 = 𝑦)) |