This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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