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 ‘ 𝐴 ) = 𝐴 ↔ ( 𝐴 ∈ On ∧ ∀ 𝑥𝐴 𝑥𝐴 ) )

Proof

Step Hyp Ref Expression
1 cardon ( card ‘ 𝐴 ) ∈ On
2 eleq1 ( ( card ‘ 𝐴 ) = 𝐴 → ( ( card ‘ 𝐴 ) ∈ On ↔ 𝐴 ∈ On ) )
3 1 2 mpbii ( ( card ‘ 𝐴 ) = 𝐴𝐴 ∈ On )
4 cardonle ( 𝐴 ∈ On → ( card ‘ 𝐴 ) ⊆ 𝐴 )
5 eqss ( ( card ‘ 𝐴 ) = 𝐴 ↔ ( ( card ‘ 𝐴 ) ⊆ 𝐴𝐴 ⊆ ( card ‘ 𝐴 ) ) )
6 5 baibr ( ( card ‘ 𝐴 ) ⊆ 𝐴 → ( 𝐴 ⊆ ( card ‘ 𝐴 ) ↔ ( card ‘ 𝐴 ) = 𝐴 ) )
7 4 6 syl ( 𝐴 ∈ On → ( 𝐴 ⊆ ( card ‘ 𝐴 ) ↔ ( card ‘ 𝐴 ) = 𝐴 ) )
8 dfss3 ( 𝐴 ⊆ ( card ‘ 𝐴 ) ↔ ∀ 𝑥𝐴 𝑥 ∈ ( card ‘ 𝐴 ) )
9 onelon ( ( 𝐴 ∈ On ∧ 𝑥𝐴 ) → 𝑥 ∈ On )
10 onenon ( 𝐴 ∈ On → 𝐴 ∈ dom card )
11 10 adantr ( ( 𝐴 ∈ On ∧ 𝑥𝐴 ) → 𝐴 ∈ dom card )
12 cardsdomel ( ( 𝑥 ∈ On ∧ 𝐴 ∈ dom card ) → ( 𝑥𝐴𝑥 ∈ ( card ‘ 𝐴 ) ) )
13 9 11 12 syl2anc ( ( 𝐴 ∈ On ∧ 𝑥𝐴 ) → ( 𝑥𝐴𝑥 ∈ ( card ‘ 𝐴 ) ) )
14 13 ralbidva ( 𝐴 ∈ On → ( ∀ 𝑥𝐴 𝑥𝐴 ↔ ∀ 𝑥𝐴 𝑥 ∈ ( card ‘ 𝐴 ) ) )
15 8 14 bitr4id ( 𝐴 ∈ On → ( 𝐴 ⊆ ( card ‘ 𝐴 ) ↔ ∀ 𝑥𝐴 𝑥𝐴 ) )
16 7 15 bitr3d ( 𝐴 ∈ On → ( ( card ‘ 𝐴 ) = 𝐴 ↔ ∀ 𝑥𝐴 𝑥𝐴 ) )
17 3 16 biadanii ( ( card ‘ 𝐴 ) = 𝐴 ↔ ( 𝐴 ∈ On ∧ ∀ 𝑥𝐴 𝑥𝐴 ) )