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