Proof of Theorem alephinit
Step | Hyp | Ref
| Expression |
1 | | isinfcard 9706 |
. . . . 5
⊢ ((ω
⊆ 𝐴 ∧
(card‘𝐴) = 𝐴) ↔ 𝐴 ∈ ran ℵ) |
2 | 1 | bicomi 227 |
. . . 4
⊢ (𝐴 ∈ ran ℵ ↔
(ω ⊆ 𝐴 ∧
(card‘𝐴) = 𝐴)) |
3 | 2 | baib 539 |
. . 3
⊢ (ω
⊆ 𝐴 → (𝐴 ∈ ran ℵ ↔
(card‘𝐴) = 𝐴)) |
4 | 3 | adantl 485 |
. 2
⊢ ((𝐴 ∈ On ∧ ω ⊆
𝐴) → (𝐴 ∈ ran ℵ ↔
(card‘𝐴) = 𝐴)) |
5 | | onenon 9565 |
. . . . . . . 8
⊢ (𝐴 ∈ On → 𝐴 ∈ dom
card) |
6 | 5 | adantr 484 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ ω ⊆
𝐴) → 𝐴 ∈ dom card) |
7 | | onenon 9565 |
. . . . . . 7
⊢ (𝑥 ∈ On → 𝑥 ∈ dom
card) |
8 | | carddom2 9593 |
. . . . . . 7
⊢ ((𝐴 ∈ dom card ∧ 𝑥 ∈ dom card) →
((card‘𝐴) ⊆
(card‘𝑥) ↔ 𝐴 ≼ 𝑥)) |
9 | 6, 7, 8 | syl2an 599 |
. . . . . 6
⊢ (((𝐴 ∈ On ∧ ω ⊆
𝐴) ∧ 𝑥 ∈ On) → ((card‘𝐴) ⊆ (card‘𝑥) ↔ 𝐴 ≼ 𝑥)) |
10 | | cardonle 9573 |
. . . . . . . 8
⊢ (𝑥 ∈ On →
(card‘𝑥) ⊆
𝑥) |
11 | 10 | adantl 485 |
. . . . . . 7
⊢ (((𝐴 ∈ On ∧ ω ⊆
𝐴) ∧ 𝑥 ∈ On) → (card‘𝑥) ⊆ 𝑥) |
12 | | sstr 3909 |
. . . . . . . 8
⊢
(((card‘𝐴)
⊆ (card‘𝑥)
∧ (card‘𝑥)
⊆ 𝑥) →
(card‘𝐴) ⊆
𝑥) |
13 | 12 | expcom 417 |
. . . . . . 7
⊢
((card‘𝑥)
⊆ 𝑥 →
((card‘𝐴) ⊆
(card‘𝑥) →
(card‘𝐴) ⊆
𝑥)) |
14 | 11, 13 | syl 17 |
. . . . . 6
⊢ (((𝐴 ∈ On ∧ ω ⊆
𝐴) ∧ 𝑥 ∈ On) → ((card‘𝐴) ⊆ (card‘𝑥) → (card‘𝐴) ⊆ 𝑥)) |
15 | 9, 14 | sylbird 263 |
. . . . 5
⊢ (((𝐴 ∈ On ∧ ω ⊆
𝐴) ∧ 𝑥 ∈ On) → (𝐴 ≼ 𝑥 → (card‘𝐴) ⊆ 𝑥)) |
16 | | sseq1 3926 |
. . . . . 6
⊢
((card‘𝐴) =
𝐴 → ((card‘𝐴) ⊆ 𝑥 ↔ 𝐴 ⊆ 𝑥)) |
17 | 16 | imbi2d 344 |
. . . . 5
⊢
((card‘𝐴) =
𝐴 → ((𝐴 ≼ 𝑥 → (card‘𝐴) ⊆ 𝑥) ↔ (𝐴 ≼ 𝑥 → 𝐴 ⊆ 𝑥))) |
18 | 15, 17 | syl5ibcom 248 |
. . . 4
⊢ (((𝐴 ∈ On ∧ ω ⊆
𝐴) ∧ 𝑥 ∈ On) → ((card‘𝐴) = 𝐴 → (𝐴 ≼ 𝑥 → 𝐴 ⊆ 𝑥))) |
19 | 18 | ralrimdva 3110 |
. . 3
⊢ ((𝐴 ∈ On ∧ ω ⊆
𝐴) →
((card‘𝐴) = 𝐴 → ∀𝑥 ∈ On (𝐴 ≼ 𝑥 → 𝐴 ⊆ 𝑥))) |
20 | | oncardid 9572 |
. . . . . . 7
⊢ (𝐴 ∈ On →
(card‘𝐴) ≈
𝐴) |
21 | | ensym 8677 |
. . . . . . 7
⊢
((card‘𝐴)
≈ 𝐴 → 𝐴 ≈ (card‘𝐴)) |
22 | | endom 8655 |
. . . . . . 7
⊢ (𝐴 ≈ (card‘𝐴) → 𝐴 ≼ (card‘𝐴)) |
23 | 20, 21, 22 | 3syl 18 |
. . . . . 6
⊢ (𝐴 ∈ On → 𝐴 ≼ (card‘𝐴)) |
24 | 23 | adantr 484 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ ω ⊆
𝐴) → 𝐴 ≼ (card‘𝐴)) |
25 | | cardon 9560 |
. . . . . 6
⊢
(card‘𝐴)
∈ On |
26 | | breq2 5057 |
. . . . . . . 8
⊢ (𝑥 = (card‘𝐴) → (𝐴 ≼ 𝑥 ↔ 𝐴 ≼ (card‘𝐴))) |
27 | | sseq2 3927 |
. . . . . . . 8
⊢ (𝑥 = (card‘𝐴) → (𝐴 ⊆ 𝑥 ↔ 𝐴 ⊆ (card‘𝐴))) |
28 | 26, 27 | imbi12d 348 |
. . . . . . 7
⊢ (𝑥 = (card‘𝐴) → ((𝐴 ≼ 𝑥 → 𝐴 ⊆ 𝑥) ↔ (𝐴 ≼ (card‘𝐴) → 𝐴 ⊆ (card‘𝐴)))) |
29 | 28 | rspcv 3532 |
. . . . . 6
⊢
((card‘𝐴)
∈ On → (∀𝑥
∈ On (𝐴 ≼ 𝑥 → 𝐴 ⊆ 𝑥) → (𝐴 ≼ (card‘𝐴) → 𝐴 ⊆ (card‘𝐴)))) |
30 | 25, 29 | ax-mp 5 |
. . . . 5
⊢
(∀𝑥 ∈ On
(𝐴 ≼ 𝑥 → 𝐴 ⊆ 𝑥) → (𝐴 ≼ (card‘𝐴) → 𝐴 ⊆ (card‘𝐴))) |
31 | 24, 30 | syl5com 31 |
. . . 4
⊢ ((𝐴 ∈ On ∧ ω ⊆
𝐴) → (∀𝑥 ∈ On (𝐴 ≼ 𝑥 → 𝐴 ⊆ 𝑥) → 𝐴 ⊆ (card‘𝐴))) |
32 | | cardonle 9573 |
. . . . . . 7
⊢ (𝐴 ∈ On →
(card‘𝐴) ⊆
𝐴) |
33 | 32 | adantr 484 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ ω ⊆
𝐴) → (card‘𝐴) ⊆ 𝐴) |
34 | 33 | biantrurd 536 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ ω ⊆
𝐴) → (𝐴 ⊆ (card‘𝐴) ↔ ((card‘𝐴) ⊆ 𝐴 ∧ 𝐴 ⊆ (card‘𝐴)))) |
35 | | eqss 3916 |
. . . . 5
⊢
((card‘𝐴) =
𝐴 ↔ ((card‘𝐴) ⊆ 𝐴 ∧ 𝐴 ⊆ (card‘𝐴))) |
36 | 34, 35 | bitr4di 292 |
. . . 4
⊢ ((𝐴 ∈ On ∧ ω ⊆
𝐴) → (𝐴 ⊆ (card‘𝐴) ↔ (card‘𝐴) = 𝐴)) |
37 | 31, 36 | sylibd 242 |
. . 3
⊢ ((𝐴 ∈ On ∧ ω ⊆
𝐴) → (∀𝑥 ∈ On (𝐴 ≼ 𝑥 → 𝐴 ⊆ 𝑥) → (card‘𝐴) = 𝐴)) |
38 | 19, 37 | impbid 215 |
. 2
⊢ ((𝐴 ∈ On ∧ ω ⊆
𝐴) →
((card‘𝐴) = 𝐴 ↔ ∀𝑥 ∈ On (𝐴 ≼ 𝑥 → 𝐴 ⊆ 𝑥))) |
39 | 4, 38 | bitrd 282 |
1
⊢ ((𝐴 ∈ On ∧ ω ⊆
𝐴) → (𝐴 ∈ ran ℵ ↔
∀𝑥 ∈ On (𝐴 ≼ 𝑥 → 𝐴 ⊆ 𝑥))) |