Step |
Hyp |
Ref |
Expression |
1 |
|
df1o2 |
⊢ 1o = { ∅ } |
2 |
1
|
breq2i |
⊢ ( 𝐴 ≈ 1o ↔ 𝐴 ≈ { ∅ } ) |
3 |
|
encv |
⊢ ( 𝐴 ≈ { ∅ } → ( 𝐴 ∈ V ∧ { ∅ } ∈ V ) ) |
4 |
|
breng |
⊢ ( ( 𝐴 ∈ V ∧ { ∅ } ∈ V ) → ( 𝐴 ≈ { ∅ } ↔ ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ { ∅ } ) ) |
5 |
3 4
|
syl |
⊢ ( 𝐴 ≈ { ∅ } → ( 𝐴 ≈ { ∅ } ↔ ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ { ∅ } ) ) |
6 |
5
|
ibi |
⊢ ( 𝐴 ≈ { ∅ } → ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ { ∅ } ) |
7 |
2 6
|
sylbi |
⊢ ( 𝐴 ≈ 1o → ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ { ∅ } ) |
8 |
|
f1ocnv |
⊢ ( 𝑓 : 𝐴 –1-1-onto→ { ∅ } → ◡ 𝑓 : { ∅ } –1-1-onto→ 𝐴 ) |
9 |
|
f1ofo |
⊢ ( ◡ 𝑓 : { ∅ } –1-1-onto→ 𝐴 → ◡ 𝑓 : { ∅ } –onto→ 𝐴 ) |
10 |
|
forn |
⊢ ( ◡ 𝑓 : { ∅ } –onto→ 𝐴 → ran ◡ 𝑓 = 𝐴 ) |
11 |
9 10
|
syl |
⊢ ( ◡ 𝑓 : { ∅ } –1-1-onto→ 𝐴 → ran ◡ 𝑓 = 𝐴 ) |
12 |
|
f1of |
⊢ ( ◡ 𝑓 : { ∅ } –1-1-onto→ 𝐴 → ◡ 𝑓 : { ∅ } ⟶ 𝐴 ) |
13 |
|
0ex |
⊢ ∅ ∈ V |
14 |
13
|
fsn2 |
⊢ ( ◡ 𝑓 : { ∅ } ⟶ 𝐴 ↔ ( ( ◡ 𝑓 ‘ ∅ ) ∈ 𝐴 ∧ ◡ 𝑓 = { 〈 ∅ , ( ◡ 𝑓 ‘ ∅ ) 〉 } ) ) |
15 |
14
|
simprbi |
⊢ ( ◡ 𝑓 : { ∅ } ⟶ 𝐴 → ◡ 𝑓 = { 〈 ∅ , ( ◡ 𝑓 ‘ ∅ ) 〉 } ) |
16 |
12 15
|
syl |
⊢ ( ◡ 𝑓 : { ∅ } –1-1-onto→ 𝐴 → ◡ 𝑓 = { 〈 ∅ , ( ◡ 𝑓 ‘ ∅ ) 〉 } ) |
17 |
16
|
rneqd |
⊢ ( ◡ 𝑓 : { ∅ } –1-1-onto→ 𝐴 → ran ◡ 𝑓 = ran { 〈 ∅ , ( ◡ 𝑓 ‘ ∅ ) 〉 } ) |
18 |
13
|
rnsnop |
⊢ ran { 〈 ∅ , ( ◡ 𝑓 ‘ ∅ ) 〉 } = { ( ◡ 𝑓 ‘ ∅ ) } |
19 |
17 18
|
eqtrdi |
⊢ ( ◡ 𝑓 : { ∅ } –1-1-onto→ 𝐴 → ran ◡ 𝑓 = { ( ◡ 𝑓 ‘ ∅ ) } ) |
20 |
11 19
|
eqtr3d |
⊢ ( ◡ 𝑓 : { ∅ } –1-1-onto→ 𝐴 → 𝐴 = { ( ◡ 𝑓 ‘ ∅ ) } ) |
21 |
|
fvex |
⊢ ( ◡ 𝑓 ‘ ∅ ) ∈ V |
22 |
|
sneq |
⊢ ( 𝑥 = ( ◡ 𝑓 ‘ ∅ ) → { 𝑥 } = { ( ◡ 𝑓 ‘ ∅ ) } ) |
23 |
22
|
eqeq2d |
⊢ ( 𝑥 = ( ◡ 𝑓 ‘ ∅ ) → ( 𝐴 = { 𝑥 } ↔ 𝐴 = { ( ◡ 𝑓 ‘ ∅ ) } ) ) |
24 |
21 23
|
spcev |
⊢ ( 𝐴 = { ( ◡ 𝑓 ‘ ∅ ) } → ∃ 𝑥 𝐴 = { 𝑥 } ) |
25 |
8 20 24
|
3syl |
⊢ ( 𝑓 : 𝐴 –1-1-onto→ { ∅ } → ∃ 𝑥 𝐴 = { 𝑥 } ) |
26 |
25
|
exlimiv |
⊢ ( ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ { ∅ } → ∃ 𝑥 𝐴 = { 𝑥 } ) |
27 |
7 26
|
syl |
⊢ ( 𝐴 ≈ 1o → ∃ 𝑥 𝐴 = { 𝑥 } ) |
28 |
|
vex |
⊢ 𝑥 ∈ V |
29 |
28
|
ensn1 |
⊢ { 𝑥 } ≈ 1o |
30 |
|
breq1 |
⊢ ( 𝐴 = { 𝑥 } → ( 𝐴 ≈ 1o ↔ { 𝑥 } ≈ 1o ) ) |
31 |
29 30
|
mpbiri |
⊢ ( 𝐴 = { 𝑥 } → 𝐴 ≈ 1o ) |
32 |
31
|
exlimiv |
⊢ ( ∃ 𝑥 𝐴 = { 𝑥 } → 𝐴 ≈ 1o ) |
33 |
27 32
|
impbii |
⊢ ( 𝐴 ≈ 1o ↔ ∃ 𝑥 𝐴 = { 𝑥 } ) |