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