Step | Hyp | Ref
| Expression |
1 | | df1o2 7725 |
. . . . 5
⊢
1𝑜 = {∅} |
2 | 1 | breq2i 4792 |
. . . 4
⊢ (𝐴 ≈ 1𝑜
↔ 𝐴 ≈
{∅}) |
3 | | bren 8117 |
. . . 4
⊢ (𝐴 ≈ {∅} ↔
∃𝑓 𝑓:𝐴–1-1-onto→{∅}) |
4 | 2, 3 | bitri 264 |
. . 3
⊢ (𝐴 ≈ 1𝑜
↔ ∃𝑓 𝑓:𝐴–1-1-onto→{∅}) |
5 | | f1ocnv 6290 |
. . . . 5
⊢ (𝑓:𝐴–1-1-onto→{∅} → ◡𝑓:{∅}–1-1-onto→𝐴) |
6 | | f1ofo 6285 |
. . . . . . 7
⊢ (◡𝑓:{∅}–1-1-onto→𝐴 → ◡𝑓:{∅}–onto→𝐴) |
7 | | forn 6259 |
. . . . . . 7
⊢ (◡𝑓:{∅}–onto→𝐴 → ran ◡𝑓 = 𝐴) |
8 | 6, 7 | syl 17 |
. . . . . 6
⊢ (◡𝑓:{∅}–1-1-onto→𝐴 → ran ◡𝑓 = 𝐴) |
9 | | f1of 6278 |
. . . . . . . . 9
⊢ (◡𝑓:{∅}–1-1-onto→𝐴 → ◡𝑓:{∅}⟶𝐴) |
10 | | 0ex 4921 |
. . . . . . . . . . 11
⊢ ∅
∈ V |
11 | 10 | fsn2 6545 |
. . . . . . . . . 10
⊢ (◡𝑓:{∅}⟶𝐴 ↔ ((◡𝑓‘∅) ∈ 𝐴 ∧ ◡𝑓 = {〈∅, (◡𝑓‘∅)〉})) |
12 | 11 | simprbi 478 |
. . . . . . . . 9
⊢ (◡𝑓:{∅}⟶𝐴 → ◡𝑓 = {〈∅, (◡𝑓‘∅)〉}) |
13 | 9, 12 | syl 17 |
. . . . . . . 8
⊢ (◡𝑓:{∅}–1-1-onto→𝐴 → ◡𝑓 = {〈∅, (◡𝑓‘∅)〉}) |
14 | 13 | rneqd 5491 |
. . . . . . 7
⊢ (◡𝑓:{∅}–1-1-onto→𝐴 → ran ◡𝑓 = ran {〈∅, (◡𝑓‘∅)〉}) |
15 | 10 | rnsnop 5759 |
. . . . . . 7
⊢ ran
{〈∅, (◡𝑓‘∅)〉} = {(◡𝑓‘∅)} |
16 | 14, 15 | syl6eq 2820 |
. . . . . 6
⊢ (◡𝑓:{∅}–1-1-onto→𝐴 → ran ◡𝑓 = {(◡𝑓‘∅)}) |
17 | 8, 16 | eqtr3d 2806 |
. . . . 5
⊢ (◡𝑓:{∅}–1-1-onto→𝐴 → 𝐴 = {(◡𝑓‘∅)}) |
18 | | fvex 6342 |
. . . . . 6
⊢ (◡𝑓‘∅) ∈ V |
19 | | sneq 4324 |
. . . . . . 7
⊢ (𝑥 = (◡𝑓‘∅) → {𝑥} = {(◡𝑓‘∅)}) |
20 | 19 | eqeq2d 2780 |
. . . . . 6
⊢ (𝑥 = (◡𝑓‘∅) → (𝐴 = {𝑥} ↔ 𝐴 = {(◡𝑓‘∅)})) |
21 | 18, 20 | spcev 3449 |
. . . . 5
⊢ (𝐴 = {(◡𝑓‘∅)} → ∃𝑥 𝐴 = {𝑥}) |
22 | 5, 17, 21 | 3syl 18 |
. . . 4
⊢ (𝑓:𝐴–1-1-onto→{∅} → ∃𝑥 𝐴 = {𝑥}) |
23 | 22 | exlimiv 2009 |
. . 3
⊢
(∃𝑓 𝑓:𝐴–1-1-onto→{∅} → ∃𝑥 𝐴 = {𝑥}) |
24 | 4, 23 | sylbi 207 |
. 2
⊢ (𝐴 ≈ 1𝑜
→ ∃𝑥 𝐴 = {𝑥}) |
25 | | vex 3352 |
. . . . 5
⊢ 𝑥 ∈ V |
26 | 25 | ensn1 8172 |
. . . 4
⊢ {𝑥} ≈
1𝑜 |
27 | | breq1 4787 |
. . . 4
⊢ (𝐴 = {𝑥} → (𝐴 ≈ 1𝑜 ↔ {𝑥} ≈
1𝑜)) |
28 | 26, 27 | mpbiri 248 |
. . 3
⊢ (𝐴 = {𝑥} → 𝐴 ≈
1𝑜) |
29 | 28 | exlimiv 2009 |
. 2
⊢
(∃𝑥 𝐴 = {𝑥} → 𝐴 ≈
1𝑜) |
30 | 24, 29 | impbii 199 |
1
⊢ (𝐴 ≈ 1𝑜
↔ ∃𝑥 𝐴 = {𝑥}) |