Step | Hyp | Ref
| Expression |
1 | | eldifi 3694 |
. . . 4
⊢ (𝐴 ∈ (On ∖
2𝑜) → 𝐴 ∈ On) |
2 | | limelon 5705 |
. . . 4
⊢ ((𝐵 ∈ 𝐶 ∧ Lim 𝐵) → 𝐵 ∈ On) |
3 | | oecl 7504 |
. . . 4
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ↑𝑜
𝐵) ∈
On) |
4 | 1, 2, 3 | syl2an 493 |
. . 3
⊢ ((𝐴 ∈ (On ∖
2𝑜) ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) → (𝐴 ↑𝑜 𝐵) ∈ On) |
5 | | eloni 5650 |
. . 3
⊢ ((𝐴 ↑𝑜
𝐵) ∈ On → Ord
(𝐴
↑𝑜 𝐵)) |
6 | 4, 5 | syl 17 |
. 2
⊢ ((𝐴 ∈ (On ∖
2𝑜) ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) → Ord (𝐴 ↑𝑜 𝐵)) |
7 | 1 | adantr 480 |
. . 3
⊢ ((𝐴 ∈ (On ∖
2𝑜) ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) → 𝐴 ∈ On) |
8 | 2 | adantl 481 |
. . 3
⊢ ((𝐴 ∈ (On ∖
2𝑜) ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) → 𝐵 ∈ On) |
9 | | dif20el 7472 |
. . . 4
⊢ (𝐴 ∈ (On ∖
2𝑜) → ∅ ∈ 𝐴) |
10 | 9 | adantr 480 |
. . 3
⊢ ((𝐴 ∈ (On ∖
2𝑜) ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) → ∅ ∈ 𝐴) |
11 | | oen0 7553 |
. . 3
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ ∅ ∈
𝐴) → ∅ ∈
(𝐴
↑𝑜 𝐵)) |
12 | 7, 8, 10, 11 | syl21anc 1317 |
. 2
⊢ ((𝐴 ∈ (On ∖
2𝑜) ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) → ∅ ∈ (𝐴 ↑𝑜 𝐵)) |
13 | | oelim2 7562 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) → (𝐴 ↑𝑜 𝐵) = ∪ 𝑦 ∈ (𝐵 ∖ 1𝑜)(𝐴 ↑𝑜
𝑦)) |
14 | 1, 13 | sylan 487 |
. . . . 5
⊢ ((𝐴 ∈ (On ∖
2𝑜) ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) → (𝐴 ↑𝑜 𝐵) = ∪ 𝑦 ∈ (𝐵 ∖ 1𝑜)(𝐴 ↑𝑜
𝑦)) |
15 | 14 | eleq2d 2673 |
. . . 4
⊢ ((𝐴 ∈ (On ∖
2𝑜) ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) → (𝑥 ∈ (𝐴 ↑𝑜 𝐵) ↔ 𝑥 ∈ ∪
𝑦 ∈ (𝐵 ∖ 1𝑜)(𝐴 ↑𝑜
𝑦))) |
16 | | eliun 4460 |
. . . . 5
⊢ (𝑥 ∈ ∪ 𝑦 ∈ (𝐵 ∖ 1𝑜)(𝐴 ↑𝑜
𝑦) ↔ ∃𝑦 ∈ (𝐵 ∖ 1𝑜)𝑥 ∈ (𝐴 ↑𝑜 𝑦)) |
17 | | eldifi 3694 |
. . . . . . 7
⊢ (𝑦 ∈ (𝐵 ∖ 1𝑜) → 𝑦 ∈ 𝐵) |
18 | 7 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ (On ∖
2𝑜) ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ (𝐴 ↑𝑜 𝑦))) → 𝐴 ∈ On) |
19 | 8 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ (On ∖
2𝑜) ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ (𝐴 ↑𝑜 𝑦))) → 𝐵 ∈ On) |
20 | | simprl 790 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ (On ∖
2𝑜) ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ (𝐴 ↑𝑜 𝑦))) → 𝑦 ∈ 𝐵) |
21 | | onelon 5665 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ On ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ On) |
22 | 19, 20, 21 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ (On ∖
2𝑜) ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ (𝐴 ↑𝑜 𝑦))) → 𝑦 ∈ On) |
23 | | oecl 7504 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ On ∧ 𝑦 ∈ On) → (𝐴 ↑𝑜
𝑦) ∈
On) |
24 | 18, 22, 23 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ (On ∖
2𝑜) ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ (𝐴 ↑𝑜 𝑦))) → (𝐴 ↑𝑜 𝑦) ∈ On) |
25 | | eloni 5650 |
. . . . . . . . . . 11
⊢ ((𝐴 ↑𝑜
𝑦) ∈ On → Ord
(𝐴
↑𝑜 𝑦)) |
26 | 24, 25 | syl 17 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ (On ∖
2𝑜) ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ (𝐴 ↑𝑜 𝑦))) → Ord (𝐴 ↑𝑜
𝑦)) |
27 | | simprr 792 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ (On ∖
2𝑜) ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ (𝐴 ↑𝑜 𝑦))) → 𝑥 ∈ (𝐴 ↑𝑜 𝑦)) |
28 | | ordsucss 6910 |
. . . . . . . . . 10
⊢ (Ord
(𝐴
↑𝑜 𝑦) → (𝑥 ∈ (𝐴 ↑𝑜 𝑦) → suc 𝑥 ⊆ (𝐴 ↑𝑜 𝑦))) |
29 | 26, 27, 28 | sylc 63 |
. . . . . . . . 9
⊢ (((𝐴 ∈ (On ∖
2𝑜) ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ (𝐴 ↑𝑜 𝑦))) → suc 𝑥 ⊆ (𝐴 ↑𝑜 𝑦)) |
30 | | simpll 786 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ (On ∖
2𝑜) ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ (𝐴 ↑𝑜 𝑦))) → 𝐴 ∈ (On ∖
2𝑜)) |
31 | | oeordi 7554 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ On ∧ 𝐴 ∈ (On ∖
2𝑜)) → (𝑦 ∈ 𝐵 → (𝐴 ↑𝑜 𝑦) ∈ (𝐴 ↑𝑜 𝐵))) |
32 | 19, 30, 31 | syl2anc 691 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ (On ∖
2𝑜) ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ (𝐴 ↑𝑜 𝑦))) → (𝑦 ∈ 𝐵 → (𝐴 ↑𝑜 𝑦) ∈ (𝐴 ↑𝑜 𝐵))) |
33 | 20, 32 | mpd 15 |
. . . . . . . . 9
⊢ (((𝐴 ∈ (On ∖
2𝑜) ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ (𝐴 ↑𝑜 𝑦))) → (𝐴 ↑𝑜 𝑦) ∈ (𝐴 ↑𝑜 𝐵)) |
34 | | onelon 5665 |
. . . . . . . . . . . 12
⊢ (((𝐴 ↑𝑜
𝑦) ∈ On ∧ 𝑥 ∈ (𝐴 ↑𝑜 𝑦)) → 𝑥 ∈ On) |
35 | 24, 27, 34 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ (On ∖
2𝑜) ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ (𝐴 ↑𝑜 𝑦))) → 𝑥 ∈ On) |
36 | | suceloni 6905 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ On → suc 𝑥 ∈ On) |
37 | 35, 36 | syl 17 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ (On ∖
2𝑜) ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ (𝐴 ↑𝑜 𝑦))) → suc 𝑥 ∈ On) |
38 | 4 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ (On ∖
2𝑜) ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ (𝐴 ↑𝑜 𝑦))) → (𝐴 ↑𝑜 𝐵) ∈ On) |
39 | | ontr2 5689 |
. . . . . . . . . 10
⊢ ((suc
𝑥 ∈ On ∧ (𝐴 ↑𝑜
𝐵) ∈ On) → ((suc
𝑥 ⊆ (𝐴 ↑𝑜
𝑦) ∧ (𝐴 ↑𝑜 𝑦) ∈ (𝐴 ↑𝑜 𝐵)) → suc 𝑥 ∈ (𝐴 ↑𝑜 𝐵))) |
40 | 37, 38, 39 | syl2anc 691 |
. . . . . . . . 9
⊢ (((𝐴 ∈ (On ∖
2𝑜) ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ (𝐴 ↑𝑜 𝑦))) → ((suc 𝑥 ⊆ (𝐴 ↑𝑜 𝑦) ∧ (𝐴 ↑𝑜 𝑦) ∈ (𝐴 ↑𝑜 𝐵)) → suc 𝑥 ∈ (𝐴 ↑𝑜 𝐵))) |
41 | 29, 33, 40 | mp2and 711 |
. . . . . . . 8
⊢ (((𝐴 ∈ (On ∖
2𝑜) ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ (𝐴 ↑𝑜 𝑦))) → suc 𝑥 ∈ (𝐴 ↑𝑜 𝐵)) |
42 | 41 | expr 641 |
. . . . . . 7
⊢ (((𝐴 ∈ (On ∖
2𝑜) ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ 𝑦 ∈ 𝐵) → (𝑥 ∈ (𝐴 ↑𝑜 𝑦) → suc 𝑥 ∈ (𝐴 ↑𝑜 𝐵))) |
43 | 17, 42 | sylan2 490 |
. . . . . 6
⊢ (((𝐴 ∈ (On ∖
2𝑜) ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ 𝑦 ∈ (𝐵 ∖ 1𝑜)) →
(𝑥 ∈ (𝐴 ↑𝑜
𝑦) → suc 𝑥 ∈ (𝐴 ↑𝑜 𝐵))) |
44 | 43 | rexlimdva 3013 |
. . . . 5
⊢ ((𝐴 ∈ (On ∖
2𝑜) ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) → (∃𝑦 ∈ (𝐵 ∖ 1𝑜)𝑥 ∈ (𝐴 ↑𝑜 𝑦) → suc 𝑥 ∈ (𝐴 ↑𝑜 𝐵))) |
45 | 16, 44 | syl5bi 231 |
. . . 4
⊢ ((𝐴 ∈ (On ∖
2𝑜) ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) → (𝑥 ∈ ∪
𝑦 ∈ (𝐵 ∖ 1𝑜)(𝐴 ↑𝑜
𝑦) → suc 𝑥 ∈ (𝐴 ↑𝑜 𝐵))) |
46 | 15, 45 | sylbid 229 |
. . 3
⊢ ((𝐴 ∈ (On ∖
2𝑜) ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) → (𝑥 ∈ (𝐴 ↑𝑜 𝐵) → suc 𝑥 ∈ (𝐴 ↑𝑜 𝐵))) |
47 | 46 | ralrimiv 2948 |
. 2
⊢ ((𝐴 ∈ (On ∖
2𝑜) ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) → ∀𝑥 ∈ (𝐴 ↑𝑜 𝐵)suc 𝑥 ∈ (𝐴 ↑𝑜 𝐵)) |
48 | | dflim4 6940 |
. 2
⊢ (Lim
(𝐴
↑𝑜 𝐵) ↔ (Ord (𝐴 ↑𝑜 𝐵) ∧ ∅ ∈ (𝐴 ↑𝑜
𝐵) ∧ ∀𝑥 ∈ (𝐴 ↑𝑜 𝐵)suc 𝑥 ∈ (𝐴 ↑𝑜 𝐵))) |
49 | 6, 12, 47, 48 | syl3anbrc 1239 |
1
⊢ ((𝐴 ∈ (On ∖
2𝑜) ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) → Lim (𝐴 ↑𝑜 𝐵)) |