Metamath Proof Explorer


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 ‘ 𝐴 ) ⊆ 𝐴 )