Theorem alephord2i

Description: Ordering property of the aleph function. Theorem 66 of Suppes p. 229. (Contributed by NM, 25-Oct-2003)

	Ref	Expression
Assertion	alephord2i	⊢ ( 𝐵 ∈ On → ( 𝐴 ∈ 𝐵 → ( ℵ ‘ 𝐴 ) ∈ ( ℵ ‘ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		onelon	⊢ ( ( 𝐵 ∈ On ∧ 𝐴 ∈ 𝐵 ) → 𝐴 ∈ On )
2		alephord2	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ∈ 𝐵 ↔ ( ℵ ‘ 𝐴 ) ∈ ( ℵ ‘ 𝐵 ) ) )
3	2	biimpd	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ∈ 𝐵 → ( ℵ ‘ 𝐴 ) ∈ ( ℵ ‘ 𝐵 ) ) )
4	3	expimpd	⊢ ( 𝐴 ∈ On → ( ( 𝐵 ∈ On ∧ 𝐴 ∈ 𝐵 ) → ( ℵ ‘ 𝐴 ) ∈ ( ℵ ‘ 𝐵 ) ) )
5	1 4	mpcom	⊢ ( ( 𝐵 ∈ On ∧ 𝐴 ∈ 𝐵 ) → ( ℵ ‘ 𝐴 ) ∈ ( ℵ ‘ 𝐵 ) )
6	5	ex	⊢ ( 𝐵 ∈ On → ( 𝐴 ∈ 𝐵 → ( ℵ ‘ 𝐴 ) ∈ ( ℵ ‘ 𝐵 ) ) )