Step |
Hyp |
Ref |
Expression |
1 |
|
1onn |
|- 1o e. _om |
2 |
|
cardnn |
|- ( 1o e. _om -> ( card ` 1o ) = 1o ) |
3 |
1 2
|
ax-mp |
|- ( card ` 1o ) = 1o |
4 |
|
1n0 |
|- 1o =/= (/) |
5 |
3 4
|
eqnetri |
|- ( card ` 1o ) =/= (/) |
6 |
|
carden2a |
|- ( ( ( card ` 1o ) = ( card ` A ) /\ ( card ` 1o ) =/= (/) ) -> 1o ~~ A ) |
7 |
5 6
|
mpan2 |
|- ( ( card ` 1o ) = ( card ` A ) -> 1o ~~ A ) |
8 |
7
|
eqcoms |
|- ( ( card ` A ) = ( card ` 1o ) -> 1o ~~ A ) |
9 |
8
|
ensymd |
|- ( ( card ` A ) = ( card ` 1o ) -> A ~~ 1o ) |
10 |
|
carden2b |
|- ( A ~~ 1o -> ( card ` A ) = ( card ` 1o ) ) |
11 |
9 10
|
impbii |
|- ( ( card ` A ) = ( card ` 1o ) <-> A ~~ 1o ) |
12 |
3
|
eqeq2i |
|- ( ( card ` A ) = ( card ` 1o ) <-> ( card ` A ) = 1o ) |
13 |
|
en1 |
|- ( A ~~ 1o <-> E. x A = { x } ) |
14 |
11 12 13
|
3bitr3i |
|- ( ( card ` A ) = 1o <-> E. x A = { x } ) |