Theorem ondomen

Description: If a set is dominated by an ordinal, then it is numerable. (Contributed by Mario Carneiro, 5-Jan-2013)

	Ref	Expression
Assertion	ondomen	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ≼ 𝐴 ) → 𝐵 ∈ dom card )

Proof

Step	Hyp	Ref	Expression
1		breq2	⊢ ( 𝑥 = 𝐴 → ( 𝐵 ≼ 𝑥 ↔ 𝐵 ≼ 𝐴 ) )
2	1	rspcev	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ≼ 𝐴 ) → ∃ 𝑥 ∈ On 𝐵 ≼ 𝑥 )
3		ac10ct	⊢ ( ∃ 𝑥 ∈ On 𝐵 ≼ 𝑥 → ∃ 𝑟 𝑟 We 𝐵 )
4	2 3	syl	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ≼ 𝐴 ) → ∃ 𝑟 𝑟 We 𝐵 )
5		ween	⊢ ( 𝐵 ∈ dom card ↔ ∃ 𝑟 𝑟 We 𝐵 )
6	4 5	sylibr	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ≼ 𝐴 ) → 𝐵 ∈ dom card )