Metamath Proof Explorer

Theorem alephnbtwn2

Description: No set has equinumerosity between an aleph and its successor aleph. (Contributed by NM, 3-Nov-2003) (Revised by Mario Carneiro, 2-Feb-2013)

Ref Expression
Assertion alephnbtwn2 ¬ ( ( ℵ ‘ 𝐴 ) ≺ 𝐵 ∧ 𝐵 ≺ ( ℵ ‘ suc 𝐴 ) )

Proof

Step Hyp Ref Expression
1 cardidm ⊢ ( card ‘ ( card ‘ 𝐵 ) ) = ( card ‘ 𝐵 )
2 alephnbtwn ⊢ ( ( card ‘ ( card ‘ 𝐵 ) ) = ( card ‘ 𝐵 ) → ¬ ( ( ℵ ‘ 𝐴 ) ∈ ( card ‘ 𝐵 ) ∧ ( card ‘ 𝐵 ) ∈ ( ℵ ‘ suc 𝐴 ) ) )
3 1 2 ax-mp ⊢ ¬ ( ( ℵ ‘ 𝐴 ) ∈ ( card ‘ 𝐵 ) ∧ ( card ‘ 𝐵 ) ∈ ( ℵ ‘ suc 𝐴 ) )
4 alephon ⊢ ( ℵ ‘ suc 𝐴 ) ∈ On
5 sdomdom ⊢ ( 𝐵 ≺ ( ℵ ‘ suc 𝐴 ) → 𝐵 ≼ ( ℵ ‘ suc 𝐴 ) )
6 ondomen ⊢ ( ( ( ℵ ‘ suc 𝐴 ) ∈ On ∧ 𝐵 ≼ ( ℵ ‘ suc 𝐴 ) ) → 𝐵 ∈ dom card )
7 4 5 6 sylancr ⊢ ( 𝐵 ≺ ( ℵ ‘ suc 𝐴 ) → 𝐵 ∈ dom card )
8 cardid2 ⊢ ( 𝐵 ∈ dom card → ( card ‘ 𝐵 ) ≈ 𝐵 )
9 7 8 syl ⊢ ( 𝐵 ≺ ( ℵ ‘ suc 𝐴 ) → ( card ‘ 𝐵 ) ≈ 𝐵 )
10 9 ensymd ⊢ ( 𝐵 ≺ ( ℵ ‘ suc 𝐴 ) → 𝐵 ≈ ( card ‘ 𝐵 ) )
11 sdomentr ⊢ ( ( ( ℵ ‘ 𝐴 ) ≺ 𝐵 ∧ 𝐵 ≈ ( card ‘ 𝐵 ) ) → ( ℵ ‘ 𝐴 ) ≺ ( card ‘ 𝐵 ) )
12 10 11 sylan2 ⊢ ( ( ( ℵ ‘ 𝐴 ) ≺ 𝐵 ∧ 𝐵 ≺ ( ℵ ‘ suc 𝐴 ) ) → ( ℵ ‘ 𝐴 ) ≺ ( card ‘ 𝐵 ) )
13 alephon ⊢ ( ℵ ‘ 𝐴 ) ∈ On
14 cardon ⊢ ( card ‘ 𝐵 ) ∈ On
15 onenon ⊢ ( ( card ‘ 𝐵 ) ∈ On → ( card ‘ 𝐵 ) ∈ dom card )
16 14 15 ax-mp ⊢ ( card ‘ 𝐵 ) ∈ dom card
17 cardsdomel ⊢ ( ( ( ℵ ‘ 𝐴 ) ∈ On ∧ ( card ‘ 𝐵 ) ∈ dom card ) → ( ( ℵ ‘ 𝐴 ) ≺ ( card ‘ 𝐵 ) ↔ ( ℵ ‘ 𝐴 ) ∈ ( card ‘ ( card ‘ 𝐵 ) ) ) )
18 13 16 17 mp2an ⊢ ( ( ℵ ‘ 𝐴 ) ≺ ( card ‘ 𝐵 ) ↔ ( ℵ ‘ 𝐴 ) ∈ ( card ‘ ( card ‘ 𝐵 ) ) )
19 1 eleq2i ⊢ ( ( ℵ ‘ 𝐴 ) ∈ ( card ‘ ( card ‘ 𝐵 ) ) ↔ ( ℵ ‘ 𝐴 ) ∈ ( card ‘ 𝐵 ) )
20 18 19 bitri ⊢ ( ( ℵ ‘ 𝐴 ) ≺ ( card ‘ 𝐵 ) ↔ ( ℵ ‘ 𝐴 ) ∈ ( card ‘ 𝐵 ) )
21 12 20 sylib ⊢ ( ( ( ℵ ‘ 𝐴 ) ≺ 𝐵 ∧ 𝐵 ≺ ( ℵ ‘ suc 𝐴 ) ) → ( ℵ ‘ 𝐴 ) ∈ ( card ‘ 𝐵 ) )
22 ensdomtr ⊢ ( ( ( card ‘ 𝐵 ) ≈ 𝐵 ∧ 𝐵 ≺ ( ℵ ‘ suc 𝐴 ) ) → ( card ‘ 𝐵 ) ≺ ( ℵ ‘ suc 𝐴 ) )
23 9 22 mpancom ⊢ ( 𝐵 ≺ ( ℵ ‘ suc 𝐴 ) → ( card ‘ 𝐵 ) ≺ ( ℵ ‘ suc 𝐴 ) )
24 23 adantl ⊢ ( ( ( ℵ ‘ 𝐴 ) ≺ 𝐵 ∧ 𝐵 ≺ ( ℵ ‘ suc 𝐴 ) ) → ( card ‘ 𝐵 ) ≺ ( ℵ ‘ suc 𝐴 ) )
25 onenon ⊢ ( ( ℵ ‘ suc 𝐴 ) ∈ On → ( ℵ ‘ suc 𝐴 ) ∈ dom card )
26 4 25 ax-mp ⊢ ( ℵ ‘ suc 𝐴 ) ∈ dom card
27 cardsdomel ⊢ ( ( ( card ‘ 𝐵 ) ∈ On ∧ ( ℵ ‘ suc 𝐴 ) ∈ dom card ) → ( ( card ‘ 𝐵 ) ≺ ( ℵ ‘ suc 𝐴 ) ↔ ( card ‘ 𝐵 ) ∈ ( card ‘ ( ℵ ‘ suc 𝐴 ) ) ) )
28 14 26 27 mp2an ⊢ ( ( card ‘ 𝐵 ) ≺ ( ℵ ‘ suc 𝐴 ) ↔ ( card ‘ 𝐵 ) ∈ ( card ‘ ( ℵ ‘ suc 𝐴 ) ) )
29 alephcard ⊢ ( card ‘ ( ℵ ‘ suc 𝐴 ) ) = ( ℵ ‘ suc 𝐴 )
30 29 eleq2i ⊢ ( ( card ‘ 𝐵 ) ∈ ( card ‘ ( ℵ ‘ suc 𝐴 ) ) ↔ ( card ‘ 𝐵 ) ∈ ( ℵ ‘ suc 𝐴 ) )
31 28 30 bitri ⊢ ( ( card ‘ 𝐵 ) ≺ ( ℵ ‘ suc 𝐴 ) ↔ ( card ‘ 𝐵 ) ∈ ( ℵ ‘ suc 𝐴 ) )
32 24 31 sylib ⊢ ( ( ( ℵ ‘ 𝐴 ) ≺ 𝐵 ∧ 𝐵 ≺ ( ℵ ‘ suc 𝐴 ) ) → ( card ‘ 𝐵 ) ∈ ( ℵ ‘ suc 𝐴 ) )
33 21 32 jca ⊢ ( ( ( ℵ ‘ 𝐴 ) ≺ 𝐵 ∧ 𝐵 ≺ ( ℵ ‘ suc 𝐴 ) ) → ( ( ℵ ‘ 𝐴 ) ∈ ( card ‘ 𝐵 ) ∧ ( card ‘ 𝐵 ) ∈ ( ℵ ‘ suc 𝐴 ) ) )
34 3 33 mto ⊢ ¬ ( ( ℵ ‘ 𝐴 ) ≺ 𝐵 ∧ 𝐵 ≺ ( ℵ ‘ suc 𝐴 ) )