Step | Hyp | Ref
| Expression |
1 | | id 22 |
. . . 4
⊢ (𝑥 = ∅ → 𝑥 = ∅) |
2 | | oveq2 6557 |
. . . 4
⊢ (𝑥 = ∅ → (𝐴 ↑𝑜
𝑥) = (𝐴 ↑𝑜
∅)) |
3 | 1, 2 | sseq12d 3597 |
. . 3
⊢ (𝑥 = ∅ → (𝑥 ⊆ (𝐴 ↑𝑜 𝑥) ↔ ∅ ⊆ (𝐴 ↑𝑜
∅))) |
4 | | id 22 |
. . . 4
⊢ (𝑥 = 𝑦 → 𝑥 = 𝑦) |
5 | | oveq2 6557 |
. . . 4
⊢ (𝑥 = 𝑦 → (𝐴 ↑𝑜 𝑥) = (𝐴 ↑𝑜 𝑦)) |
6 | 4, 5 | sseq12d 3597 |
. . 3
⊢ (𝑥 = 𝑦 → (𝑥 ⊆ (𝐴 ↑𝑜 𝑥) ↔ 𝑦 ⊆ (𝐴 ↑𝑜 𝑦))) |
7 | | id 22 |
. . . 4
⊢ (𝑥 = suc 𝑦 → 𝑥 = suc 𝑦) |
8 | | oveq2 6557 |
. . . 4
⊢ (𝑥 = suc 𝑦 → (𝐴 ↑𝑜 𝑥) = (𝐴 ↑𝑜 suc 𝑦)) |
9 | 7, 8 | sseq12d 3597 |
. . 3
⊢ (𝑥 = suc 𝑦 → (𝑥 ⊆ (𝐴 ↑𝑜 𝑥) ↔ suc 𝑦 ⊆ (𝐴 ↑𝑜 suc 𝑦))) |
10 | | id 22 |
. . . 4
⊢ (𝑥 = 𝐵 → 𝑥 = 𝐵) |
11 | | oveq2 6557 |
. . . 4
⊢ (𝑥 = 𝐵 → (𝐴 ↑𝑜 𝑥) = (𝐴 ↑𝑜 𝐵)) |
12 | 10, 11 | sseq12d 3597 |
. . 3
⊢ (𝑥 = 𝐵 → (𝑥 ⊆ (𝐴 ↑𝑜 𝑥) ↔ 𝐵 ⊆ (𝐴 ↑𝑜 𝐵))) |
13 | | 0ss 3924 |
. . . 4
⊢ ∅
⊆ (𝐴
↑𝑜 ∅) |
14 | 13 | a1i 11 |
. . 3
⊢ (𝐴 ∈ (On ∖
2𝑜) → ∅ ⊆ (𝐴 ↑𝑜
∅)) |
15 | | eloni 5650 |
. . . . . . 7
⊢ (𝑦 ∈ On → Ord 𝑦) |
16 | 15 | adantl 481 |
. . . . . 6
⊢ ((𝐴 ∈ (On ∖
2𝑜) ∧ 𝑦 ∈ On) → Ord 𝑦) |
17 | | eldifi 3694 |
. . . . . . . 8
⊢ (𝐴 ∈ (On ∖
2𝑜) → 𝐴 ∈ On) |
18 | | oecl 7504 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧ 𝑦 ∈ On) → (𝐴 ↑𝑜
𝑦) ∈
On) |
19 | 17, 18 | sylan 487 |
. . . . . . 7
⊢ ((𝐴 ∈ (On ∖
2𝑜) ∧ 𝑦 ∈ On) → (𝐴 ↑𝑜 𝑦) ∈ On) |
20 | | eloni 5650 |
. . . . . . 7
⊢ ((𝐴 ↑𝑜
𝑦) ∈ On → Ord
(𝐴
↑𝑜 𝑦)) |
21 | 19, 20 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ (On ∖
2𝑜) ∧ 𝑦 ∈ On) → Ord (𝐴 ↑𝑜 𝑦)) |
22 | | ordsucsssuc 6915 |
. . . . . 6
⊢ ((Ord
𝑦 ∧ Ord (𝐴 ↑𝑜
𝑦)) → (𝑦 ⊆ (𝐴 ↑𝑜 𝑦) ↔ suc 𝑦 ⊆ suc (𝐴 ↑𝑜 𝑦))) |
23 | 16, 21, 22 | syl2anc 691 |
. . . . 5
⊢ ((𝐴 ∈ (On ∖
2𝑜) ∧ 𝑦 ∈ On) → (𝑦 ⊆ (𝐴 ↑𝑜 𝑦) ↔ suc 𝑦 ⊆ suc (𝐴 ↑𝑜 𝑦))) |
24 | | suceloni 6905 |
. . . . . . . . 9
⊢ (𝑦 ∈ On → suc 𝑦 ∈ On) |
25 | | oecl 7504 |
. . . . . . . . 9
⊢ ((𝐴 ∈ On ∧ suc 𝑦 ∈ On) → (𝐴 ↑𝑜 suc
𝑦) ∈
On) |
26 | 17, 24, 25 | syl2an 493 |
. . . . . . . 8
⊢ ((𝐴 ∈ (On ∖
2𝑜) ∧ 𝑦 ∈ On) → (𝐴 ↑𝑜 suc 𝑦) ∈ On) |
27 | | eloni 5650 |
. . . . . . . 8
⊢ ((𝐴 ↑𝑜 suc
𝑦) ∈ On → Ord
(𝐴
↑𝑜 suc 𝑦)) |
28 | 26, 27 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ (On ∖
2𝑜) ∧ 𝑦 ∈ On) → Ord (𝐴 ↑𝑜 suc 𝑦)) |
29 | | id 22 |
. . . . . . . 8
⊢ (𝐴 ∈ (On ∖
2𝑜) → 𝐴 ∈ (On ∖
2𝑜)) |
30 | | vex 3176 |
. . . . . . . . . 10
⊢ 𝑦 ∈ V |
31 | 30 | sucid 5721 |
. . . . . . . . 9
⊢ 𝑦 ∈ suc 𝑦 |
32 | | oeordi 7554 |
. . . . . . . . 9
⊢ ((suc
𝑦 ∈ On ∧ 𝐴 ∈ (On ∖
2𝑜)) → (𝑦 ∈ suc 𝑦 → (𝐴 ↑𝑜 𝑦) ∈ (𝐴 ↑𝑜 suc 𝑦))) |
33 | 31, 32 | mpi 20 |
. . . . . . . 8
⊢ ((suc
𝑦 ∈ On ∧ 𝐴 ∈ (On ∖
2𝑜)) → (𝐴 ↑𝑜 𝑦) ∈ (𝐴 ↑𝑜 suc 𝑦)) |
34 | 24, 29, 33 | syl2anr 494 |
. . . . . . 7
⊢ ((𝐴 ∈ (On ∖
2𝑜) ∧ 𝑦 ∈ On) → (𝐴 ↑𝑜 𝑦) ∈ (𝐴 ↑𝑜 suc 𝑦)) |
35 | | ordsucss 6910 |
. . . . . . 7
⊢ (Ord
(𝐴
↑𝑜 suc 𝑦) → ((𝐴 ↑𝑜 𝑦) ∈ (𝐴 ↑𝑜 suc 𝑦) → suc (𝐴 ↑𝑜 𝑦) ⊆ (𝐴 ↑𝑜 suc 𝑦))) |
36 | 28, 34, 35 | sylc 63 |
. . . . . 6
⊢ ((𝐴 ∈ (On ∖
2𝑜) ∧ 𝑦 ∈ On) → suc (𝐴 ↑𝑜 𝑦) ⊆ (𝐴 ↑𝑜 suc 𝑦)) |
37 | | sstr2 3575 |
. . . . . 6
⊢ (suc
𝑦 ⊆ suc (𝐴 ↑𝑜
𝑦) → (suc (𝐴 ↑𝑜
𝑦) ⊆ (𝐴 ↑𝑜 suc
𝑦) → suc 𝑦 ⊆ (𝐴 ↑𝑜 suc 𝑦))) |
38 | 36, 37 | syl5com 31 |
. . . . 5
⊢ ((𝐴 ∈ (On ∖
2𝑜) ∧ 𝑦 ∈ On) → (suc 𝑦 ⊆ suc (𝐴 ↑𝑜 𝑦) → suc 𝑦 ⊆ (𝐴 ↑𝑜 suc 𝑦))) |
39 | 23, 38 | sylbid 229 |
. . . 4
⊢ ((𝐴 ∈ (On ∖
2𝑜) ∧ 𝑦 ∈ On) → (𝑦 ⊆ (𝐴 ↑𝑜 𝑦) → suc 𝑦 ⊆ (𝐴 ↑𝑜 suc 𝑦))) |
40 | 39 | expcom 450 |
. . 3
⊢ (𝑦 ∈ On → (𝐴 ∈ (On ∖
2𝑜) → (𝑦 ⊆ (𝐴 ↑𝑜 𝑦) → suc 𝑦 ⊆ (𝐴 ↑𝑜 suc 𝑦)))) |
41 | | dif20el 7472 |
. . . . 5
⊢ (𝐴 ∈ (On ∖
2𝑜) → ∅ ∈ 𝐴) |
42 | 17, 41 | jca 553 |
. . . 4
⊢ (𝐴 ∈ (On ∖
2𝑜) → (𝐴 ∈ On ∧ ∅ ∈ 𝐴)) |
43 | | ss2iun 4472 |
. . . . . 6
⊢
(∀𝑦 ∈
𝑥 𝑦 ⊆ (𝐴 ↑𝑜 𝑦) → ∪ 𝑦 ∈ 𝑥 𝑦 ⊆ ∪
𝑦 ∈ 𝑥 (𝐴 ↑𝑜 𝑦)) |
44 | | limuni 5702 |
. . . . . . . . 9
⊢ (Lim
𝑥 → 𝑥 = ∪ 𝑥) |
45 | | uniiun 4509 |
. . . . . . . . 9
⊢ ∪ 𝑥 =
∪ 𝑦 ∈ 𝑥 𝑦 |
46 | 44, 45 | syl6eq 2660 |
. . . . . . . 8
⊢ (Lim
𝑥 → 𝑥 = ∪ 𝑦 ∈ 𝑥 𝑦) |
47 | 46 | adantr 480 |
. . . . . . 7
⊢ ((Lim
𝑥 ∧ (𝐴 ∈ On ∧ ∅ ∈ 𝐴)) → 𝑥 = ∪ 𝑦 ∈ 𝑥 𝑦) |
48 | | vex 3176 |
. . . . . . . . . 10
⊢ 𝑥 ∈ V |
49 | | oelim 7501 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) ∧ ∅ ∈ 𝐴) → (𝐴 ↑𝑜 𝑥) = ∪ 𝑦 ∈ 𝑥 (𝐴 ↑𝑜 𝑦)) |
50 | 48, 49 | mpanlr1 718 |
. . . . . . . . 9
⊢ (((𝐴 ∈ On ∧ Lim 𝑥) ∧ ∅ ∈ 𝐴) → (𝐴 ↑𝑜 𝑥) = ∪ 𝑦 ∈ 𝑥 (𝐴 ↑𝑜 𝑦)) |
51 | 50 | anasss 677 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧ (Lim 𝑥 ∧ ∅ ∈ 𝐴)) → (𝐴 ↑𝑜 𝑥) = ∪ 𝑦 ∈ 𝑥 (𝐴 ↑𝑜 𝑦)) |
52 | 51 | an12s 839 |
. . . . . . 7
⊢ ((Lim
𝑥 ∧ (𝐴 ∈ On ∧ ∅ ∈ 𝐴)) → (𝐴 ↑𝑜 𝑥) = ∪ 𝑦 ∈ 𝑥 (𝐴 ↑𝑜 𝑦)) |
53 | 47, 52 | sseq12d 3597 |
. . . . . 6
⊢ ((Lim
𝑥 ∧ (𝐴 ∈ On ∧ ∅ ∈ 𝐴)) → (𝑥 ⊆ (𝐴 ↑𝑜 𝑥) ↔ ∪ 𝑦 ∈ 𝑥 𝑦 ⊆ ∪
𝑦 ∈ 𝑥 (𝐴 ↑𝑜 𝑦))) |
54 | 43, 53 | syl5ibr 235 |
. . . . 5
⊢ ((Lim
𝑥 ∧ (𝐴 ∈ On ∧ ∅ ∈ 𝐴)) → (∀𝑦 ∈ 𝑥 𝑦 ⊆ (𝐴 ↑𝑜 𝑦) → 𝑥 ⊆ (𝐴 ↑𝑜 𝑥))) |
55 | 54 | ex 449 |
. . . 4
⊢ (Lim
𝑥 → ((𝐴 ∈ On ∧ ∅ ∈
𝐴) → (∀𝑦 ∈ 𝑥 𝑦 ⊆ (𝐴 ↑𝑜 𝑦) → 𝑥 ⊆ (𝐴 ↑𝑜 𝑥)))) |
56 | 42, 55 | syl5 33 |
. . 3
⊢ (Lim
𝑥 → (𝐴 ∈ (On ∖ 2𝑜)
→ (∀𝑦 ∈
𝑥 𝑦 ⊆ (𝐴 ↑𝑜 𝑦) → 𝑥 ⊆ (𝐴 ↑𝑜 𝑥)))) |
57 | 3, 6, 9, 12, 14, 40, 56 | tfinds3 6956 |
. 2
⊢ (𝐵 ∈ On → (𝐴 ∈ (On ∖
2𝑜) → 𝐵 ⊆ (𝐴 ↑𝑜 𝐵))) |
58 | 57 | impcom 445 |
1
⊢ ((𝐴 ∈ (On ∖
2𝑜) ∧ 𝐵 ∈ On) → 𝐵 ⊆ (𝐴 ↑𝑜 𝐵)) |