Step |
Hyp |
Ref |
Expression |
1 |
|
cardne |
|- ( ( card ` B ) e. ( card ` A ) -> -. ( card ` B ) ~~ A ) |
2 |
|
ennum |
|- ( A ~~ B -> ( A e. dom card <-> B e. dom card ) ) |
3 |
2
|
biimpa |
|- ( ( A ~~ B /\ A e. dom card ) -> B e. dom card ) |
4 |
|
cardid2 |
|- ( B e. dom card -> ( card ` B ) ~~ B ) |
5 |
3 4
|
syl |
|- ( ( A ~~ B /\ A e. dom card ) -> ( card ` B ) ~~ B ) |
6 |
|
ensym |
|- ( A ~~ B -> B ~~ A ) |
7 |
6
|
adantr |
|- ( ( A ~~ B /\ A e. dom card ) -> B ~~ A ) |
8 |
|
entr |
|- ( ( ( card ` B ) ~~ B /\ B ~~ A ) -> ( card ` B ) ~~ A ) |
9 |
5 7 8
|
syl2anc |
|- ( ( A ~~ B /\ A e. dom card ) -> ( card ` B ) ~~ A ) |
10 |
1 9
|
nsyl3 |
|- ( ( A ~~ B /\ A e. dom card ) -> -. ( card ` B ) e. ( card ` A ) ) |
11 |
|
cardon |
|- ( card ` A ) e. On |
12 |
|
cardon |
|- ( card ` B ) e. On |
13 |
|
ontri1 |
|- ( ( ( card ` A ) e. On /\ ( card ` B ) e. On ) -> ( ( card ` A ) C_ ( card ` B ) <-> -. ( card ` B ) e. ( card ` A ) ) ) |
14 |
11 12 13
|
mp2an |
|- ( ( card ` A ) C_ ( card ` B ) <-> -. ( card ` B ) e. ( card ` A ) ) |
15 |
10 14
|
sylibr |
|- ( ( A ~~ B /\ A e. dom card ) -> ( card ` A ) C_ ( card ` B ) ) |
16 |
|
cardne |
|- ( ( card ` A ) e. ( card ` B ) -> -. ( card ` A ) ~~ B ) |
17 |
|
cardid2 |
|- ( A e. dom card -> ( card ` A ) ~~ A ) |
18 |
|
id |
|- ( A ~~ B -> A ~~ B ) |
19 |
|
entr |
|- ( ( ( card ` A ) ~~ A /\ A ~~ B ) -> ( card ` A ) ~~ B ) |
20 |
17 18 19
|
syl2anr |
|- ( ( A ~~ B /\ A e. dom card ) -> ( card ` A ) ~~ B ) |
21 |
16 20
|
nsyl3 |
|- ( ( A ~~ B /\ A e. dom card ) -> -. ( card ` A ) e. ( card ` B ) ) |
22 |
|
ontri1 |
|- ( ( ( card ` B ) e. On /\ ( card ` A ) e. On ) -> ( ( card ` B ) C_ ( card ` A ) <-> -. ( card ` A ) e. ( card ` B ) ) ) |
23 |
12 11 22
|
mp2an |
|- ( ( card ` B ) C_ ( card ` A ) <-> -. ( card ` A ) e. ( card ` B ) ) |
24 |
21 23
|
sylibr |
|- ( ( A ~~ B /\ A e. dom card ) -> ( card ` B ) C_ ( card ` A ) ) |
25 |
15 24
|
eqssd |
|- ( ( A ~~ B /\ A e. dom card ) -> ( card ` A ) = ( card ` B ) ) |
26 |
|
ndmfv |
|- ( -. A e. dom card -> ( card ` A ) = (/) ) |
27 |
26
|
adantl |
|- ( ( A ~~ B /\ -. A e. dom card ) -> ( card ` A ) = (/) ) |
28 |
2
|
notbid |
|- ( A ~~ B -> ( -. A e. dom card <-> -. B e. dom card ) ) |
29 |
28
|
biimpa |
|- ( ( A ~~ B /\ -. A e. dom card ) -> -. B e. dom card ) |
30 |
|
ndmfv |
|- ( -. B e. dom card -> ( card ` B ) = (/) ) |
31 |
29 30
|
syl |
|- ( ( A ~~ B /\ -. A e. dom card ) -> ( card ` B ) = (/) ) |
32 |
27 31
|
eqtr4d |
|- ( ( A ~~ B /\ -. A e. dom card ) -> ( card ` A ) = ( card ` B ) ) |
33 |
25 32
|
pm2.61dan |
|- ( A ~~ B -> ( card ` A ) = ( card ` B ) ) |