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 AcardB¬AB

Proof

Step Hyp Ref Expression
1 elfvdm AcardBBdomcard
2 cardon cardBOn
3 2 oneli AcardBAOn
4 breq1 x=AxBAB
5 4 onintss AOnABxOn|xBA
6 3 5 syl AcardBABxOn|xBA
7 6 adantl BdomcardAcardBABxOn|xBA
8 cardval3 BdomcardcardB=xOn|xB
9 8 sseq1d BdomcardcardBAxOn|xBA
10 9 adantr BdomcardAcardBcardBAxOn|xBA
11 7 10 sylibrd BdomcardAcardBABcardBA
12 ontri1 cardBOnAOncardBA¬AcardB
13 2 3 12 sylancr AcardBcardBA¬AcardB
14 13 adantl BdomcardAcardBcardBA¬AcardB
15 11 14 sylibd BdomcardAcardBAB¬AcardB
16 15 con2d BdomcardAcardBAcardB¬AB
17 16 ex BdomcardAcardBAcardB¬AB
18 17 pm2.43d BdomcardAcardB¬AB
19 1 18 mpcom AcardB¬AB