Step | Hyp | Ref
| Expression |
1 | | df1o2 5952 |
. . . . 5
⊢
1𝑜 = {∅} |
2 | 1 | breq2i 3763 |
. . . 4
⊢ (A ≈ 1𝑜 ↔ A ≈ {∅}) |
3 | | bren 6164 |
. . . 4
⊢ (A ≈ {∅} ↔ ∃f f:A–1-1-onto→{∅}) |
4 | 2, 3 | bitri 173 |
. . 3
⊢ (A ≈ 1𝑜 ↔ ∃f f:A–1-1-onto→{∅}) |
5 | | f1ocnv 5082 |
. . . . 5
⊢ (f:A–1-1-onto→{∅} → ◡f:{∅}–1-1-onto→A) |
6 | | f1ofo 5076 |
. . . . . . . 8
⊢ (◡f:{∅}–1-1-onto→A →
◡f:{∅}–onto→A) |
7 | | forn 5052 |
. . . . . . . 8
⊢ (◡f:{∅}–onto→A →
ran ◡f = A) |
8 | 6, 7 | syl 14 |
. . . . . . 7
⊢ (◡f:{∅}–1-1-onto→A →
ran ◡f = A) |
9 | | f1of 5069 |
. . . . . . . . . 10
⊢ (◡f:{∅}–1-1-onto→A →
◡f:{∅}⟶A) |
10 | | 0ex 3875 |
. . . . . . . . . . . 12
⊢ ∅
∈ V |
11 | 10 | fsn2 5280 |
. . . . . . . . . . 11
⊢ (◡f:{∅}⟶A ↔ ((◡f‘∅) ∈
A ∧ ◡f =
{〈∅, (◡f‘∅)〉})) |
12 | 11 | simprbi 260 |
. . . . . . . . . 10
⊢ (◡f:{∅}⟶A → ◡f =
{〈∅, (◡f‘∅)〉}) |
13 | 9, 12 | syl 14 |
. . . . . . . . 9
⊢ (◡f:{∅}–1-1-onto→A →
◡f
= {〈∅, (◡f‘∅)〉}) |
14 | 13 | rneqd 4506 |
. . . . . . . 8
⊢ (◡f:{∅}–1-1-onto→A →
ran ◡f = ran {〈∅, (◡f‘∅)〉}) |
15 | 10 | rnsnop 4744 |
. . . . . . . 8
⊢ ran
{〈∅, (◡f‘∅)〉} = {(◡f‘∅)} |
16 | 14, 15 | syl6eq 2085 |
. . . . . . 7
⊢ (◡f:{∅}–1-1-onto→A →
ran ◡f = {(◡f‘∅)}) |
17 | 8, 16 | eqtr3d 2071 |
. . . . . 6
⊢ (◡f:{∅}–1-1-onto→A →
A = {(◡f‘∅)}) |
18 | 5, 17 | syl 14 |
. . . . 5
⊢ (f:A–1-1-onto→{∅} → A = {(◡f‘∅)}) |
19 | | f1ofn 5070 |
. . . . . . 7
⊢ (◡f:{∅}–1-1-onto→A →
◡f
Fn {∅}) |
20 | 10 | snid 3394 |
. . . . . . 7
⊢ ∅
∈ {∅} |
21 | | funfvex 5135 |
. . . . . . . 8
⊢ ((Fun
◡f
∧ ∅ ∈
dom ◡f) → (◡f‘∅) ∈
V) |
22 | 21 | funfni 4942 |
. . . . . . 7
⊢ ((◡f Fn
{∅} ∧ ∅ ∈ {∅}) → (◡f‘∅) ∈
V) |
23 | 19, 20, 22 | sylancl 392 |
. . . . . 6
⊢ (◡f:{∅}–1-1-onto→A →
(◡f‘∅) ∈
V) |
24 | | sneq 3378 |
. . . . . . . 8
⊢ (x = (◡f‘∅) → {x} = {(◡f‘∅)}) |
25 | 24 | eqeq2d 2048 |
. . . . . . 7
⊢ (x = (◡f‘∅) → (A = {x} ↔
A = {(◡f‘∅)})) |
26 | 25 | spcegv 2635 |
. . . . . 6
⊢ ((◡f‘∅) ∈
V → (A = {(◡f‘∅)} → ∃x A = {x})) |
27 | 23, 26 | syl 14 |
. . . . 5
⊢ (◡f:{∅}–1-1-onto→A →
(A = {(◡f‘∅)} → ∃x A = {x})) |
28 | 5, 18, 27 | sylc 56 |
. . . 4
⊢ (f:A–1-1-onto→{∅} → ∃x A = {x}) |
29 | 28 | exlimiv 1486 |
. . 3
⊢ (∃f f:A–1-1-onto→{∅} → ∃x A = {x}) |
30 | 4, 29 | sylbi 114 |
. 2
⊢ (A ≈ 1𝑜 → ∃x A = {x}) |
31 | | vex 2554 |
. . . . 5
⊢ x ∈
V |
32 | 31 | ensn1 6212 |
. . . 4
⊢ {x} ≈ 1𝑜 |
33 | | breq1 3758 |
. . . 4
⊢ (A = {x} →
(A ≈ 1𝑜 ↔
{x} ≈
1𝑜)) |
34 | 32, 33 | mpbiri 157 |
. . 3
⊢ (A = {x} →
A ≈
1𝑜) |
35 | 34 | exlimiv 1486 |
. 2
⊢ (∃x A = {x} →
A ≈
1𝑜) |
36 | 30, 35 | impbii 117 |
1
⊢ (A ≈ 1𝑜 ↔ ∃x A = {x}) |