| Step | Hyp | Ref
| Expression |
| 1 | | oeeu.1 |
. . 3
⊢ 𝑋 = ∪
∩ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} |
| 2 | | eldifi 4131 |
. . . . . . . 8
⊢ (𝐵 ∈ (On ∖
1o) → 𝐵
∈ On) |
| 3 | 2 | adantl 481 |
. . . . . . 7
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → 𝐵 ∈ On) |
| 4 | | onsuc 7831 |
. . . . . . 7
⊢ (𝐵 ∈ On → suc 𝐵 ∈ On) |
| 5 | 3, 4 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → suc 𝐵 ∈ On) |
| 6 | | oeworde 8631 |
. . . . . . . 8
⊢ ((𝐴 ∈ (On ∖
2o) ∧ suc 𝐵
∈ On) → suc 𝐵
⊆ (𝐴
↑o suc 𝐵)) |
| 7 | 5, 6 | syldan 591 |
. . . . . . 7
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → suc 𝐵 ⊆ (𝐴 ↑o suc 𝐵)) |
| 8 | | sucidg 6465 |
. . . . . . . 8
⊢ (𝐵 ∈ On → 𝐵 ∈ suc 𝐵) |
| 9 | 3, 8 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → 𝐵 ∈ suc 𝐵) |
| 10 | 7, 9 | sseldd 3984 |
. . . . . 6
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → 𝐵 ∈ (𝐴 ↑o suc 𝐵)) |
| 11 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑥 = suc 𝐵 → (𝐴 ↑o 𝑥) = (𝐴 ↑o suc 𝐵)) |
| 12 | 11 | eleq2d 2827 |
. . . . . . 7
⊢ (𝑥 = suc 𝐵 → (𝐵 ∈ (𝐴 ↑o 𝑥) ↔ 𝐵 ∈ (𝐴 ↑o suc 𝐵))) |
| 13 | 12 | rspcev 3622 |
. . . . . 6
⊢ ((suc
𝐵 ∈ On ∧ 𝐵 ∈ (𝐴 ↑o suc 𝐵)) → ∃𝑥 ∈ On 𝐵 ∈ (𝐴 ↑o 𝑥)) |
| 14 | 5, 10, 13 | syl2anc 584 |
. . . . 5
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → ∃𝑥 ∈ On 𝐵 ∈ (𝐴 ↑o 𝑥)) |
| 15 | | onintrab2 7817 |
. . . . 5
⊢
(∃𝑥 ∈ On
𝐵 ∈ (𝐴 ↑o 𝑥) ↔ ∩ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} ∈ On) |
| 16 | 14, 15 | sylib 218 |
. . . 4
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → ∩ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} ∈ On) |
| 17 | | onuni 7808 |
. . . 4
⊢ (∩ {𝑥
∈ On ∣ 𝐵 ∈
(𝐴 ↑o 𝑥)} ∈ On → ∪ ∩ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} ∈ On) |
| 18 | 16, 17 | syl 17 |
. . 3
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → ∪ ∩ {𝑥
∈ On ∣ 𝐵 ∈
(𝐴 ↑o 𝑥)} ∈ On) |
| 19 | 1, 18 | eqeltrid 2845 |
. 2
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → 𝑋 ∈ On) |
| 20 | | sucidg 6465 |
. . . . . . 7
⊢ (𝑋 ∈ On → 𝑋 ∈ suc 𝑋) |
| 21 | 19, 20 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → 𝑋 ∈ suc 𝑋) |
| 22 | | suceq 6450 |
. . . . . . . 8
⊢ (𝑋 = ∪
∩ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} → suc 𝑋 = suc ∪ ∩ {𝑥
∈ On ∣ 𝐵 ∈
(𝐴 ↑o 𝑥)}) |
| 23 | 1, 22 | ax-mp 5 |
. . . . . . 7
⊢ suc 𝑋 = suc ∪ ∩ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} |
| 24 | | dif1o 8538 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∈ (On ∖
1o) ↔ (𝐵
∈ On ∧ 𝐵 ≠
∅)) |
| 25 | 24 | simprbi 496 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈ (On ∖
1o) → 𝐵
≠ ∅) |
| 26 | 25 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → 𝐵 ≠ ∅) |
| 27 | | ssrab2 4080 |
. . . . . . . . . . . . . . 15
⊢ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} ⊆ On |
| 28 | | rabn0 4389 |
. . . . . . . . . . . . . . . 16
⊢ ({𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} ≠ ∅ ↔ ∃𝑥 ∈ On 𝐵 ∈ (𝐴 ↑o 𝑥)) |
| 29 | 14, 28 | sylibr 234 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} ≠ ∅) |
| 30 | | onint 7810 |
. . . . . . . . . . . . . . 15
⊢ (({𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} ⊆ On ∧ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} ≠ ∅) → ∩ {𝑥
∈ On ∣ 𝐵 ∈
(𝐴 ↑o 𝑥)} ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)}) |
| 31 | 27, 29, 30 | sylancr 587 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → ∩ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)}) |
| 32 | | eleq1 2829 |
. . . . . . . . . . . . . 14
⊢ (∩ {𝑥
∈ On ∣ 𝐵 ∈
(𝐴 ↑o 𝑥)} = ∅ → (∩ {𝑥
∈ On ∣ 𝐵 ∈
(𝐴 ↑o 𝑥)} ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} ↔ ∅ ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)})) |
| 33 | 31, 32 | syl5ibcom 245 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → (∩ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} = ∅ → ∅ ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)})) |
| 34 | | oveq2 7439 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = ∅ → (𝐴 ↑o 𝑥) = (𝐴 ↑o
∅)) |
| 35 | 34 | eleq2d 2827 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = ∅ → (𝐵 ∈ (𝐴 ↑o 𝑥) ↔ 𝐵 ∈ (𝐴 ↑o
∅))) |
| 36 | 35 | elrab 3692 |
. . . . . . . . . . . . . . 15
⊢ (∅
∈ {𝑥 ∈ On ∣
𝐵 ∈ (𝐴 ↑o 𝑥)} ↔ (∅ ∈ On ∧ 𝐵 ∈ (𝐴 ↑o
∅))) |
| 37 | 36 | simprbi 496 |
. . . . . . . . . . . . . 14
⊢ (∅
∈ {𝑥 ∈ On ∣
𝐵 ∈ (𝐴 ↑o 𝑥)} → 𝐵 ∈ (𝐴 ↑o
∅)) |
| 38 | | eldifi 4131 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ (On ∖
2o) → 𝐴
∈ On) |
| 39 | 38 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → 𝐴 ∈ On) |
| 40 | | oe0 8560 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ On → (𝐴 ↑o ∅) =
1o) |
| 41 | 39, 40 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → (𝐴 ↑o ∅) =
1o) |
| 42 | 41 | eleq2d 2827 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → (𝐵 ∈ (𝐴 ↑o ∅) ↔ 𝐵 ∈
1o)) |
| 43 | | el1o 8533 |
. . . . . . . . . . . . . . 15
⊢ (𝐵 ∈ 1o ↔
𝐵 =
∅) |
| 44 | 42, 43 | bitrdi 287 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → (𝐵 ∈ (𝐴 ↑o ∅) ↔ 𝐵 = ∅)) |
| 45 | 37, 44 | imbitrid 244 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → (∅ ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} → 𝐵 = ∅)) |
| 46 | 33, 45 | syld 47 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → (∩ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} = ∅ → 𝐵 = ∅)) |
| 47 | 46 | necon3ad 2953 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → (𝐵 ≠ ∅ → ¬ ∩ {𝑥
∈ On ∣ 𝐵 ∈
(𝐴 ↑o 𝑥)} = ∅)) |
| 48 | 26, 47 | mpd 15 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → ¬ ∩
{𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} = ∅) |
| 49 | | limuni 6445 |
. . . . . . . . . . . . . . . . 17
⊢ (Lim
∩ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} → ∩ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} = ∪ ∩ {𝑥
∈ On ∣ 𝐵 ∈
(𝐴 ↑o 𝑥)}) |
| 50 | 49, 1 | eqtr4di 2795 |
. . . . . . . . . . . . . . . 16
⊢ (Lim
∩ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} → ∩ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} = 𝑋) |
| 51 | 50 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ Lim ∩
{𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)}) → ∩
{𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} = 𝑋) |
| 52 | 31 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ Lim ∩
{𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)}) → ∩
{𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)}) |
| 53 | 51, 52 | eqeltrrd 2842 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ Lim ∩
{𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)}) → 𝑋 ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)}) |
| 54 | | oveq2 7439 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑋 → (𝐴 ↑o 𝑦) = (𝐴 ↑o 𝑋)) |
| 55 | 54 | eleq2d 2827 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑋 → (𝐵 ∈ (𝐴 ↑o 𝑦) ↔ 𝐵 ∈ (𝐴 ↑o 𝑋))) |
| 56 | | oveq2 7439 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑦 → (𝐴 ↑o 𝑥) = (𝐴 ↑o 𝑦)) |
| 57 | 56 | eleq2d 2827 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑦 → (𝐵 ∈ (𝐴 ↑o 𝑥) ↔ 𝐵 ∈ (𝐴 ↑o 𝑦))) |
| 58 | 57 | cbvrabv 3447 |
. . . . . . . . . . . . . . . 16
⊢ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} = {𝑦 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑦)} |
| 59 | 55, 58 | elrab2 3695 |
. . . . . . . . . . . . . . 15
⊢ (𝑋 ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} ↔ (𝑋 ∈ On ∧ 𝐵 ∈ (𝐴 ↑o 𝑋))) |
| 60 | 59 | simprbi 496 |
. . . . . . . . . . . . . 14
⊢ (𝑋 ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} → 𝐵 ∈ (𝐴 ↑o 𝑋)) |
| 61 | 53, 60 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ Lim ∩
{𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)}) → 𝐵 ∈ (𝐴 ↑o 𝑋)) |
| 62 | 38 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ Lim ∩
{𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)}) → 𝐴 ∈ On) |
| 63 | | limeq 6396 |
. . . . . . . . . . . . . . . . 17
⊢ (∩ {𝑥
∈ On ∣ 𝐵 ∈
(𝐴 ↑o 𝑥)} = 𝑋 → (Lim ∩
{𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} ↔ Lim 𝑋)) |
| 64 | 50, 63 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (Lim
∩ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} → (Lim ∩
{𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} ↔ Lim 𝑋)) |
| 65 | 64 | ibi 267 |
. . . . . . . . . . . . . . 15
⊢ (Lim
∩ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} → Lim 𝑋) |
| 66 | 19, 65 | anim12i 613 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ Lim ∩
{𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)}) → (𝑋 ∈ On ∧ Lim 𝑋)) |
| 67 | | dif20el 8543 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ (On ∖
2o) → ∅ ∈ 𝐴) |
| 68 | 67 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ Lim ∩
{𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)}) → ∅ ∈ 𝐴) |
| 69 | | oelim 8572 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ On ∧ (𝑋 ∈ On ∧ Lim 𝑋)) ∧ ∅ ∈ 𝐴) → (𝐴 ↑o 𝑋) = ∪
𝑦 ∈ 𝑋 (𝐴 ↑o 𝑦)) |
| 70 | 62, 66, 68, 69 | syl21anc 838 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ Lim ∩
{𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)}) → (𝐴 ↑o 𝑋) = ∪
𝑦 ∈ 𝑋 (𝐴 ↑o 𝑦)) |
| 71 | 61, 70 | eleqtrd 2843 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ Lim ∩
{𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)}) → 𝐵 ∈ ∪
𝑦 ∈ 𝑋 (𝐴 ↑o 𝑦)) |
| 72 | | eliun 4995 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈ ∪ 𝑦 ∈ 𝑋 (𝐴 ↑o 𝑦) ↔ ∃𝑦 ∈ 𝑋 𝐵 ∈ (𝐴 ↑o 𝑦)) |
| 73 | 71, 72 | sylib 218 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ Lim ∩
{𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)}) → ∃𝑦 ∈ 𝑋 𝐵 ∈ (𝐴 ↑o 𝑦)) |
| 74 | 19 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ Lim ∩
{𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)}) → 𝑋 ∈ On) |
| 75 | | onss 7805 |
. . . . . . . . . . . . . . 15
⊢ (𝑋 ∈ On → 𝑋 ⊆ On) |
| 76 | 74, 75 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ Lim ∩
{𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)}) → 𝑋 ⊆ On) |
| 77 | 76 | sselda 3983 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ Lim ∩
{𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)}) ∧ 𝑦 ∈ 𝑋) → 𝑦 ∈ On) |
| 78 | 51 | eleq2d 2827 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ Lim ∩
{𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)}) → (𝑦 ∈ ∩ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} ↔ 𝑦 ∈ 𝑋)) |
| 79 | 78 | biimpar 477 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ Lim ∩
{𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)}) ∧ 𝑦 ∈ 𝑋) → 𝑦 ∈ ∩ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)}) |
| 80 | 57 | onnminsb 7819 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ On → (𝑦 ∈ ∩ {𝑥
∈ On ∣ 𝐵 ∈
(𝐴 ↑o 𝑥)} → ¬ 𝐵 ∈ (𝐴 ↑o 𝑦))) |
| 81 | 77, 79, 80 | sylc 65 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ Lim ∩
{𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)}) ∧ 𝑦 ∈ 𝑋) → ¬ 𝐵 ∈ (𝐴 ↑o 𝑦)) |
| 82 | 81 | nrexdv 3149 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ Lim ∩
{𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)}) → ¬ ∃𝑦 ∈ 𝑋 𝐵 ∈ (𝐴 ↑o 𝑦)) |
| 83 | 73, 82 | pm2.65da 817 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → ¬ Lim ∩ {𝑥
∈ On ∣ 𝐵 ∈
(𝐴 ↑o 𝑥)}) |
| 84 | | ioran 986 |
. . . . . . . . . 10
⊢ (¬
(∩ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} = ∅ ∨ Lim ∩ {𝑥
∈ On ∣ 𝐵 ∈
(𝐴 ↑o 𝑥)}) ↔ (¬ ∩ {𝑥
∈ On ∣ 𝐵 ∈
(𝐴 ↑o 𝑥)} = ∅ ∧ ¬ Lim
∩ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)})) |
| 85 | 48, 83, 84 | sylanbrc 583 |
. . . . . . . . 9
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → ¬ (∩
{𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} = ∅ ∨ Lim ∩ {𝑥
∈ On ∣ 𝐵 ∈
(𝐴 ↑o 𝑥)})) |
| 86 | | eloni 6394 |
. . . . . . . . . 10
⊢ (∩ {𝑥
∈ On ∣ 𝐵 ∈
(𝐴 ↑o 𝑥)} ∈ On → Ord ∩ {𝑥
∈ On ∣ 𝐵 ∈
(𝐴 ↑o 𝑥)}) |
| 87 | | unizlim 6507 |
. . . . . . . . . 10
⊢ (Ord
∩ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} → (∩
{𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} = ∪ ∩ {𝑥
∈ On ∣ 𝐵 ∈
(𝐴 ↑o 𝑥)} ↔ (∩ {𝑥
∈ On ∣ 𝐵 ∈
(𝐴 ↑o 𝑥)} = ∅ ∨ Lim ∩ {𝑥
∈ On ∣ 𝐵 ∈
(𝐴 ↑o 𝑥)}))) |
| 88 | 16, 86, 87 | 3syl 18 |
. . . . . . . . 9
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → (∩ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} = ∪ ∩ {𝑥
∈ On ∣ 𝐵 ∈
(𝐴 ↑o 𝑥)} ↔ (∩ {𝑥
∈ On ∣ 𝐵 ∈
(𝐴 ↑o 𝑥)} = ∅ ∨ Lim ∩ {𝑥
∈ On ∣ 𝐵 ∈
(𝐴 ↑o 𝑥)}))) |
| 89 | 85, 88 | mtbird 325 |
. . . . . . . 8
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → ¬ ∩
{𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} = ∪ ∩ {𝑥
∈ On ∣ 𝐵 ∈
(𝐴 ↑o 𝑥)}) |
| 90 | | orduniorsuc 7850 |
. . . . . . . . . 10
⊢ (Ord
∩ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} → (∩
{𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} = ∪ ∩ {𝑥
∈ On ∣ 𝐵 ∈
(𝐴 ↑o 𝑥)} ∨ ∩ {𝑥
∈ On ∣ 𝐵 ∈
(𝐴 ↑o 𝑥)} = suc ∪ ∩ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)})) |
| 91 | 16, 86, 90 | 3syl 18 |
. . . . . . . . 9
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → (∩ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} = ∪ ∩ {𝑥
∈ On ∣ 𝐵 ∈
(𝐴 ↑o 𝑥)} ∨ ∩ {𝑥
∈ On ∣ 𝐵 ∈
(𝐴 ↑o 𝑥)} = suc ∪ ∩ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)})) |
| 92 | 91 | ord 865 |
. . . . . . . 8
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → (¬ ∩
{𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} = ∪ ∩ {𝑥
∈ On ∣ 𝐵 ∈
(𝐴 ↑o 𝑥)} → ∩ {𝑥
∈ On ∣ 𝐵 ∈
(𝐴 ↑o 𝑥)} = suc ∪ ∩ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)})) |
| 93 | 89, 92 | mpd 15 |
. . . . . . 7
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → ∩ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} = suc ∪ ∩ {𝑥
∈ On ∣ 𝐵 ∈
(𝐴 ↑o 𝑥)}) |
| 94 | 23, 93 | eqtr4id 2796 |
. . . . . 6
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → suc 𝑋 = ∩ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)}) |
| 95 | 21, 94 | eleqtrd 2843 |
. . . . 5
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → 𝑋 ∈ ∩ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)}) |
| 96 | 58 | inteqi 4950 |
. . . . 5
⊢ ∩ {𝑥
∈ On ∣ 𝐵 ∈
(𝐴 ↑o 𝑥)} = ∩ {𝑦
∈ On ∣ 𝐵 ∈
(𝐴 ↑o 𝑦)} |
| 97 | 95, 96 | eleqtrdi 2851 |
. . . 4
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → 𝑋 ∈ ∩ {𝑦 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑦)}) |
| 98 | 55 | onnminsb 7819 |
. . . 4
⊢ (𝑋 ∈ On → (𝑋 ∈ ∩ {𝑦
∈ On ∣ 𝐵 ∈
(𝐴 ↑o 𝑦)} → ¬ 𝐵 ∈ (𝐴 ↑o 𝑋))) |
| 99 | 19, 97, 98 | sylc 65 |
. . 3
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → ¬ 𝐵 ∈ (𝐴 ↑o 𝑋)) |
| 100 | | oecl 8575 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝑋 ∈ On) → (𝐴 ↑o 𝑋) ∈ On) |
| 101 | 39, 19, 100 | syl2anc 584 |
. . . 4
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → (𝐴 ↑o 𝑋) ∈ On) |
| 102 | | ontri1 6418 |
. . . 4
⊢ (((𝐴 ↑o 𝑋) ∈ On ∧ 𝐵 ∈ On) → ((𝐴 ↑o 𝑋) ⊆ 𝐵 ↔ ¬ 𝐵 ∈ (𝐴 ↑o 𝑋))) |
| 103 | 101, 3, 102 | syl2anc 584 |
. . 3
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → ((𝐴 ↑o 𝑋) ⊆ 𝐵 ↔ ¬ 𝐵 ∈ (𝐴 ↑o 𝑋))) |
| 104 | 99, 103 | mpbird 257 |
. 2
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → (𝐴 ↑o 𝑋) ⊆ 𝐵) |
| 105 | 94, 31 | eqeltrd 2841 |
. . 3
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → suc 𝑋 ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)}) |
| 106 | | oveq2 7439 |
. . . . . 6
⊢ (𝑦 = suc 𝑋 → (𝐴 ↑o 𝑦) = (𝐴 ↑o suc 𝑋)) |
| 107 | 106 | eleq2d 2827 |
. . . . 5
⊢ (𝑦 = suc 𝑋 → (𝐵 ∈ (𝐴 ↑o 𝑦) ↔ 𝐵 ∈ (𝐴 ↑o suc 𝑋))) |
| 108 | 107, 58 | elrab2 3695 |
. . . 4
⊢ (suc
𝑋 ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} ↔ (suc 𝑋 ∈ On ∧ 𝐵 ∈ (𝐴 ↑o suc 𝑋))) |
| 109 | 108 | simprbi 496 |
. . 3
⊢ (suc
𝑋 ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} → 𝐵 ∈ (𝐴 ↑o suc 𝑋)) |
| 110 | 105, 109 | syl 17 |
. 2
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → 𝐵 ∈ (𝐴 ↑o suc 𝑋)) |
| 111 | 19, 104, 110 | 3jca 1129 |
1
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → (𝑋 ∈ On ∧ (𝐴 ↑o 𝑋) ⊆ 𝐵 ∧ 𝐵 ∈ (𝐴 ↑o suc 𝑋))) |