Step | Hyp | Ref
| Expression |
1 | | breq2 5152 |
. 2
⊢ (𝑎 = 𝐴 → (1o ≺ 𝑎 ↔ 1o ≺
𝐴)) |
2 | | rexeq 3322 |
. . 3
⊢ (𝑎 = 𝐴 → (∃𝑦 ∈ 𝑎 ¬ 𝑥 = 𝑦 ↔ ∃𝑦 ∈ 𝐴 ¬ 𝑥 = 𝑦)) |
3 | 2 | rexeqbi1dv 3335 |
. 2
⊢ (𝑎 = 𝐴 → (∃𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑎 ¬ 𝑥 = 𝑦 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ¬ 𝑥 = 𝑦)) |
4 | | 1onn 8636 |
. . . 4
⊢
1o ∈ ω |
5 | | sucdom 9232 |
. . . 4
⊢
(1o ∈ ω → (1o ≺ 𝑎 ↔ suc 1o
≼ 𝑎)) |
6 | 4, 5 | ax-mp 5 |
. . 3
⊢
(1o ≺ 𝑎 ↔ suc 1o ≼ 𝑎) |
7 | | df-2o 8464 |
. . . 4
⊢
2o = suc 1o |
8 | 7 | breq1i 5155 |
. . 3
⊢
(2o ≼ 𝑎 ↔ suc 1o ≼ 𝑎) |
9 | | 2dom 9027 |
. . . 4
⊢
(2o ≼ 𝑎 → ∃𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑎 ¬ 𝑥 = 𝑦) |
10 | | df2o3 8471 |
. . . . 5
⊢
2o = {∅, 1o} |
11 | | vex 3479 |
. . . . . . . . . . . 12
⊢ 𝑥 ∈ V |
12 | | vex 3479 |
. . . . . . . . . . . 12
⊢ 𝑦 ∈ V |
13 | | 0ex 5307 |
. . . . . . . . . . . 12
⊢ ∅
∈ V |
14 | | 1oex 8473 |
. . . . . . . . . . . 12
⊢
1o ∈ V |
15 | 11, 12, 13, 14 | funpr 6602 |
. . . . . . . . . . 11
⊢ (𝑥 ≠ 𝑦 → Fun {⟨𝑥, ∅⟩, ⟨𝑦, 1o⟩}) |
16 | | df-ne 2942 |
. . . . . . . . . . 11
⊢ (𝑥 ≠ 𝑦 ↔ ¬ 𝑥 = 𝑦) |
17 | | 1n0 8485 |
. . . . . . . . . . . . . . 15
⊢
1o ≠ ∅ |
18 | 17 | necomi 2996 |
. . . . . . . . . . . . . 14
⊢ ∅
≠ 1o |
19 | 13, 14, 11, 12 | fpr 7149 |
. . . . . . . . . . . . . 14
⊢ (∅
≠ 1o → {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}:{∅,
1o}⟶{𝑥,
𝑦}) |
20 | 18, 19 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
{⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}:{∅,
1o}⟶{𝑥,
𝑦} |
21 | | df-f1 6546 |
. . . . . . . . . . . . 13
⊢
({⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}:{∅,
1o}–1-1→{𝑥, 𝑦} ↔ ({⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}:{∅,
1o}⟶{𝑥,
𝑦} ∧ Fun ◡{⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})) |
22 | 20, 21 | mpbiran 708 |
. . . . . . . . . . . 12
⊢
({⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}:{∅,
1o}–1-1→{𝑥, 𝑦} ↔ Fun ◡{⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) |
23 | 13, 11 | cnvsn 6223 |
. . . . . . . . . . . . . . 15
⊢ ◡{⟨∅, 𝑥⟩} = {⟨𝑥, ∅⟩} |
24 | 14, 12 | cnvsn 6223 |
. . . . . . . . . . . . . . 15
⊢ ◡{⟨1o, 𝑦⟩} = {⟨𝑦, 1o⟩} |
25 | 23, 24 | uneq12i 4161 |
. . . . . . . . . . . . . 14
⊢ (◡{⟨∅, 𝑥⟩} ∪ ◡{⟨1o, 𝑦⟩}) = ({⟨𝑥, ∅⟩} ∪ {⟨𝑦,
1o⟩}) |
26 | | df-pr 4631 |
. . . . . . . . . . . . . . . 16
⊢
{⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩} = ({⟨∅, 𝑥⟩} ∪
{⟨1o, 𝑦⟩}) |
27 | 26 | cnveqi 5873 |
. . . . . . . . . . . . . . 15
⊢ ◡{⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩} = ◡({⟨∅, 𝑥⟩} ∪ {⟨1o, 𝑦⟩}) |
28 | | cnvun 6140 |
. . . . . . . . . . . . . . 15
⊢ ◡({⟨∅, 𝑥⟩} ∪ {⟨1o, 𝑦⟩}) = (◡{⟨∅, 𝑥⟩} ∪ ◡{⟨1o, 𝑦⟩}) |
29 | 27, 28 | eqtri 2761 |
. . . . . . . . . . . . . 14
⊢ ◡{⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩} = (◡{⟨∅, 𝑥⟩} ∪ ◡{⟨1o, 𝑦⟩}) |
30 | | df-pr 4631 |
. . . . . . . . . . . . . 14
⊢
{⟨𝑥,
∅⟩, ⟨𝑦,
1o⟩} = ({⟨𝑥, ∅⟩} ∪ {⟨𝑦,
1o⟩}) |
31 | 25, 29, 30 | 3eqtr4i 2771 |
. . . . . . . . . . . . 13
⊢ ◡{⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩} = {⟨𝑥, ∅⟩, ⟨𝑦,
1o⟩} |
32 | 31 | funeqi 6567 |
. . . . . . . . . . . 12
⊢ (Fun
◡{⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩} ↔ Fun {⟨𝑥, ∅⟩, ⟨𝑦,
1o⟩}) |
33 | 22, 32 | bitr2i 276 |
. . . . . . . . . . 11
⊢ (Fun
{⟨𝑥, ∅⟩,
⟨𝑦,
1o⟩} ↔ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}:{∅,
1o}–1-1→{𝑥, 𝑦}) |
34 | 15, 16, 33 | 3imtr3i 291 |
. . . . . . . . . 10
⊢ (¬
𝑥 = 𝑦 → {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}:{∅,
1o}–1-1→{𝑥, 𝑦}) |
35 | | prssi 4824 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝑎 ∧ 𝑦 ∈ 𝑎) → {𝑥, 𝑦} ⊆ 𝑎) |
36 | | f1ss 6791 |
. . . . . . . . . 10
⊢
(({⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}:{∅,
1o}–1-1→{𝑥, 𝑦} ∧ {𝑥, 𝑦} ⊆ 𝑎) → {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}:{∅,
1o}–1-1→𝑎) |
37 | 34, 35, 36 | syl2an 597 |
. . . . . . . . 9
⊢ ((¬
𝑥 = 𝑦 ∧ (𝑥 ∈ 𝑎 ∧ 𝑦 ∈ 𝑎)) → {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}:{∅,
1o}–1-1→𝑎) |
38 | | prex 5432 |
. . . . . . . . . 10
⊢
{⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩} ∈
V |
39 | | f1eq1 6780 |
. . . . . . . . . 10
⊢ (𝑓 = {⟨∅, 𝑥⟩, ⟨1o,
𝑦⟩} → (𝑓:{∅,
1o}–1-1→𝑎 ↔ {⟨∅, 𝑥⟩, ⟨1o,
𝑦⟩}:{∅,
1o}–1-1→𝑎)) |
40 | 38, 39 | spcev 3597 |
. . . . . . . . 9
⊢
({⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}:{∅,
1o}–1-1→𝑎 → ∃𝑓 𝑓:{∅, 1o}–1-1→𝑎) |
41 | 37, 40 | syl 17 |
. . . . . . . 8
⊢ ((¬
𝑥 = 𝑦 ∧ (𝑥 ∈ 𝑎 ∧ 𝑦 ∈ 𝑎)) → ∃𝑓 𝑓:{∅, 1o}–1-1→𝑎) |
42 | | vex 3479 |
. . . . . . . . 9
⊢ 𝑎 ∈ V |
43 | 42 | brdom 8953 |
. . . . . . . 8
⊢
({∅, 1o} ≼ 𝑎 ↔ ∃𝑓 𝑓:{∅, 1o}–1-1→𝑎) |
44 | 41, 43 | sylibr 233 |
. . . . . . 7
⊢ ((¬
𝑥 = 𝑦 ∧ (𝑥 ∈ 𝑎 ∧ 𝑦 ∈ 𝑎)) → {∅, 1o} ≼
𝑎) |
45 | 44 | expcom 415 |
. . . . . 6
⊢ ((𝑥 ∈ 𝑎 ∧ 𝑦 ∈ 𝑎) → (¬ 𝑥 = 𝑦 → {∅, 1o} ≼
𝑎)) |
46 | 45 | rexlimivv 3200 |
. . . . 5
⊢
(∃𝑥 ∈
𝑎 ∃𝑦 ∈ 𝑎 ¬ 𝑥 = 𝑦 → {∅, 1o} ≼
𝑎) |
47 | 10, 46 | eqbrtrid 5183 |
. . . 4
⊢
(∃𝑥 ∈
𝑎 ∃𝑦 ∈ 𝑎 ¬ 𝑥 = 𝑦 → 2o ≼ 𝑎) |
48 | 9, 47 | impbii 208 |
. . 3
⊢
(2o ≼ 𝑎 ↔ ∃𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑎 ¬ 𝑥 = 𝑦) |
49 | 6, 8, 48 | 3bitr2i 299 |
. 2
⊢
(1o ≺ 𝑎 ↔ ∃𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑎 ¬ 𝑥 = 𝑦) |
50 | 1, 3, 49 | vtoclbg 3560 |
1
⊢ (𝐴 ∈ 𝑉 → (1o ≺ 𝐴 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ¬ 𝑥 = 𝑦)) |