Proof of Theorem alephnbtwn2
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | cardidm 9999 | . . 3
⊢
(card‘(card‘𝐵)) = (card‘𝐵) | 
| 2 |  | alephnbtwn 10111 | . . 3
⊢
((card‘(card‘𝐵)) = (card‘𝐵) → ¬ ((ℵ‘𝐴) ∈ (card‘𝐵) ∧ (card‘𝐵) ∈ (ℵ‘suc
𝐴))) | 
| 3 | 1, 2 | ax-mp 5 | . 2
⊢  ¬
((ℵ‘𝐴) ∈
(card‘𝐵) ∧
(card‘𝐵) ∈
(ℵ‘suc 𝐴)) | 
| 4 |  | alephon 10109 | . . . . . . . 8
⊢
(ℵ‘suc 𝐴) ∈ On | 
| 5 |  | sdomdom 9020 | . . . . . . . 8
⊢ (𝐵 ≺ (ℵ‘suc
𝐴) → 𝐵 ≼ (ℵ‘suc 𝐴)) | 
| 6 |  | ondomen 10077 | . . . . . . . 8
⊢
(((ℵ‘suc 𝐴) ∈ On ∧ 𝐵 ≼ (ℵ‘suc 𝐴)) → 𝐵 ∈ dom card) | 
| 7 | 4, 5, 6 | sylancr 587 | . . . . . . 7
⊢ (𝐵 ≺ (ℵ‘suc
𝐴) → 𝐵 ∈ dom card) | 
| 8 |  | cardid2 9993 | . . . . . . 7
⊢ (𝐵 ∈ dom card →
(card‘𝐵) ≈
𝐵) | 
| 9 | 7, 8 | syl 17 | . . . . . 6
⊢ (𝐵 ≺ (ℵ‘suc
𝐴) → (card‘𝐵) ≈ 𝐵) | 
| 10 | 9 | ensymd 9045 | . . . . 5
⊢ (𝐵 ≺ (ℵ‘suc
𝐴) → 𝐵 ≈ (card‘𝐵)) | 
| 11 |  | sdomentr 9151 | . . . . 5
⊢
(((ℵ‘𝐴)
≺ 𝐵 ∧ 𝐵 ≈ (card‘𝐵)) → (ℵ‘𝐴) ≺ (card‘𝐵)) | 
| 12 | 10, 11 | sylan2 593 | . . . 4
⊢
(((ℵ‘𝐴)
≺ 𝐵 ∧ 𝐵 ≺ (ℵ‘suc
𝐴)) →
(ℵ‘𝐴) ≺
(card‘𝐵)) | 
| 13 |  | alephon 10109 | . . . . . 6
⊢
(ℵ‘𝐴)
∈ On | 
| 14 |  | cardon 9984 | . . . . . . 7
⊢
(card‘𝐵)
∈ On | 
| 15 |  | onenon 9989 | . . . . . . 7
⊢
((card‘𝐵)
∈ On → (card‘𝐵) ∈ dom card) | 
| 16 | 14, 15 | ax-mp 5 | . . . . . 6
⊢
(card‘𝐵)
∈ dom card | 
| 17 |  | cardsdomel 10014 | . . . . . 6
⊢
(((ℵ‘𝐴)
∈ On ∧ (card‘𝐵) ∈ dom card) →
((ℵ‘𝐴) ≺
(card‘𝐵) ↔
(ℵ‘𝐴) ∈
(card‘(card‘𝐵)))) | 
| 18 | 13, 16, 17 | mp2an 692 | . . . . 5
⊢
((ℵ‘𝐴)
≺ (card‘𝐵)
↔ (ℵ‘𝐴)
∈ (card‘(card‘𝐵))) | 
| 19 | 1 | eleq2i 2833 | . . . . 5
⊢
((ℵ‘𝐴)
∈ (card‘(card‘𝐵)) ↔ (ℵ‘𝐴) ∈ (card‘𝐵)) | 
| 20 | 18, 19 | bitri 275 | . . . 4
⊢
((ℵ‘𝐴)
≺ (card‘𝐵)
↔ (ℵ‘𝐴)
∈ (card‘𝐵)) | 
| 21 | 12, 20 | sylib 218 | . . 3
⊢
(((ℵ‘𝐴)
≺ 𝐵 ∧ 𝐵 ≺ (ℵ‘suc
𝐴)) →
(ℵ‘𝐴) ∈
(card‘𝐵)) | 
| 22 |  | ensdomtr 9153 | . . . . . 6
⊢
(((card‘𝐵)
≈ 𝐵 ∧ 𝐵 ≺ (ℵ‘suc
𝐴)) →
(card‘𝐵) ≺
(ℵ‘suc 𝐴)) | 
| 23 | 9, 22 | mpancom 688 | . . . . 5
⊢ (𝐵 ≺ (ℵ‘suc
𝐴) → (card‘𝐵) ≺ (ℵ‘suc
𝐴)) | 
| 24 | 23 | adantl 481 | . . . 4
⊢
(((ℵ‘𝐴)
≺ 𝐵 ∧ 𝐵 ≺ (ℵ‘suc
𝐴)) →
(card‘𝐵) ≺
(ℵ‘suc 𝐴)) | 
| 25 |  | onenon 9989 | . . . . . . 7
⊢
((ℵ‘suc 𝐴) ∈ On → (ℵ‘suc 𝐴) ∈ dom
card) | 
| 26 | 4, 25 | ax-mp 5 | . . . . . 6
⊢
(ℵ‘suc 𝐴) ∈ dom card | 
| 27 |  | cardsdomel 10014 | . . . . . 6
⊢
(((card‘𝐵)
∈ On ∧ (ℵ‘suc 𝐴) ∈ dom card) → ((card‘𝐵) ≺ (ℵ‘suc
𝐴) ↔ (card‘𝐵) ∈
(card‘(ℵ‘suc 𝐴)))) | 
| 28 | 14, 26, 27 | mp2an 692 | . . . . 5
⊢
((card‘𝐵)
≺ (ℵ‘suc 𝐴) ↔ (card‘𝐵) ∈ (card‘(ℵ‘suc
𝐴))) | 
| 29 |  | alephcard 10110 | . . . . . 6
⊢
(card‘(ℵ‘suc 𝐴)) = (ℵ‘suc 𝐴) | 
| 30 | 29 | eleq2i 2833 | . . . . 5
⊢
((card‘𝐵)
∈ (card‘(ℵ‘suc 𝐴)) ↔ (card‘𝐵) ∈ (ℵ‘suc 𝐴)) | 
| 31 | 28, 30 | bitri 275 | . . . 4
⊢
((card‘𝐵)
≺ (ℵ‘suc 𝐴) ↔ (card‘𝐵) ∈ (ℵ‘suc 𝐴)) | 
| 32 | 24, 31 | sylib 218 | . . 3
⊢
(((ℵ‘𝐴)
≺ 𝐵 ∧ 𝐵 ≺ (ℵ‘suc
𝐴)) →
(card‘𝐵) ∈
(ℵ‘suc 𝐴)) | 
| 33 | 21, 32 | jca 511 | . 2
⊢
(((ℵ‘𝐴)
≺ 𝐵 ∧ 𝐵 ≺ (ℵ‘suc
𝐴)) →
((ℵ‘𝐴) ∈
(card‘𝐵) ∧
(card‘𝐵) ∈
(ℵ‘suc 𝐴))) | 
| 34 | 3, 33 | mto 197 | 1
⊢  ¬
((ℵ‘𝐴) ≺
𝐵 ∧ 𝐵 ≺ (ℵ‘suc 𝐴)) |