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 ∈ On ∧ ∀ x ∈ A x ≺ A

Proof

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