Theorem cardonle

Description: The cardinal of an ordinal number is less than or equal to the ordinal number. Proposition 10.6(3) of TakeutiZaring p. 85. (Contributed by NM, 22-Oct-2003)

	Ref	Expression
Assertion	cardonle	⊢ ( 𝐴 ∈ On → ( card ‘ 𝐴 ) ⊆ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		oncardval	⊢ ( 𝐴 ∈ On → ( card ‘ 𝐴 ) = ∩ { 𝑥 ∈ On ∣ 𝑥 ≈ 𝐴 } )
2		enrefg	⊢ ( 𝐴 ∈ On → 𝐴 ≈ 𝐴 )
3		breq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ≈ 𝐴 ↔ 𝐴 ≈ 𝐴 ) )
4	3	intminss	⊢ ( ( 𝐴 ∈ On ∧ 𝐴 ≈ 𝐴 ) → ∩ { 𝑥 ∈ On ∣ 𝑥 ≈ 𝐴 } ⊆ 𝐴 )
5	2 4	mpdan	⊢ ( 𝐴 ∈ On → ∩ { 𝑥 ∈ On ∣ 𝑥 ≈ 𝐴 } ⊆ 𝐴 )
6	1 5	eqsstrd	⊢ ( 𝐴 ∈ On → ( card ‘ 𝐴 ) ⊆ 𝐴 )