This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cardne

Description: No member of a cardinal number of a set is equinumerous to the set. Proposition 10.6(2) of TakeutiZaring p. 85. (Contributed by Mario Carneiro, 9-Jan-2013)

Ref Expression
Assertion cardne 
|- ( A e. ( card ` B ) -> -. A ~~ B )

Proof

Step Hyp Ref Expression
1 elfvdm 
 |-  ( A e. ( card ` B ) -> B e. dom card )
2 cardon 
 |-  ( card ` B ) e. On
3 2 oneli 
 |-  ( A e. ( card ` B ) -> A e. On )
4 breq1 
 |-  ( x = A -> ( x ~~ B <-> A ~~ B ) )
5 4 onintss 
 |-  ( A e. On -> ( A ~~ B -> |^| { x e. On | x ~~ B } C_ A ) )
6 3 5 syl 
 |-  ( A e. ( card ` B ) -> ( A ~~ B -> |^| { x e. On | x ~~ B } C_ A ) )
7 6 adantl 
 |-  ( ( B e. dom card /\ A e. ( card ` B ) ) -> ( A ~~ B -> |^| { x e. On | x ~~ B } C_ A ) )
8 cardval3 
 |-  ( B e. dom card -> ( card ` B ) = |^| { x e. On | x ~~ B } )
9 8 sseq1d 
 |-  ( B e. dom card -> ( ( card ` B ) C_ A <-> |^| { x e. On | x ~~ B } C_ A ) )
10 9 adantr 
 |-  ( ( B e. dom card /\ A e. ( card ` B ) ) -> ( ( card ` B ) C_ A <-> |^| { x e. On | x ~~ B } C_ A ) )
11 7 10 sylibrd 
 |-  ( ( B e. dom card /\ A e. ( card ` B ) ) -> ( A ~~ B -> ( card ` B ) C_ A ) )
12 ontri1 
 |-  ( ( ( card ` B ) e. On /\ A e. On ) -> ( ( card ` B ) C_ A <-> -. A e. ( card ` B ) ) )
13 2 3 12 sylancr 
 |-  ( A e. ( card ` B ) -> ( ( card ` B ) C_ A <-> -. A e. ( card ` B ) ) )
14 13 adantl 
 |-  ( ( B e. dom card /\ A e. ( card ` B ) ) -> ( ( card ` B ) C_ A <-> -. A e. ( card ` B ) ) )
15 11 14 sylibd 
 |-  ( ( B e. dom card /\ A e. ( card ` B ) ) -> ( A ~~ B -> -. A e. ( card ` B ) ) )
16 15 con2d 
 |-  ( ( B e. dom card /\ A e. ( card ` B ) ) -> ( A e. ( card ` B ) -> -. A ~~ B ) )
17 16 ex 
 |-  ( B e. dom card -> ( A e. ( card ` B ) -> ( A e. ( card ` B ) -> -. A ~~ B ) ) )
18 17 pm2.43d 
 |-  ( B e. dom card -> ( A e. ( card ` B ) -> -. A ~~ B ) )
19 1 18 mpcom 
 |-  ( A e. ( card ` B ) -> -. A ~~ B )