Step | Hyp | Ref
| Expression |
1 | | df1o2 6319 |
. . . . 5
⊢
1o = {∅} |
2 | 1 | breq2i 3932 |
. . . 4
⊢ (𝐴 ≈ 1o ↔
𝐴 ≈
{∅}) |
3 | | bren 6634 |
. . . 4
⊢ (𝐴 ≈ {∅} ↔
∃𝑓 𝑓:𝐴–1-1-onto→{∅}) |
4 | 2, 3 | bitri 183 |
. . 3
⊢ (𝐴 ≈ 1o ↔
∃𝑓 𝑓:𝐴–1-1-onto→{∅}) |
5 | | f1ocnv 5373 |
. . . . 5
⊢ (𝑓:𝐴–1-1-onto→{∅} → ◡𝑓:{∅}–1-1-onto→𝐴) |
6 | | f1ofo 5367 |
. . . . . . . 8
⊢ (◡𝑓:{∅}–1-1-onto→𝐴 → ◡𝑓:{∅}–onto→𝐴) |
7 | | forn 5343 |
. . . . . . . 8
⊢ (◡𝑓:{∅}–onto→𝐴 → ran ◡𝑓 = 𝐴) |
8 | 6, 7 | syl 14 |
. . . . . . 7
⊢ (◡𝑓:{∅}–1-1-onto→𝐴 → ran ◡𝑓 = 𝐴) |
9 | | f1of 5360 |
. . . . . . . . . 10
⊢ (◡𝑓:{∅}–1-1-onto→𝐴 → ◡𝑓:{∅}⟶𝐴) |
10 | | 0ex 4050 |
. . . . . . . . . . . 12
⊢ ∅
∈ V |
11 | 10 | fsn2 5587 |
. . . . . . . . . . 11
⊢ (◡𝑓:{∅}⟶𝐴 ↔ ((◡𝑓‘∅) ∈ 𝐴 ∧ ◡𝑓 = {〈∅, (◡𝑓‘∅)〉})) |
12 | 11 | simprbi 273 |
. . . . . . . . . 10
⊢ (◡𝑓:{∅}⟶𝐴 → ◡𝑓 = {〈∅, (◡𝑓‘∅)〉}) |
13 | 9, 12 | syl 14 |
. . . . . . . . 9
⊢ (◡𝑓:{∅}–1-1-onto→𝐴 → ◡𝑓 = {〈∅, (◡𝑓‘∅)〉}) |
14 | 13 | rneqd 4763 |
. . . . . . . 8
⊢ (◡𝑓:{∅}–1-1-onto→𝐴 → ran ◡𝑓 = ran {〈∅, (◡𝑓‘∅)〉}) |
15 | 10 | rnsnop 5014 |
. . . . . . . 8
⊢ ran
{〈∅, (◡𝑓‘∅)〉} = {(◡𝑓‘∅)} |
16 | 14, 15 | syl6eq 2186 |
. . . . . . 7
⊢ (◡𝑓:{∅}–1-1-onto→𝐴 → ran ◡𝑓 = {(◡𝑓‘∅)}) |
17 | 8, 16 | eqtr3d 2172 |
. . . . . 6
⊢ (◡𝑓:{∅}–1-1-onto→𝐴 → 𝐴 = {(◡𝑓‘∅)}) |
18 | 5, 17 | syl 14 |
. . . . 5
⊢ (𝑓:𝐴–1-1-onto→{∅} → 𝐴 = {(◡𝑓‘∅)}) |
19 | | f1ofn 5361 |
. . . . . . 7
⊢ (◡𝑓:{∅}–1-1-onto→𝐴 → ◡𝑓 Fn {∅}) |
20 | 10 | snid 3551 |
. . . . . . 7
⊢ ∅
∈ {∅} |
21 | | funfvex 5431 |
. . . . . . . 8
⊢ ((Fun
◡𝑓 ∧ ∅ ∈ dom ◡𝑓) → (◡𝑓‘∅) ∈ V) |
22 | 21 | funfni 5218 |
. . . . . . 7
⊢ ((◡𝑓 Fn {∅} ∧ ∅ ∈ {∅})
→ (◡𝑓‘∅) ∈ V) |
23 | 19, 20, 22 | sylancl 409 |
. . . . . 6
⊢ (◡𝑓:{∅}–1-1-onto→𝐴 → (◡𝑓‘∅) ∈ V) |
24 | | sneq 3533 |
. . . . . . . 8
⊢ (𝑥 = (◡𝑓‘∅) → {𝑥} = {(◡𝑓‘∅)}) |
25 | 24 | eqeq2d 2149 |
. . . . . . 7
⊢ (𝑥 = (◡𝑓‘∅) → (𝐴 = {𝑥} ↔ 𝐴 = {(◡𝑓‘∅)})) |
26 | 25 | spcegv 2769 |
. . . . . 6
⊢ ((◡𝑓‘∅) ∈ V → (𝐴 = {(◡𝑓‘∅)} → ∃𝑥 𝐴 = {𝑥})) |
27 | 23, 26 | syl 14 |
. . . . 5
⊢ (◡𝑓:{∅}–1-1-onto→𝐴 → (𝐴 = {(◡𝑓‘∅)} → ∃𝑥 𝐴 = {𝑥})) |
28 | 5, 18, 27 | sylc 62 |
. . . 4
⊢ (𝑓:𝐴–1-1-onto→{∅} → ∃𝑥 𝐴 = {𝑥}) |
29 | 28 | exlimiv 1577 |
. . 3
⊢
(∃𝑓 𝑓:𝐴–1-1-onto→{∅} → ∃𝑥 𝐴 = {𝑥}) |
30 | 4, 29 | sylbi 120 |
. 2
⊢ (𝐴 ≈ 1o →
∃𝑥 𝐴 = {𝑥}) |
31 | | vex 2684 |
. . . . 5
⊢ 𝑥 ∈ V |
32 | 31 | ensn1 6683 |
. . . 4
⊢ {𝑥} ≈
1o |
33 | | breq1 3927 |
. . . 4
⊢ (𝐴 = {𝑥} → (𝐴 ≈ 1o ↔ {𝑥} ≈
1o)) |
34 | 32, 33 | mpbiri 167 |
. . 3
⊢ (𝐴 = {𝑥} → 𝐴 ≈ 1o) |
35 | 34 | exlimiv 1577 |
. 2
⊢
(∃𝑥 𝐴 = {𝑥} → 𝐴 ≈ 1o) |
36 | 30, 35 | impbii 125 |
1
⊢ (𝐴 ≈ 1o ↔
∃𝑥 𝐴 = {𝑥}) |