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 ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≺ 𝐴 ) )