Step | Hyp | Ref
| Expression |
1 | | alephordi 8897 |
. . . . . 6
⊢ (𝐴 ∈ On → (𝑦 ∈ 𝐴 → (ℵ‘𝑦) ≺ (ℵ‘𝐴))) |
2 | 1 | ralrimiv 2965 |
. . . . 5
⊢ (𝐴 ∈ On → ∀𝑦 ∈ 𝐴 (ℵ‘𝑦) ≺ (ℵ‘𝐴)) |
3 | | alephon 8892 |
. . . . 5
⊢
(ℵ‘𝐴)
∈ On |
4 | 2, 3 | jctil 560 |
. . . 4
⊢ (𝐴 ∈ On →
((ℵ‘𝐴) ∈
On ∧ ∀𝑦 ∈
𝐴 (ℵ‘𝑦) ≺ (ℵ‘𝐴))) |
5 | | breq2 4657 |
. . . . . 6
⊢ (𝑥 = (ℵ‘𝐴) → ((ℵ‘𝑦) ≺ 𝑥 ↔ (ℵ‘𝑦) ≺ (ℵ‘𝐴))) |
6 | 5 | ralbidv 2986 |
. . . . 5
⊢ (𝑥 = (ℵ‘𝐴) → (∀𝑦 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑥 ↔ ∀𝑦 ∈ 𝐴 (ℵ‘𝑦) ≺ (ℵ‘𝐴))) |
7 | 6 | elrab 3363 |
. . . 4
⊢
((ℵ‘𝐴)
∈ {𝑥 ∈ On ∣
∀𝑦 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑥} ↔ ((ℵ‘𝐴) ∈ On ∧ ∀𝑦 ∈ 𝐴 (ℵ‘𝑦) ≺ (ℵ‘𝐴))) |
8 | 4, 7 | sylibr 224 |
. . 3
⊢ (𝐴 ∈ On →
(ℵ‘𝐴) ∈
{𝑥 ∈ On ∣
∀𝑦 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑥}) |
9 | 8 | adantr 481 |
. 2
⊢ ((𝐴 ∈ On ∧ ∅ ∈
𝐴) →
(ℵ‘𝐴) ∈
{𝑥 ∈ On ∣
∀𝑦 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑥}) |
10 | | cardsdomelir 8799 |
. . . . 5
⊢ (𝑧 ∈
(card‘(ℵ‘𝐴)) → 𝑧 ≺ (ℵ‘𝐴)) |
11 | | alephcard 8893 |
. . . . . 6
⊢
(card‘(ℵ‘𝐴)) = (ℵ‘𝐴) |
12 | 11 | eqcomi 2631 |
. . . . 5
⊢
(ℵ‘𝐴) =
(card‘(ℵ‘𝐴)) |
13 | 10, 12 | eleq2s 2719 |
. . . 4
⊢ (𝑧 ∈ (ℵ‘𝐴) → 𝑧 ≺ (ℵ‘𝐴)) |
14 | | omex 8540 |
. . . . . 6
⊢ ω
∈ V |
15 | | vex 3203 |
. . . . . 6
⊢ 𝑧 ∈ V |
16 | | entri3 9381 |
. . . . . 6
⊢ ((ω
∈ V ∧ 𝑧 ∈ V)
→ (ω ≼ 𝑧
∨ 𝑧 ≼
ω)) |
17 | 14, 15, 16 | mp2an 708 |
. . . . 5
⊢ (ω
≼ 𝑧 ∨ 𝑧 ≼
ω) |
18 | | carddom 9376 |
. . . . . . . . . 10
⊢ ((ω
∈ V ∧ 𝑧 ∈ V)
→ ((card‘ω) ⊆ (card‘𝑧) ↔ ω ≼ 𝑧)) |
19 | 14, 15, 18 | mp2an 708 |
. . . . . . . . 9
⊢
((card‘ω) ⊆ (card‘𝑧) ↔ ω ≼ 𝑧) |
20 | | cardom 8812 |
. . . . . . . . . 10
⊢
(card‘ω) = ω |
21 | 20 | sseq1i 3629 |
. . . . . . . . 9
⊢
((card‘ω) ⊆ (card‘𝑧) ↔ ω ⊆ (card‘𝑧)) |
22 | 19, 21 | bitr3i 266 |
. . . . . . . 8
⊢ (ω
≼ 𝑧 ↔ ω
⊆ (card‘𝑧)) |
23 | | cardidm 8785 |
. . . . . . . . . 10
⊢
(card‘(card‘𝑧)) = (card‘𝑧) |
24 | | cardalephex 8913 |
. . . . . . . . . 10
⊢ (ω
⊆ (card‘𝑧)
→ ((card‘(card‘𝑧)) = (card‘𝑧) ↔ ∃𝑥 ∈ On (card‘𝑧) = (ℵ‘𝑥))) |
25 | 23, 24 | mpbii 223 |
. . . . . . . . 9
⊢ (ω
⊆ (card‘𝑧)
→ ∃𝑥 ∈ On
(card‘𝑧) =
(ℵ‘𝑥)) |
26 | | alephord 8898 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ On ∧ 𝐴 ∈ On) → (𝑥 ∈ 𝐴 ↔ (ℵ‘𝑥) ≺ (ℵ‘𝐴))) |
27 | 26 | ancoms 469 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ On) → (𝑥 ∈ 𝐴 ↔ (ℵ‘𝑥) ≺ (ℵ‘𝐴))) |
28 | 15 | cardid 9369 |
. . . . . . . . . . . . . . 15
⊢
(card‘𝑧)
≈ 𝑧 |
29 | | sdomen1 8104 |
. . . . . . . . . . . . . . 15
⊢
((card‘𝑧)
≈ 𝑧 →
((card‘𝑧) ≺
(ℵ‘𝐴) ↔
𝑧 ≺
(ℵ‘𝐴))) |
30 | 28, 29 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢
((card‘𝑧)
≺ (ℵ‘𝐴)
↔ 𝑧 ≺
(ℵ‘𝐴)) |
31 | | breq1 4656 |
. . . . . . . . . . . . . 14
⊢
((card‘𝑧) =
(ℵ‘𝑥) →
((card‘𝑧) ≺
(ℵ‘𝐴) ↔
(ℵ‘𝑥) ≺
(ℵ‘𝐴))) |
32 | 30, 31 | syl5rbbr 275 |
. . . . . . . . . . . . 13
⊢
((card‘𝑧) =
(ℵ‘𝑥) →
((ℵ‘𝑥) ≺
(ℵ‘𝐴) ↔
𝑧 ≺
(ℵ‘𝐴))) |
33 | 27, 32 | sylan9bb 736 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ On ∧ 𝑥 ∈ On) ∧
(card‘𝑧) =
(ℵ‘𝑥)) →
(𝑥 ∈ 𝐴 ↔ 𝑧 ≺ (ℵ‘𝐴))) |
34 | | fveq2 6191 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑥 → (ℵ‘𝑦) = (ℵ‘𝑥)) |
35 | 34 | breq1d 4663 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑥 → ((ℵ‘𝑦) ≺ 𝑧 ↔ (ℵ‘𝑥) ≺ 𝑧)) |
36 | 35 | rspcv 3305 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ 𝐴 → (∀𝑦 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑧 → (ℵ‘𝑥) ≺ 𝑧)) |
37 | | sdomirr 8097 |
. . . . . . . . . . . . . . . 16
⊢ ¬
(ℵ‘𝑥) ≺
(ℵ‘𝑥) |
38 | | sdomen2 8105 |
. . . . . . . . . . . . . . . . . 18
⊢
((card‘𝑧)
≈ 𝑧 →
((ℵ‘𝑥) ≺
(card‘𝑧) ↔
(ℵ‘𝑥) ≺
𝑧)) |
39 | 28, 38 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢
((ℵ‘𝑥)
≺ (card‘𝑧)
↔ (ℵ‘𝑥)
≺ 𝑧) |
40 | | breq2 4657 |
. . . . . . . . . . . . . . . . 17
⊢
((card‘𝑧) =
(ℵ‘𝑥) →
((ℵ‘𝑥) ≺
(card‘𝑧) ↔
(ℵ‘𝑥) ≺
(ℵ‘𝑥))) |
41 | 39, 40 | syl5bbr 274 |
. . . . . . . . . . . . . . . 16
⊢
((card‘𝑧) =
(ℵ‘𝑥) →
((ℵ‘𝑥) ≺
𝑧 ↔
(ℵ‘𝑥) ≺
(ℵ‘𝑥))) |
42 | 37, 41 | mtbiri 317 |
. . . . . . . . . . . . . . 15
⊢
((card‘𝑧) =
(ℵ‘𝑥) →
¬ (ℵ‘𝑥)
≺ 𝑧) |
43 | 36, 42 | nsyli 155 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝐴 → ((card‘𝑧) = (ℵ‘𝑥) → ¬ ∀𝑦 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑧)) |
44 | 43 | com12 32 |
. . . . . . . . . . . . 13
⊢
((card‘𝑧) =
(ℵ‘𝑥) →
(𝑥 ∈ 𝐴 → ¬ ∀𝑦 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑧)) |
45 | 44 | adantl 482 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ On ∧ 𝑥 ∈ On) ∧
(card‘𝑧) =
(ℵ‘𝑥)) →
(𝑥 ∈ 𝐴 → ¬ ∀𝑦 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑧)) |
46 | 33, 45 | sylbird 250 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ On ∧ 𝑥 ∈ On) ∧
(card‘𝑧) =
(ℵ‘𝑥)) →
(𝑧 ≺
(ℵ‘𝐴) →
¬ ∀𝑦 ∈
𝐴 (ℵ‘𝑦) ≺ 𝑧)) |
47 | 46 | exp31 630 |
. . . . . . . . . 10
⊢ (𝐴 ∈ On → (𝑥 ∈ On →
((card‘𝑧) =
(ℵ‘𝑥) →
(𝑧 ≺
(ℵ‘𝐴) →
¬ ∀𝑦 ∈
𝐴 (ℵ‘𝑦) ≺ 𝑧)))) |
48 | 47 | rexlimdv 3030 |
. . . . . . . . 9
⊢ (𝐴 ∈ On → (∃𝑥 ∈ On (card‘𝑧) = (ℵ‘𝑥) → (𝑧 ≺ (ℵ‘𝐴) → ¬ ∀𝑦 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑧))) |
49 | 25, 48 | syl5 34 |
. . . . . . . 8
⊢ (𝐴 ∈ On → (ω
⊆ (card‘𝑧)
→ (𝑧 ≺
(ℵ‘𝐴) →
¬ ∀𝑦 ∈
𝐴 (ℵ‘𝑦) ≺ 𝑧))) |
50 | 22, 49 | syl5bi 232 |
. . . . . . 7
⊢ (𝐴 ∈ On → (ω
≼ 𝑧 → (𝑧 ≺ (ℵ‘𝐴) → ¬ ∀𝑦 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑧))) |
51 | 50 | adantr 481 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ ∅ ∈
𝐴) → (ω ≼
𝑧 → (𝑧 ≺ (ℵ‘𝐴) → ¬ ∀𝑦 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑧))) |
52 | | ne0i 3921 |
. . . . . . . . . . . 12
⊢ (∅
∈ 𝐴 → 𝐴 ≠ ∅) |
53 | | onelon 5748 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ On ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ On) |
54 | | alephgeom 8905 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ On ↔ ω
⊆ (ℵ‘𝑦)) |
55 | | alephon 8892 |
. . . . . . . . . . . . . . . . . . 19
⊢
(ℵ‘𝑦)
∈ On |
56 | | ssdomg 8001 |
. . . . . . . . . . . . . . . . . . 19
⊢
((ℵ‘𝑦)
∈ On → (ω ⊆ (ℵ‘𝑦) → ω ≼ (ℵ‘𝑦))) |
57 | 55, 56 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
⊢ (ω
⊆ (ℵ‘𝑦)
→ ω ≼ (ℵ‘𝑦)) |
58 | 54, 57 | sylbi 207 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ On → ω
≼ (ℵ‘𝑦)) |
59 | | domtr 8009 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑧 ≼ ω ∧ ω
≼ (ℵ‘𝑦))
→ 𝑧 ≼
(ℵ‘𝑦)) |
60 | 58, 59 | sylan2 491 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑧 ≼ ω ∧ 𝑦 ∈ On) → 𝑧 ≼ (ℵ‘𝑦)) |
61 | | domnsym 8086 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ≼ (ℵ‘𝑦) → ¬
(ℵ‘𝑦) ≺
𝑧) |
62 | 60, 61 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝑧 ≼ ω ∧ 𝑦 ∈ On) → ¬
(ℵ‘𝑦) ≺
𝑧) |
63 | 53, 62 | sylan2 491 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ≼ ω ∧ (𝐴 ∈ On ∧ 𝑦 ∈ 𝐴)) → ¬ (ℵ‘𝑦) ≺ 𝑧) |
64 | 63 | expr 643 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ≼ ω ∧ 𝐴 ∈ On) → (𝑦 ∈ 𝐴 → ¬ (ℵ‘𝑦) ≺ 𝑧)) |
65 | 64 | ralrimiv 2965 |
. . . . . . . . . . . 12
⊢ ((𝑧 ≼ ω ∧ 𝐴 ∈ On) → ∀𝑦 ∈ 𝐴 ¬ (ℵ‘𝑦) ≺ 𝑧) |
66 | | r19.2z 4060 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ≠ ∅ ∧
∀𝑦 ∈ 𝐴 ¬ (ℵ‘𝑦) ≺ 𝑧) → ∃𝑦 ∈ 𝐴 ¬ (ℵ‘𝑦) ≺ 𝑧) |
67 | 66 | ex 450 |
. . . . . . . . . . . 12
⊢ (𝐴 ≠ ∅ →
(∀𝑦 ∈ 𝐴 ¬ (ℵ‘𝑦) ≺ 𝑧 → ∃𝑦 ∈ 𝐴 ¬ (ℵ‘𝑦) ≺ 𝑧)) |
68 | 52, 65, 67 | syl2im 40 |
. . . . . . . . . . 11
⊢ (∅
∈ 𝐴 → ((𝑧 ≼ ω ∧ 𝐴 ∈ On) → ∃𝑦 ∈ 𝐴 ¬ (ℵ‘𝑦) ≺ 𝑧)) |
69 | | rexnal 2995 |
. . . . . . . . . . 11
⊢
(∃𝑦 ∈
𝐴 ¬
(ℵ‘𝑦) ≺
𝑧 ↔ ¬
∀𝑦 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑧) |
70 | 68, 69 | syl6ib 241 |
. . . . . . . . . 10
⊢ (∅
∈ 𝐴 → ((𝑧 ≼ ω ∧ 𝐴 ∈ On) → ¬
∀𝑦 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑧)) |
71 | 70 | com12 32 |
. . . . . . . . 9
⊢ ((𝑧 ≼ ω ∧ 𝐴 ∈ On) → (∅
∈ 𝐴 → ¬
∀𝑦 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑧)) |
72 | 71 | expimpd 629 |
. . . . . . . 8
⊢ (𝑧 ≼ ω → ((𝐴 ∈ On ∧ ∅ ∈
𝐴) → ¬
∀𝑦 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑧)) |
73 | 72 | a1d 25 |
. . . . . . 7
⊢ (𝑧 ≼ ω → (𝑧 ≺ (ℵ‘𝐴) → ((𝐴 ∈ On ∧ ∅ ∈ 𝐴) → ¬ ∀𝑦 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑧))) |
74 | 73 | com3r 87 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ ∅ ∈
𝐴) → (𝑧 ≼ ω → (𝑧 ≺ (ℵ‘𝐴) → ¬ ∀𝑦 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑧))) |
75 | 51, 74 | jaod 395 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ ∅ ∈
𝐴) → ((ω ≼
𝑧 ∨ 𝑧 ≼ ω) → (𝑧 ≺ (ℵ‘𝐴) → ¬ ∀𝑦 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑧))) |
76 | 17, 75 | mpi 20 |
. . . 4
⊢ ((𝐴 ∈ On ∧ ∅ ∈
𝐴) → (𝑧 ≺ (ℵ‘𝐴) → ¬ ∀𝑦 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑧)) |
77 | | breq2 4657 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → ((ℵ‘𝑦) ≺ 𝑥 ↔ (ℵ‘𝑦) ≺ 𝑧)) |
78 | 77 | ralbidv 2986 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → (∀𝑦 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑥 ↔ ∀𝑦 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑧)) |
79 | 78 | elrab 3363 |
. . . . . 6
⊢ (𝑧 ∈ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑥} ↔ (𝑧 ∈ On ∧ ∀𝑦 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑧)) |
80 | 79 | simprbi 480 |
. . . . 5
⊢ (𝑧 ∈ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑥} → ∀𝑦 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑧) |
81 | 80 | con3i 150 |
. . . 4
⊢ (¬
∀𝑦 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑧 → ¬ 𝑧 ∈ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑥}) |
82 | 13, 76, 81 | syl56 36 |
. . 3
⊢ ((𝐴 ∈ On ∧ ∅ ∈
𝐴) → (𝑧 ∈ (ℵ‘𝐴) → ¬ 𝑧 ∈ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑥})) |
83 | 82 | ralrimiv 2965 |
. 2
⊢ ((𝐴 ∈ On ∧ ∅ ∈
𝐴) → ∀𝑧 ∈ (ℵ‘𝐴) ¬ 𝑧 ∈ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑥}) |
84 | | ssrab2 3687 |
. . 3
⊢ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑥} ⊆ On |
85 | | oneqmini 5776 |
. . 3
⊢ ({𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑥} ⊆ On → (((ℵ‘𝐴) ∈ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑥} ∧ ∀𝑧 ∈ (ℵ‘𝐴) ¬ 𝑧 ∈ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑥}) → (ℵ‘𝐴) = ∩ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑥})) |
86 | 84, 85 | ax-mp 5 |
. 2
⊢
(((ℵ‘𝐴)
∈ {𝑥 ∈ On ∣
∀𝑦 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑥} ∧ ∀𝑧 ∈ (ℵ‘𝐴) ¬ 𝑧 ∈ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑥}) → (ℵ‘𝐴) = ∩ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑥}) |
87 | 9, 83, 86 | syl2anc 693 |
1
⊢ ((𝐴 ∈ On ∧ ∅ ∈
𝐴) →
(ℵ‘𝐴) = ∩ {𝑥
∈ On ∣ ∀𝑦
∈ 𝐴
(ℵ‘𝑦) ≺
𝑥}) |