| Step | Hyp | Ref
| Expression |
| 1 | | id 22 |
. . . 4
⊢ (𝑥 = ∅ → 𝑥 = ∅) |
| 2 | | oveq2 7439 |
. . . 4
⊢ (𝑥 = ∅ → (𝐴 ↑o 𝑥) = (𝐴 ↑o
∅)) |
| 3 | 1, 2 | sseq12d 4017 |
. . 3
⊢ (𝑥 = ∅ → (𝑥 ⊆ (𝐴 ↑o 𝑥) ↔ ∅ ⊆ (𝐴 ↑o
∅))) |
| 4 | | id 22 |
. . . 4
⊢ (𝑥 = 𝑦 → 𝑥 = 𝑦) |
| 5 | | oveq2 7439 |
. . . 4
⊢ (𝑥 = 𝑦 → (𝐴 ↑o 𝑥) = (𝐴 ↑o 𝑦)) |
| 6 | 4, 5 | sseq12d 4017 |
. . 3
⊢ (𝑥 = 𝑦 → (𝑥 ⊆ (𝐴 ↑o 𝑥) ↔ 𝑦 ⊆ (𝐴 ↑o 𝑦))) |
| 7 | | id 22 |
. . . 4
⊢ (𝑥 = suc 𝑦 → 𝑥 = suc 𝑦) |
| 8 | | oveq2 7439 |
. . . 4
⊢ (𝑥 = suc 𝑦 → (𝐴 ↑o 𝑥) = (𝐴 ↑o suc 𝑦)) |
| 9 | 7, 8 | sseq12d 4017 |
. . 3
⊢ (𝑥 = suc 𝑦 → (𝑥 ⊆ (𝐴 ↑o 𝑥) ↔ suc 𝑦 ⊆ (𝐴 ↑o suc 𝑦))) |
| 10 | | id 22 |
. . . 4
⊢ (𝑥 = 𝐵 → 𝑥 = 𝐵) |
| 11 | | oveq2 7439 |
. . . 4
⊢ (𝑥 = 𝐵 → (𝐴 ↑o 𝑥) = (𝐴 ↑o 𝐵)) |
| 12 | 10, 11 | sseq12d 4017 |
. . 3
⊢ (𝑥 = 𝐵 → (𝑥 ⊆ (𝐴 ↑o 𝑥) ↔ 𝐵 ⊆ (𝐴 ↑o 𝐵))) |
| 13 | | 0ss 4400 |
. . . 4
⊢ ∅
⊆ (𝐴
↑o ∅) |
| 14 | 13 | a1i 11 |
. . 3
⊢ (𝐴 ∈ (On ∖
2o) → ∅ ⊆ (𝐴 ↑o
∅)) |
| 15 | | eloni 6394 |
. . . . . 6
⊢ (𝑦 ∈ On → Ord 𝑦) |
| 16 | | eldifi 4131 |
. . . . . . . 8
⊢ (𝐴 ∈ (On ∖
2o) → 𝐴
∈ On) |
| 17 | | oecl 8575 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧ 𝑦 ∈ On) → (𝐴 ↑o 𝑦) ∈ On) |
| 18 | 16, 17 | sylan 580 |
. . . . . . 7
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝑦
∈ On) → (𝐴
↑o 𝑦)
∈ On) |
| 19 | | eloni 6394 |
. . . . . . 7
⊢ ((𝐴 ↑o 𝑦) ∈ On → Ord (𝐴 ↑o 𝑦)) |
| 20 | 18, 19 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝑦
∈ On) → Ord (𝐴
↑o 𝑦)) |
| 21 | | ordsucsssuc 7843 |
. . . . . 6
⊢ ((Ord
𝑦 ∧ Ord (𝐴 ↑o 𝑦)) → (𝑦 ⊆ (𝐴 ↑o 𝑦) ↔ suc 𝑦 ⊆ suc (𝐴 ↑o 𝑦))) |
| 22 | 15, 20, 21 | syl2an2 686 |
. . . . 5
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝑦
∈ On) → (𝑦
⊆ (𝐴
↑o 𝑦)
↔ suc 𝑦 ⊆ suc
(𝐴 ↑o 𝑦))) |
| 23 | | onsuc 7831 |
. . . . . . . . 9
⊢ (𝑦 ∈ On → suc 𝑦 ∈ On) |
| 24 | | oecl 8575 |
. . . . . . . . 9
⊢ ((𝐴 ∈ On ∧ suc 𝑦 ∈ On) → (𝐴 ↑o suc 𝑦) ∈ On) |
| 25 | 16, 23, 24 | syl2an 596 |
. . . . . . . 8
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝑦
∈ On) → (𝐴
↑o suc 𝑦)
∈ On) |
| 26 | | eloni 6394 |
. . . . . . . 8
⊢ ((𝐴 ↑o suc 𝑦) ∈ On → Ord (𝐴 ↑o suc 𝑦)) |
| 27 | 25, 26 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝑦
∈ On) → Ord (𝐴
↑o suc 𝑦)) |
| 28 | | id 22 |
. . . . . . . 8
⊢ (𝐴 ∈ (On ∖
2o) → 𝐴
∈ (On ∖ 2o)) |
| 29 | | vex 3484 |
. . . . . . . . . 10
⊢ 𝑦 ∈ V |
| 30 | 29 | sucid 6466 |
. . . . . . . . 9
⊢ 𝑦 ∈ suc 𝑦 |
| 31 | | oeordi 8625 |
. . . . . . . . 9
⊢ ((suc
𝑦 ∈ On ∧ 𝐴 ∈ (On ∖
2o)) → (𝑦
∈ suc 𝑦 → (𝐴 ↑o 𝑦) ∈ (𝐴 ↑o suc 𝑦))) |
| 32 | 30, 31 | mpi 20 |
. . . . . . . 8
⊢ ((suc
𝑦 ∈ On ∧ 𝐴 ∈ (On ∖
2o)) → (𝐴
↑o 𝑦)
∈ (𝐴
↑o suc 𝑦)) |
| 33 | 23, 28, 32 | syl2anr 597 |
. . . . . . 7
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝑦
∈ On) → (𝐴
↑o 𝑦)
∈ (𝐴
↑o suc 𝑦)) |
| 34 | | ordsucss 7838 |
. . . . . . 7
⊢ (Ord
(𝐴 ↑o suc
𝑦) → ((𝐴 ↑o 𝑦) ∈ (𝐴 ↑o suc 𝑦) → suc (𝐴 ↑o 𝑦) ⊆ (𝐴 ↑o suc 𝑦))) |
| 35 | 27, 33, 34 | sylc 65 |
. . . . . 6
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝑦
∈ On) → suc (𝐴
↑o 𝑦)
⊆ (𝐴
↑o suc 𝑦)) |
| 36 | | sstr2 3990 |
. . . . . 6
⊢ (suc
𝑦 ⊆ suc (𝐴 ↑o 𝑦) → (suc (𝐴 ↑o 𝑦) ⊆ (𝐴 ↑o suc 𝑦) → suc 𝑦 ⊆ (𝐴 ↑o suc 𝑦))) |
| 37 | 35, 36 | syl5com 31 |
. . . . 5
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝑦
∈ On) → (suc 𝑦
⊆ suc (𝐴
↑o 𝑦)
→ suc 𝑦 ⊆ (𝐴 ↑o suc 𝑦))) |
| 38 | 22, 37 | sylbid 240 |
. . . 4
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝑦
∈ On) → (𝑦
⊆ (𝐴
↑o 𝑦)
→ suc 𝑦 ⊆ (𝐴 ↑o suc 𝑦))) |
| 39 | 38 | expcom 413 |
. . 3
⊢ (𝑦 ∈ On → (𝐴 ∈ (On ∖
2o) → (𝑦
⊆ (𝐴
↑o 𝑦)
→ suc 𝑦 ⊆ (𝐴 ↑o suc 𝑦)))) |
| 40 | | dif20el 8543 |
. . . . 5
⊢ (𝐴 ∈ (On ∖
2o) → ∅ ∈ 𝐴) |
| 41 | 16, 40 | jca 511 |
. . . 4
⊢ (𝐴 ∈ (On ∖
2o) → (𝐴
∈ On ∧ ∅ ∈ 𝐴)) |
| 42 | | ss2iun 5010 |
. . . . . 6
⊢
(∀𝑦 ∈
𝑥 𝑦 ⊆ (𝐴 ↑o 𝑦) → ∪
𝑦 ∈ 𝑥 𝑦 ⊆ ∪
𝑦 ∈ 𝑥 (𝐴 ↑o 𝑦)) |
| 43 | | limuni 6445 |
. . . . . . . . 9
⊢ (Lim
𝑥 → 𝑥 = ∪ 𝑥) |
| 44 | | uniiun 5058 |
. . . . . . . . 9
⊢ ∪ 𝑥 =
∪ 𝑦 ∈ 𝑥 𝑦 |
| 45 | 43, 44 | eqtrdi 2793 |
. . . . . . . 8
⊢ (Lim
𝑥 → 𝑥 = ∪ 𝑦 ∈ 𝑥 𝑦) |
| 46 | 45 | adantr 480 |
. . . . . . 7
⊢ ((Lim
𝑥 ∧ (𝐴 ∈ On ∧ ∅ ∈ 𝐴)) → 𝑥 = ∪ 𝑦 ∈ 𝑥 𝑦) |
| 47 | | vex 3484 |
. . . . . . . . . 10
⊢ 𝑥 ∈ V |
| 48 | | oelim 8572 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) ∧ ∅ ∈ 𝐴) → (𝐴 ↑o 𝑥) = ∪ 𝑦 ∈ 𝑥 (𝐴 ↑o 𝑦)) |
| 49 | 47, 48 | mpanlr1 706 |
. . . . . . . . 9
⊢ (((𝐴 ∈ On ∧ Lim 𝑥) ∧ ∅ ∈ 𝐴) → (𝐴 ↑o 𝑥) = ∪ 𝑦 ∈ 𝑥 (𝐴 ↑o 𝑦)) |
| 50 | 49 | anasss 466 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧ (Lim 𝑥 ∧ ∅ ∈ 𝐴)) → (𝐴 ↑o 𝑥) = ∪ 𝑦 ∈ 𝑥 (𝐴 ↑o 𝑦)) |
| 51 | 50 | an12s 649 |
. . . . . . 7
⊢ ((Lim
𝑥 ∧ (𝐴 ∈ On ∧ ∅ ∈ 𝐴)) → (𝐴 ↑o 𝑥) = ∪ 𝑦 ∈ 𝑥 (𝐴 ↑o 𝑦)) |
| 52 | 46, 51 | sseq12d 4017 |
. . . . . 6
⊢ ((Lim
𝑥 ∧ (𝐴 ∈ On ∧ ∅ ∈ 𝐴)) → (𝑥 ⊆ (𝐴 ↑o 𝑥) ↔ ∪
𝑦 ∈ 𝑥 𝑦 ⊆ ∪
𝑦 ∈ 𝑥 (𝐴 ↑o 𝑦))) |
| 53 | 42, 52 | imbitrrid 246 |
. . . . 5
⊢ ((Lim
𝑥 ∧ (𝐴 ∈ On ∧ ∅ ∈ 𝐴)) → (∀𝑦 ∈ 𝑥 𝑦 ⊆ (𝐴 ↑o 𝑦) → 𝑥 ⊆ (𝐴 ↑o 𝑥))) |
| 54 | 53 | ex 412 |
. . . 4
⊢ (Lim
𝑥 → ((𝐴 ∈ On ∧ ∅ ∈
𝐴) → (∀𝑦 ∈ 𝑥 𝑦 ⊆ (𝐴 ↑o 𝑦) → 𝑥 ⊆ (𝐴 ↑o 𝑥)))) |
| 55 | 41, 54 | syl5 34 |
. . 3
⊢ (Lim
𝑥 → (𝐴 ∈ (On ∖ 2o) →
(∀𝑦 ∈ 𝑥 𝑦 ⊆ (𝐴 ↑o 𝑦) → 𝑥 ⊆ (𝐴 ↑o 𝑥)))) |
| 56 | 3, 6, 9, 12, 14, 39, 55 | tfinds3 7886 |
. 2
⊢ (𝐵 ∈ On → (𝐴 ∈ (On ∖
2o) → 𝐵
⊆ (𝐴
↑o 𝐵))) |
| 57 | 56 | impcom 407 |
1
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) → 𝐵 ⊆
(𝐴 ↑o 𝐵)) |