Theorem alephord2

Description: Ordering property of the aleph function. Theorem 8A(a) of Enderton p. 213 and its converse. (Contributed by NM, 3-Nov-2003) (Revised by Mario Carneiro, 9-Feb-2013)

	Ref	Expression
Assertion	alephord2	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ∈ 𝐵 ↔ ( ℵ ‘ 𝐴 ) ∈ ( ℵ ‘ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		alephord	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ∈ 𝐵 ↔ ( ℵ ‘ 𝐴 ) ≺ ( ℵ ‘ 𝐵 ) ) )
2		alephon	⊢ ( ℵ ‘ 𝐴 ) ∈ On
3		alephon	⊢ ( ℵ ‘ 𝐵 ) ∈ On
4		onenon	⊢ ( ( ℵ ‘ 𝐵 ) ∈ On → ( ℵ ‘ 𝐵 ) ∈ dom card )
5	3 4	ax-mp	⊢ ( ℵ ‘ 𝐵 ) ∈ dom card
6		cardsdomel	⊢ ( ( ( ℵ ‘ 𝐴 ) ∈ On ∧ ( ℵ ‘ 𝐵 ) ∈ dom card ) → ( ( ℵ ‘ 𝐴 ) ≺ ( ℵ ‘ 𝐵 ) ↔ ( ℵ ‘ 𝐴 ) ∈ ( card ‘ ( ℵ ‘ 𝐵 ) ) ) )
7	2 5 6	mp2an	⊢ ( ( ℵ ‘ 𝐴 ) ≺ ( ℵ ‘ 𝐵 ) ↔ ( ℵ ‘ 𝐴 ) ∈ ( card ‘ ( ℵ ‘ 𝐵 ) ) )
8		alephcard	⊢ ( card ‘ ( ℵ ‘ 𝐵 ) ) = ( ℵ ‘ 𝐵 )
9	8	eleq2i	⊢ ( ( ℵ ‘ 𝐴 ) ∈ ( card ‘ ( ℵ ‘ 𝐵 ) ) ↔ ( ℵ ‘ 𝐴 ) ∈ ( ℵ ‘ 𝐵 ) )
10	7 9	bitri	⊢ ( ( ℵ ‘ 𝐴 ) ≺ ( ℵ ‘ 𝐵 ) ↔ ( ℵ ‘ 𝐴 ) ∈ ( ℵ ‘ 𝐵 ) )
11	1 10	bitrdi	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ∈ 𝐵 ↔ ( ℵ ‘ 𝐴 ) ∈ ( ℵ ‘ 𝐵 ) ) )