# 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}\in \mathrm{card}\left({B}\right)\to ¬{A}\approx {B}$

### Proof

Step Hyp Ref Expression
1 elfvdm ${⊢}{A}\in \mathrm{card}\left({B}\right)\to {B}\in \mathrm{dom}\mathrm{card}$
2 cardon ${⊢}\mathrm{card}\left({B}\right)\in \mathrm{On}$
3 2 oneli ${⊢}{A}\in \mathrm{card}\left({B}\right)\to {A}\in \mathrm{On}$
4 breq1 ${⊢}{x}={A}\to \left({x}\approx {B}↔{A}\approx {B}\right)$
5 4 onintss ${⊢}{A}\in \mathrm{On}\to \left({A}\approx {B}\to \bigcap \left\{{x}\in \mathrm{On}|{x}\approx {B}\right\}\subseteq {A}\right)$
6 3 5 syl ${⊢}{A}\in \mathrm{card}\left({B}\right)\to \left({A}\approx {B}\to \bigcap \left\{{x}\in \mathrm{On}|{x}\approx {B}\right\}\subseteq {A}\right)$
7 6 adantl ${⊢}\left({B}\in \mathrm{dom}\mathrm{card}\wedge {A}\in \mathrm{card}\left({B}\right)\right)\to \left({A}\approx {B}\to \bigcap \left\{{x}\in \mathrm{On}|{x}\approx {B}\right\}\subseteq {A}\right)$
8 cardval3 ${⊢}{B}\in \mathrm{dom}\mathrm{card}\to \mathrm{card}\left({B}\right)=\bigcap \left\{{x}\in \mathrm{On}|{x}\approx {B}\right\}$
9 8 sseq1d ${⊢}{B}\in \mathrm{dom}\mathrm{card}\to \left(\mathrm{card}\left({B}\right)\subseteq {A}↔\bigcap \left\{{x}\in \mathrm{On}|{x}\approx {B}\right\}\subseteq {A}\right)$
10 9 adantr ${⊢}\left({B}\in \mathrm{dom}\mathrm{card}\wedge {A}\in \mathrm{card}\left({B}\right)\right)\to \left(\mathrm{card}\left({B}\right)\subseteq {A}↔\bigcap \left\{{x}\in \mathrm{On}|{x}\approx {B}\right\}\subseteq {A}\right)$
11 7 10 sylibrd ${⊢}\left({B}\in \mathrm{dom}\mathrm{card}\wedge {A}\in \mathrm{card}\left({B}\right)\right)\to \left({A}\approx {B}\to \mathrm{card}\left({B}\right)\subseteq {A}\right)$
12 ontri1 ${⊢}\left(\mathrm{card}\left({B}\right)\in \mathrm{On}\wedge {A}\in \mathrm{On}\right)\to \left(\mathrm{card}\left({B}\right)\subseteq {A}↔¬{A}\in \mathrm{card}\left({B}\right)\right)$
13 2 3 12 sylancr ${⊢}{A}\in \mathrm{card}\left({B}\right)\to \left(\mathrm{card}\left({B}\right)\subseteq {A}↔¬{A}\in \mathrm{card}\left({B}\right)\right)$
14 13 adantl ${⊢}\left({B}\in \mathrm{dom}\mathrm{card}\wedge {A}\in \mathrm{card}\left({B}\right)\right)\to \left(\mathrm{card}\left({B}\right)\subseteq {A}↔¬{A}\in \mathrm{card}\left({B}\right)\right)$
15 11 14 sylibd ${⊢}\left({B}\in \mathrm{dom}\mathrm{card}\wedge {A}\in \mathrm{card}\left({B}\right)\right)\to \left({A}\approx {B}\to ¬{A}\in \mathrm{card}\left({B}\right)\right)$
16 15 con2d ${⊢}\left({B}\in \mathrm{dom}\mathrm{card}\wedge {A}\in \mathrm{card}\left({B}\right)\right)\to \left({A}\in \mathrm{card}\left({B}\right)\to ¬{A}\approx {B}\right)$
17 16 ex ${⊢}{B}\in \mathrm{dom}\mathrm{card}\to \left({A}\in \mathrm{card}\left({B}\right)\to \left({A}\in \mathrm{card}\left({B}\right)\to ¬{A}\approx {B}\right)\right)$
18 17 pm2.43d ${⊢}{B}\in \mathrm{dom}\mathrm{card}\to \left({A}\in \mathrm{card}\left({B}\right)\to ¬{A}\approx {B}\right)$
19 1 18 mpcom ${⊢}{A}\in \mathrm{card}\left({B}\right)\to ¬{A}\approx {B}$