| Step | Hyp | Ref
| Expression |
| 1 | | relsdom 8992 |
. . . 4
⊢ Rel
≺ |
| 2 | 1 | brrelex2i 5742 |
. . 3
⊢
(1o ≺ 𝐴 → 𝐴 ∈ V) |
| 3 | | sdomdom 9020 |
. . . . . . 7
⊢
(1o ≺ 𝐴 → 1o ≼ 𝐴) |
| 4 | | 0sdom1dom 9274 |
. . . . . . 7
⊢ (∅
≺ 𝐴 ↔
1o ≼ 𝐴) |
| 5 | 3, 4 | sylibr 234 |
. . . . . 6
⊢
(1o ≺ 𝐴 → ∅ ≺ 𝐴) |
| 6 | | 0sdomg 9144 |
. . . . . . 7
⊢ (𝐴 ∈ V → (∅
≺ 𝐴 ↔ 𝐴 ≠ ∅)) |
| 7 | 2, 6 | syl 17 |
. . . . . 6
⊢
(1o ≺ 𝐴 → (∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅)) |
| 8 | 5, 7 | mpbid 232 |
. . . . 5
⊢
(1o ≺ 𝐴 → 𝐴 ≠ ∅) |
| 9 | | n0snor2el 4833 |
. . . . 5
⊢ (𝐴 ≠ ∅ →
(∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≠ 𝑦 ∨ ∃𝑥 𝐴 = {𝑥})) |
| 10 | 8, 9 | syl 17 |
. . . 4
⊢
(1o ≺ 𝐴 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≠ 𝑦 ∨ ∃𝑥 𝐴 = {𝑥})) |
| 11 | | sdomnen 9021 |
. . . . 5
⊢
(1o ≺ 𝐴 → ¬ 1o ≈ 𝐴) |
| 12 | | df1o2 8513 |
. . . . . . . 8
⊢
1o = {∅} |
| 13 | | 0ex 5307 |
. . . . . . . . 9
⊢ ∅
∈ V |
| 14 | | vex 3484 |
. . . . . . . . 9
⊢ 𝑥 ∈ V |
| 15 | | en2sn 9081 |
. . . . . . . . 9
⊢ ((∅
∈ V ∧ 𝑥 ∈ V)
→ {∅} ≈ {𝑥}) |
| 16 | 13, 14, 15 | mp2an 692 |
. . . . . . . 8
⊢ {∅}
≈ {𝑥} |
| 17 | 12, 16 | eqbrtri 5164 |
. . . . . . 7
⊢
1o ≈ {𝑥} |
| 18 | | breq2 5147 |
. . . . . . 7
⊢ (𝐴 = {𝑥} → (1o ≈ 𝐴 ↔ 1o ≈
{𝑥})) |
| 19 | 17, 18 | mpbiri 258 |
. . . . . 6
⊢ (𝐴 = {𝑥} → 1o ≈ 𝐴) |
| 20 | 19 | exlimiv 1930 |
. . . . 5
⊢
(∃𝑥 𝐴 = {𝑥} → 1o ≈ 𝐴) |
| 21 | 11, 20 | nsyl 140 |
. . . 4
⊢
(1o ≺ 𝐴 → ¬ ∃𝑥 𝐴 = {𝑥}) |
| 22 | 10, 21 | olcnd 878 |
. . 3
⊢
(1o ≺ 𝐴 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≠ 𝑦) |
| 23 | | rex2dom 9282 |
. . 3
⊢ ((𝐴 ∈ V ∧ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≠ 𝑦) → 2o ≼ 𝐴) |
| 24 | 2, 22, 23 | syl2anc 584 |
. 2
⊢
(1o ≺ 𝐴 → 2o ≼ 𝐴) |
| 25 | | snsspr1 4814 |
. . . . 5
⊢ {∅}
⊆ {∅, 1o} |
| 26 | | df2o3 8514 |
. . . . 5
⊢
2o = {∅, 1o} |
| 27 | 25, 12, 26 | 3sstr4i 4035 |
. . . 4
⊢
1o ⊆ 2o |
| 28 | | domssl 9038 |
. . . 4
⊢
((1o ⊆ 2o ∧ 2o ≼ 𝐴) → 1o ≼
𝐴) |
| 29 | 27, 28 | mpan 690 |
. . 3
⊢
(2o ≼ 𝐴 → 1o ≼ 𝐴) |
| 30 | | snnen2o 9273 |
. . . . . . . . . . . 12
⊢ ¬
{𝑦} ≈
2o |
| 31 | 13 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (⊤
→ ∅ ∈ V) |
| 32 | | 1oex 8516 |
. . . . . . . . . . . . . . . . 17
⊢
1o ∈ V |
| 33 | 32 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (⊤
→ 1o ∈ V) |
| 34 | | 1n0 8526 |
. . . . . . . . . . . . . . . . . 18
⊢
1o ≠ ∅ |
| 35 | 34 | nesymi 2998 |
. . . . . . . . . . . . . . . . 17
⊢ ¬
∅ = 1o |
| 36 | 35 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (⊤
→ ¬ ∅ = 1o) |
| 37 | 31, 33, 36 | enpr2d 9089 |
. . . . . . . . . . . . . . 15
⊢ (⊤
→ {∅, 1o} ≈ 2o) |
| 38 | 37 | mptru 1547 |
. . . . . . . . . . . . . 14
⊢ {∅,
1o} ≈ 2o |
| 39 | 26, 38 | eqbrtri 5164 |
. . . . . . . . . . . . 13
⊢
2o ≈ 2o |
| 40 | | breq1 5146 |
. . . . . . . . . . . . 13
⊢
(2o = {𝑦}
→ (2o ≈ 2o ↔ {𝑦} ≈ 2o)) |
| 41 | 39, 40 | mpbii 233 |
. . . . . . . . . . . 12
⊢
(2o = {𝑦}
→ {𝑦} ≈
2o) |
| 42 | 30, 41 | mto 197 |
. . . . . . . . . . 11
⊢ ¬
2o = {𝑦} |
| 43 | 42 | nex 1800 |
. . . . . . . . . 10
⊢ ¬
∃𝑦2o =
{𝑦} |
| 44 | | 2on0 8522 |
. . . . . . . . . . 11
⊢
2o ≠ ∅ |
| 45 | | f1cdmsn 7302 |
. . . . . . . . . . 11
⊢ ((𝑓:2o–1-1→{𝑥} ∧ 2o ≠ ∅) →
∃𝑦2o =
{𝑦}) |
| 46 | 44, 45 | mpan2 691 |
. . . . . . . . . 10
⊢ (𝑓:2o–1-1→{𝑥} → ∃𝑦2o = {𝑦}) |
| 47 | 43, 46 | mto 197 |
. . . . . . . . 9
⊢ ¬
𝑓:2o–1-1→{𝑥} |
| 48 | 47 | nex 1800 |
. . . . . . . 8
⊢ ¬
∃𝑓 𝑓:2o–1-1→{𝑥} |
| 49 | | brdomi 8999 |
. . . . . . . 8
⊢
(2o ≼ {𝑥} → ∃𝑓 𝑓:2o–1-1→{𝑥}) |
| 50 | 48, 49 | mto 197 |
. . . . . . 7
⊢ ¬
2o ≼ {𝑥} |
| 51 | | breq2 5147 |
. . . . . . 7
⊢ (𝐴 = {𝑥} → (2o ≼ 𝐴 ↔ 2o ≼
{𝑥})) |
| 52 | 50, 51 | mtbiri 327 |
. . . . . 6
⊢ (𝐴 = {𝑥} → ¬ 2o ≼ 𝐴) |
| 53 | 52 | con2i 139 |
. . . . 5
⊢
(2o ≼ 𝐴 → ¬ 𝐴 = {𝑥}) |
| 54 | 53 | nexdv 1936 |
. . . 4
⊢
(2o ≼ 𝐴 → ¬ ∃𝑥 𝐴 = {𝑥}) |
| 55 | | reldom 8991 |
. . . . . . 7
⊢ Rel
≼ |
| 56 | 55 | brrelex2i 5742 |
. . . . . 6
⊢
(2o ≼ 𝐴 → 𝐴 ∈ V) |
| 57 | | breng 8994 |
. . . . . . 7
⊢
((1o ∈ V ∧ 𝐴 ∈ V) → (1o ≈
𝐴 ↔ ∃𝑓 𝑓:1o–1-1-onto→𝐴)) |
| 58 | 32, 57 | mpan 690 |
. . . . . 6
⊢ (𝐴 ∈ V → (1o
≈ 𝐴 ↔
∃𝑓 𝑓:1o–1-1-onto→𝐴)) |
| 59 | 56, 58 | syl 17 |
. . . . 5
⊢
(2o ≼ 𝐴 → (1o ≈ 𝐴 ↔ ∃𝑓 𝑓:1o–1-1-onto→𝐴)) |
| 60 | 29, 4 | sylibr 234 |
. . . . . . 7
⊢
(2o ≼ 𝐴 → ∅ ≺ 𝐴) |
| 61 | 56, 6 | syl 17 |
. . . . . . 7
⊢
(2o ≼ 𝐴 → (∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅)) |
| 62 | 60, 61 | mpbid 232 |
. . . . . 6
⊢
(2o ≼ 𝐴 → 𝐴 ≠ ∅) |
| 63 | | f1ocnv 6860 |
. . . . . . . . . 10
⊢ (𝑓:1o–1-1-onto→𝐴 → ◡𝑓:𝐴–1-1-onto→1o) |
| 64 | | f1of1 6847 |
. . . . . . . . . . 11
⊢ (◡𝑓:𝐴–1-1-onto→1o → ◡𝑓:𝐴–1-1→1o) |
| 65 | | f1eq3 6801 |
. . . . . . . . . . . 12
⊢
(1o = {∅} → (◡𝑓:𝐴–1-1→1o ↔ ◡𝑓:𝐴–1-1→{∅})) |
| 66 | 12, 65 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (◡𝑓:𝐴–1-1→1o ↔ ◡𝑓:𝐴–1-1→{∅}) |
| 67 | 64, 66 | sylib 218 |
. . . . . . . . . 10
⊢ (◡𝑓:𝐴–1-1-onto→1o → ◡𝑓:𝐴–1-1→{∅}) |
| 68 | 63, 67 | syl 17 |
. . . . . . . . 9
⊢ (𝑓:1o–1-1-onto→𝐴 → ◡𝑓:𝐴–1-1→{∅}) |
| 69 | | f1cdmsn 7302 |
. . . . . . . . 9
⊢ ((◡𝑓:𝐴–1-1→{∅} ∧ 𝐴 ≠ ∅) → ∃𝑥 𝐴 = {𝑥}) |
| 70 | 68, 69 | sylan 580 |
. . . . . . . 8
⊢ ((𝑓:1o–1-1-onto→𝐴 ∧ 𝐴 ≠ ∅) → ∃𝑥 𝐴 = {𝑥}) |
| 71 | 70 | expcom 413 |
. . . . . . 7
⊢ (𝐴 ≠ ∅ → (𝑓:1o–1-1-onto→𝐴 → ∃𝑥 𝐴 = {𝑥})) |
| 72 | 71 | exlimdv 1933 |
. . . . . 6
⊢ (𝐴 ≠ ∅ →
(∃𝑓 𝑓:1o–1-1-onto→𝐴 → ∃𝑥 𝐴 = {𝑥})) |
| 73 | 62, 72 | syl 17 |
. . . . 5
⊢
(2o ≼ 𝐴 → (∃𝑓 𝑓:1o–1-1-onto→𝐴 → ∃𝑥 𝐴 = {𝑥})) |
| 74 | 59, 73 | sylbid 240 |
. . . 4
⊢
(2o ≼ 𝐴 → (1o ≈ 𝐴 → ∃𝑥 𝐴 = {𝑥})) |
| 75 | 54, 74 | mtod 198 |
. . 3
⊢
(2o ≼ 𝐴 → ¬ 1o ≈ 𝐴) |
| 76 | | brsdom 9015 |
. . 3
⊢
(1o ≺ 𝐴 ↔ (1o ≼ 𝐴 ∧ ¬ 1o
≈ 𝐴)) |
| 77 | 29, 75, 76 | sylanbrc 583 |
. 2
⊢
(2o ≼ 𝐴 → 1o ≺ 𝐴) |
| 78 | 24, 77 | impbii 209 |
1
⊢
(1o ≺ 𝐴 ↔ 2o ≼ 𝐴) |