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

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 
|- ( ( card ` A ) = A <-> ( A e. On /\ A. x e. A x ~< A ) )

Proof

Step Hyp Ref Expression
1 cardon 
 |-  ( card ` A ) e. On
2 eleq1 
 |-  ( ( card ` A ) = A -> ( ( card ` A ) e. On <-> A e. On ) )
3 1 2 mpbii 
 |-  ( ( card ` A ) = A -> A e. On )
4 cardonle 
 |-  ( A e. On -> ( card ` A ) C_ A )
5 eqss 
 |-  ( ( card ` A ) = A <-> ( ( card ` A ) C_ A /\ A C_ ( card ` A ) ) )
6 5 baibr 
 |-  ( ( card ` A ) C_ A -> ( A C_ ( card ` A ) <-> ( card ` A ) = A ) )
7 4 6 syl 
 |-  ( A e. On -> ( A C_ ( card ` A ) <-> ( card ` A ) = A ) )
8 dfss3 
 |-  ( A C_ ( card ` A ) <-> A. x e. A x e. ( card ` A ) )
9 onelon 
 |-  ( ( A e. On /\ x e. A ) -> x e. On )
10 onenon 
 |-  ( A e. On -> A e. dom card )
11 10 adantr 
 |-  ( ( A e. On /\ x e. A ) -> A e. dom card )
12 cardsdomel 
 |-  ( ( x e. On /\ A e. dom card ) -> ( x ~< A <-> x e. ( card ` A ) ) )
13 9 11 12 syl2anc 
 |-  ( ( A e. On /\ x e. A ) -> ( x ~< A <-> x e. ( card ` A ) ) )
14 13 ralbidva 
 |-  ( A e. On -> ( A. x e. A x ~< A <-> A. x e. A x e. ( card ` A ) ) )
15 8 14 bitr4id 
 |-  ( A e. On -> ( A C_ ( card ` A ) <-> A. x e. A x ~< A ) )
16 7 15 bitr3d 
 |-  ( A e. On -> ( ( card ` A ) = A <-> A. x e. A x ~< A ) )
17 3 16 biadanii 
 |-  ( ( card ` A ) = A <-> ( A e. On /\ A. x e. A x ~< A ) )