Metamath Proof Explorer

Theorem iscard

Description: Two ways to express the property of being a cardinal number. (Contributed by Mario Carneiro, 15-Jan-2013)

Ref Expression
Assertion iscard ${⊢}\mathrm{card}\left({A}\right)={A}↔\left({A}\in \mathrm{On}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}\prec {A}\right)$

Proof

Step Hyp Ref Expression
1 cardon ${⊢}\mathrm{card}\left({A}\right)\in \mathrm{On}$
2 eleq1 ${⊢}\mathrm{card}\left({A}\right)={A}\to \left(\mathrm{card}\left({A}\right)\in \mathrm{On}↔{A}\in \mathrm{On}\right)$
3 1 2 mpbii ${⊢}\mathrm{card}\left({A}\right)={A}\to {A}\in \mathrm{On}$
4 cardonle ${⊢}{A}\in \mathrm{On}\to \mathrm{card}\left({A}\right)\subseteq {A}$
5 eqss ${⊢}\mathrm{card}\left({A}\right)={A}↔\left(\mathrm{card}\left({A}\right)\subseteq {A}\wedge {A}\subseteq \mathrm{card}\left({A}\right)\right)$
6 5 baibr ${⊢}\mathrm{card}\left({A}\right)\subseteq {A}\to \left({A}\subseteq \mathrm{card}\left({A}\right)↔\mathrm{card}\left({A}\right)={A}\right)$
7 4 6 syl ${⊢}{A}\in \mathrm{On}\to \left({A}\subseteq \mathrm{card}\left({A}\right)↔\mathrm{card}\left({A}\right)={A}\right)$
8 onelon ${⊢}\left({A}\in \mathrm{On}\wedge {x}\in {A}\right)\to {x}\in \mathrm{On}$
9 onenon ${⊢}{A}\in \mathrm{On}\to {A}\in \mathrm{dom}\mathrm{card}$
10 9 adantr ${⊢}\left({A}\in \mathrm{On}\wedge {x}\in {A}\right)\to {A}\in \mathrm{dom}\mathrm{card}$
11 cardsdomel ${⊢}\left({x}\in \mathrm{On}\wedge {A}\in \mathrm{dom}\mathrm{card}\right)\to \left({x}\prec {A}↔{x}\in \mathrm{card}\left({A}\right)\right)$
12 8 10 11 syl2anc ${⊢}\left({A}\in \mathrm{On}\wedge {x}\in {A}\right)\to \left({x}\prec {A}↔{x}\in \mathrm{card}\left({A}\right)\right)$
13 12 ralbidva ${⊢}{A}\in \mathrm{On}\to \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}\prec {A}↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}\in \mathrm{card}\left({A}\right)\right)$
14 dfss3 ${⊢}{A}\subseteq \mathrm{card}\left({A}\right)↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}\in \mathrm{card}\left({A}\right)$
15 13 14 syl6rbbr ${⊢}{A}\in \mathrm{On}\to \left({A}\subseteq \mathrm{card}\left({A}\right)↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}\prec {A}\right)$
16 7 15 bitr3d ${⊢}{A}\in \mathrm{On}\to \left(\mathrm{card}\left({A}\right)={A}↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}\prec {A}\right)$
17 3 16 biadanii ${⊢}\mathrm{card}\left({A}\right)={A}↔\left({A}\in \mathrm{On}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}\prec {A}\right)$