Metamath Proof Explorer

Theorem alephord

Description: Ordering property of the aleph function. (Contributed by NM, 26-Oct-2003) (Revised by Mario Carneiro, 9-Feb-2013)

Ref Expression
Assertion alephord ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ∈ 𝐵 ↔ ( ℵ ‘ 𝐴 ) ≺ ( ℵ ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 alephordi ⊢ ( 𝐵 ∈ On → ( 𝐴 ∈ 𝐵 → ( ℵ ‘ 𝐴 ) ≺ ( ℵ ‘ 𝐵 ) ) )
2 1 adantl ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ∈ 𝐵 → ( ℵ ‘ 𝐴 ) ≺ ( ℵ ‘ 𝐵 ) ) )
3 brsdom ⊢ ( ( ℵ ‘ 𝐴 ) ≺ ( ℵ ‘ 𝐵 ) ↔ ( ( ℵ ‘ 𝐴 ) ≼ ( ℵ ‘ 𝐵 ) ∧ ¬ ( ℵ ‘ 𝐴 ) ≈ ( ℵ ‘ 𝐵 ) ) )
4 alephon ⊢ ( ℵ ‘ 𝐴 ) ∈ On
5 alephon ⊢ ( ℵ ‘ 𝐵 ) ∈ On
6 domtriord ⊢ ( ( ( ℵ ‘ 𝐴 ) ∈ On ∧ ( ℵ ‘ 𝐵 ) ∈ On ) → ( ( ℵ ‘ 𝐴 ) ≼ ( ℵ ‘ 𝐵 ) ↔ ¬ ( ℵ ‘ 𝐵 ) ≺ ( ℵ ‘ 𝐴 ) ) )
7 4 5 6 mp2an ⊢ ( ( ℵ ‘ 𝐴 ) ≼ ( ℵ ‘ 𝐵 ) ↔ ¬ ( ℵ ‘ 𝐵 ) ≺ ( ℵ ‘ 𝐴 ) )
8 alephordi ⊢ ( 𝐴 ∈ On → ( 𝐵 ∈ 𝐴 → ( ℵ ‘ 𝐵 ) ≺ ( ℵ ‘ 𝐴 ) ) )
9 8 con3d ⊢ ( 𝐴 ∈ On → ( ¬ ( ℵ ‘ 𝐵 ) ≺ ( ℵ ‘ 𝐴 ) → ¬ 𝐵 ∈ 𝐴 ) )
10 7 9 biimtrid ⊢ ( 𝐴 ∈ On → ( ( ℵ ‘ 𝐴 ) ≼ ( ℵ ‘ 𝐵 ) → ¬ 𝐵 ∈ 𝐴 ) )
11 10 adantr ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( ℵ ‘ 𝐴 ) ≼ ( ℵ ‘ 𝐵 ) → ¬ 𝐵 ∈ 𝐴 ) )
12 ontri1 ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ⊆ 𝐵 ↔ ¬ 𝐵 ∈ 𝐴 ) )
13 11 12 sylibrd ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( ℵ ‘ 𝐴 ) ≼ ( ℵ ‘ 𝐵 ) → 𝐴 ⊆ 𝐵 ) )
14 fveq2 ⊢ ( 𝐴 = 𝐵 → ( ℵ ‘ 𝐴 ) = ( ℵ ‘ 𝐵 ) )
15 eqeng ⊢ ( ( ℵ ‘ 𝐴 ) ∈ On → ( ( ℵ ‘ 𝐴 ) = ( ℵ ‘ 𝐵 ) → ( ℵ ‘ 𝐴 ) ≈ ( ℵ ‘ 𝐵 ) ) )
16 4 14 15 mpsyl ⊢ ( 𝐴 = 𝐵 → ( ℵ ‘ 𝐴 ) ≈ ( ℵ ‘ 𝐵 ) )
17 16 necon3bi ⊢ ( ¬ ( ℵ ‘ 𝐴 ) ≈ ( ℵ ‘ 𝐵 ) → 𝐴 ≠ 𝐵 )
18 13 17 anim12d1 ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( ( ℵ ‘ 𝐴 ) ≼ ( ℵ ‘ 𝐵 ) ∧ ¬ ( ℵ ‘ 𝐴 ) ≈ ( ℵ ‘ 𝐵 ) ) → ( 𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵 ) ) )
19 onelpss ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ∈ 𝐵 ↔ ( 𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵 ) ) )
20 18 19 sylibrd ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( ( ℵ ‘ 𝐴 ) ≼ ( ℵ ‘ 𝐵 ) ∧ ¬ ( ℵ ‘ 𝐴 ) ≈ ( ℵ ‘ 𝐵 ) ) → 𝐴 ∈ 𝐵 ) )
21 3 20 biimtrid ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( ℵ ‘ 𝐴 ) ≺ ( ℵ ‘ 𝐵 ) → 𝐴 ∈ 𝐵 ) )
22 2 21 impbid ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ∈ 𝐵 ↔ ( ℵ ‘ 𝐴 ) ≺ ( ℵ ‘ 𝐵 ) ) )