Metamath Proof Explorer


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 ) → ( 𝐴𝐵 ↔ ( ℵ ‘ 𝐴 ) ∈ ( ℵ ‘ 𝐵 ) ) )