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 )