| Step | Hyp | Ref
| Expression |
| 1 | | df1o2 8513 |
. . . . 5
⊢
1o = {∅} |
| 2 | 1 | breq2i 5151 |
. . . 4
⊢ (𝐴 ≈ 1o ↔
𝐴 ≈
{∅}) |
| 3 | | encv 8993 |
. . . . . 6
⊢ (𝐴 ≈ {∅} → (𝐴 ∈ V ∧ {∅} ∈
V)) |
| 4 | | breng 8994 |
. . . . . 6
⊢ ((𝐴 ∈ V ∧ {∅} ∈
V) → (𝐴 ≈
{∅} ↔ ∃𝑓
𝑓:𝐴–1-1-onto→{∅})) |
| 5 | 3, 4 | syl 17 |
. . . . 5
⊢ (𝐴 ≈ {∅} → (𝐴 ≈ {∅} ↔
∃𝑓 𝑓:𝐴–1-1-onto→{∅})) |
| 6 | 5 | ibi 267 |
. . . 4
⊢ (𝐴 ≈ {∅} →
∃𝑓 𝑓:𝐴–1-1-onto→{∅}) |
| 7 | 2, 6 | sylbi 217 |
. . 3
⊢ (𝐴 ≈ 1o →
∃𝑓 𝑓:𝐴–1-1-onto→{∅}) |
| 8 | | f1ocnv 6860 |
. . . . 5
⊢ (𝑓:𝐴–1-1-onto→{∅} → ◡𝑓:{∅}–1-1-onto→𝐴) |
| 9 | | f1ofo 6855 |
. . . . . . 7
⊢ (◡𝑓:{∅}–1-1-onto→𝐴 → ◡𝑓:{∅}–onto→𝐴) |
| 10 | | forn 6823 |
. . . . . . 7
⊢ (◡𝑓:{∅}–onto→𝐴 → ran ◡𝑓 = 𝐴) |
| 11 | 9, 10 | syl 17 |
. . . . . 6
⊢ (◡𝑓:{∅}–1-1-onto→𝐴 → ran ◡𝑓 = 𝐴) |
| 12 | | f1of 6848 |
. . . . . . . . 9
⊢ (◡𝑓:{∅}–1-1-onto→𝐴 → ◡𝑓:{∅}⟶𝐴) |
| 13 | | 0ex 5307 |
. . . . . . . . . . 11
⊢ ∅
∈ V |
| 14 | 13 | fsn2 7156 |
. . . . . . . . . 10
⊢ (◡𝑓:{∅}⟶𝐴 ↔ ((◡𝑓‘∅) ∈ 𝐴 ∧ ◡𝑓 = {〈∅, (◡𝑓‘∅)〉})) |
| 15 | 14 | simprbi 496 |
. . . . . . . . 9
⊢ (◡𝑓:{∅}⟶𝐴 → ◡𝑓 = {〈∅, (◡𝑓‘∅)〉}) |
| 16 | 12, 15 | syl 17 |
. . . . . . . 8
⊢ (◡𝑓:{∅}–1-1-onto→𝐴 → ◡𝑓 = {〈∅, (◡𝑓‘∅)〉}) |
| 17 | 16 | rneqd 5949 |
. . . . . . 7
⊢ (◡𝑓:{∅}–1-1-onto→𝐴 → ran ◡𝑓 = ran {〈∅, (◡𝑓‘∅)〉}) |
| 18 | 13 | rnsnop 6244 |
. . . . . . 7
⊢ ran
{〈∅, (◡𝑓‘∅)〉} = {(◡𝑓‘∅)} |
| 19 | 17, 18 | eqtrdi 2793 |
. . . . . 6
⊢ (◡𝑓:{∅}–1-1-onto→𝐴 → ran ◡𝑓 = {(◡𝑓‘∅)}) |
| 20 | 11, 19 | eqtr3d 2779 |
. . . . 5
⊢ (◡𝑓:{∅}–1-1-onto→𝐴 → 𝐴 = {(◡𝑓‘∅)}) |
| 21 | | fvex 6919 |
. . . . . 6
⊢ (◡𝑓‘∅) ∈ V |
| 22 | | sneq 4636 |
. . . . . . 7
⊢ (𝑥 = (◡𝑓‘∅) → {𝑥} = {(◡𝑓‘∅)}) |
| 23 | 22 | eqeq2d 2748 |
. . . . . 6
⊢ (𝑥 = (◡𝑓‘∅) → (𝐴 = {𝑥} ↔ 𝐴 = {(◡𝑓‘∅)})) |
| 24 | 21, 23 | spcev 3606 |
. . . . 5
⊢ (𝐴 = {(◡𝑓‘∅)} → ∃𝑥 𝐴 = {𝑥}) |
| 25 | 8, 20, 24 | 3syl 18 |
. . . 4
⊢ (𝑓:𝐴–1-1-onto→{∅} → ∃𝑥 𝐴 = {𝑥}) |
| 26 | 25 | exlimiv 1930 |
. . 3
⊢
(∃𝑓 𝑓:𝐴–1-1-onto→{∅} → ∃𝑥 𝐴 = {𝑥}) |
| 27 | 7, 26 | syl 17 |
. 2
⊢ (𝐴 ≈ 1o →
∃𝑥 𝐴 = {𝑥}) |
| 28 | | vex 3484 |
. . . . 5
⊢ 𝑥 ∈ V |
| 29 | 28 | ensn1 9061 |
. . . 4
⊢ {𝑥} ≈
1o |
| 30 | | breq1 5146 |
. . . 4
⊢ (𝐴 = {𝑥} → (𝐴 ≈ 1o ↔ {𝑥} ≈
1o)) |
| 31 | 29, 30 | mpbiri 258 |
. . 3
⊢ (𝐴 = {𝑥} → 𝐴 ≈ 1o) |
| 32 | 31 | exlimiv 1930 |
. 2
⊢
(∃𝑥 𝐴 = {𝑥} → 𝐴 ≈ 1o) |
| 33 | 27, 32 | impbii 209 |
1
⊢ (𝐴 ≈ 1o ↔
∃𝑥 𝐴 = {𝑥}) |