Step |
Hyp |
Ref |
Expression |
1 |
|
df2o3 |
⊢ 2o = { ∅ , 1o } |
2 |
|
0ex |
⊢ ∅ ∈ V |
3 |
|
1oex |
⊢ 1o ∈ V |
4 |
|
1n0 |
⊢ 1o ≠ ∅ |
5 |
4
|
necomi |
⊢ ∅ ≠ 1o |
6 |
|
prnesn |
⊢ ( ( ∅ ∈ V ∧ 1o ∈ V ∧ ∅ ≠ 1o ) → { ∅ , 1o } ≠ { 𝑥 } ) |
7 |
2 3 5 6
|
mp3an |
⊢ { ∅ , 1o } ≠ { 𝑥 } |
8 |
1 7
|
eqnetri |
⊢ 2o ≠ { 𝑥 } |
9 |
8
|
neii |
⊢ ¬ 2o = { 𝑥 } |
10 |
9
|
nex |
⊢ ¬ ∃ 𝑥 2o = { 𝑥 } |
11 |
|
2on0 |
⊢ 2o ≠ ∅ |
12 |
|
f1cdmsn |
⊢ ( ( ◡ 𝑓 : 2o –1-1→ { 𝐴 } ∧ 2o ≠ ∅ ) → ∃ 𝑥 2o = { 𝑥 } ) |
13 |
11 12
|
mpan2 |
⊢ ( ◡ 𝑓 : 2o –1-1→ { 𝐴 } → ∃ 𝑥 2o = { 𝑥 } ) |
14 |
10 13
|
mto |
⊢ ¬ ◡ 𝑓 : 2o –1-1→ { 𝐴 } |
15 |
|
f1ocnv |
⊢ ( 𝑓 : { 𝐴 } –1-1-onto→ 2o → ◡ 𝑓 : 2o –1-1-onto→ { 𝐴 } ) |
16 |
|
f1of1 |
⊢ ( ◡ 𝑓 : 2o –1-1-onto→ { 𝐴 } → ◡ 𝑓 : 2o –1-1→ { 𝐴 } ) |
17 |
15 16
|
syl |
⊢ ( 𝑓 : { 𝐴 } –1-1-onto→ 2o → ◡ 𝑓 : 2o –1-1→ { 𝐴 } ) |
18 |
14 17
|
mto |
⊢ ¬ 𝑓 : { 𝐴 } –1-1-onto→ 2o |
19 |
18
|
nex |
⊢ ¬ ∃ 𝑓 𝑓 : { 𝐴 } –1-1-onto→ 2o |
20 |
|
snex |
⊢ { 𝐴 } ∈ V |
21 |
|
2oex |
⊢ 2o ∈ V |
22 |
|
breng |
⊢ ( ( { 𝐴 } ∈ V ∧ 2o ∈ V ) → ( { 𝐴 } ≈ 2o ↔ ∃ 𝑓 𝑓 : { 𝐴 } –1-1-onto→ 2o ) ) |
23 |
20 21 22
|
mp2an |
⊢ ( { 𝐴 } ≈ 2o ↔ ∃ 𝑓 𝑓 : { 𝐴 } –1-1-onto→ 2o ) |
24 |
19 23
|
mtbir |
⊢ ¬ { 𝐴 } ≈ 2o |