Step | Hyp | Ref
| Expression |
1 | | oeeu.1 |
. . 3
⊢ 𝑋 = ∪
∩ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} |
2 | | eldifi 3960 |
. . . . . . . 8
⊢ (𝐵 ∈ (On ∖
1o) → 𝐵
∈ On) |
3 | 2 | adantl 475 |
. . . . . . 7
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → 𝐵 ∈ On) |
4 | | suceloni 7275 |
. . . . . . 7
⊢ (𝐵 ∈ On → suc 𝐵 ∈ On) |
5 | 3, 4 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → suc 𝐵 ∈ On) |
6 | | oeworde 7941 |
. . . . . . . 8
⊢ ((𝐴 ∈ (On ∖
2o) ∧ suc 𝐵
∈ On) → suc 𝐵
⊆ (𝐴
↑o suc 𝐵)) |
7 | 5, 6 | syldan 587 |
. . . . . . 7
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → suc 𝐵 ⊆ (𝐴 ↑o suc 𝐵)) |
8 | | sucidg 6042 |
. . . . . . . 8
⊢ (𝐵 ∈ On → 𝐵 ∈ suc 𝐵) |
9 | 3, 8 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → 𝐵 ∈ suc 𝐵) |
10 | 7, 9 | sseldd 3829 |
. . . . . 6
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → 𝐵 ∈ (𝐴 ↑o suc 𝐵)) |
11 | | oveq2 6914 |
. . . . . . . 8
⊢ (𝑥 = suc 𝐵 → (𝐴 ↑o 𝑥) = (𝐴 ↑o suc 𝐵)) |
12 | 11 | eleq2d 2893 |
. . . . . . 7
⊢ (𝑥 = suc 𝐵 → (𝐵 ∈ (𝐴 ↑o 𝑥) ↔ 𝐵 ∈ (𝐴 ↑o suc 𝐵))) |
13 | 12 | rspcev 3527 |
. . . . . 6
⊢ ((suc
𝐵 ∈ On ∧ 𝐵 ∈ (𝐴 ↑o suc 𝐵)) → ∃𝑥 ∈ On 𝐵 ∈ (𝐴 ↑o 𝑥)) |
14 | 5, 10, 13 | syl2anc 581 |
. . . . 5
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → ∃𝑥 ∈ On 𝐵 ∈ (𝐴 ↑o 𝑥)) |
15 | | onintrab2 7264 |
. . . . 5
⊢
(∃𝑥 ∈ On
𝐵 ∈ (𝐴 ↑o 𝑥) ↔ ∩ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} ∈ On) |
16 | 14, 15 | sylib 210 |
. . . 4
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → ∩ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} ∈ On) |
17 | | onuni 7255 |
. . . 4
⊢ (∩ {𝑥
∈ On ∣ 𝐵 ∈
(𝐴 ↑o 𝑥)} ∈ On → ∪ ∩ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} ∈ On) |
18 | 16, 17 | syl 17 |
. . 3
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → ∪ ∩ {𝑥
∈ On ∣ 𝐵 ∈
(𝐴 ↑o 𝑥)} ∈ On) |
19 | 1, 18 | syl5eqel 2911 |
. 2
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → 𝑋 ∈ On) |
20 | | sucidg 6042 |
. . . . . . 7
⊢ (𝑋 ∈ On → 𝑋 ∈ suc 𝑋) |
21 | 19, 20 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → 𝑋 ∈ suc 𝑋) |
22 | | dif1o 7848 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∈ (On ∖
1o) ↔ (𝐵
∈ On ∧ 𝐵 ≠
∅)) |
23 | 22 | simprbi 492 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈ (On ∖
1o) → 𝐵
≠ ∅) |
24 | 23 | adantl 475 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → 𝐵 ≠ ∅) |
25 | | ssrab2 3913 |
. . . . . . . . . . . . . . 15
⊢ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} ⊆ On |
26 | | rabn0 4188 |
. . . . . . . . . . . . . . . 16
⊢ ({𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} ≠ ∅ ↔ ∃𝑥 ∈ On 𝐵 ∈ (𝐴 ↑o 𝑥)) |
27 | 14, 26 | sylibr 226 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} ≠ ∅) |
28 | | onint 7257 |
. . . . . . . . . . . . . . 15
⊢ (({𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} ⊆ On ∧ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} ≠ ∅) → ∩ {𝑥
∈ On ∣ 𝐵 ∈
(𝐴 ↑o 𝑥)} ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)}) |
29 | 25, 27, 28 | sylancr 583 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → ∩ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)}) |
30 | | eleq1 2895 |
. . . . . . . . . . . . . 14
⊢ (∩ {𝑥
∈ On ∣ 𝐵 ∈
(𝐴 ↑o 𝑥)} = ∅ → (∩ {𝑥
∈ On ∣ 𝐵 ∈
(𝐴 ↑o 𝑥)} ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} ↔ ∅ ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)})) |
31 | 29, 30 | syl5ibcom 237 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → (∩ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} = ∅ → ∅ ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)})) |
32 | | oveq2 6914 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = ∅ → (𝐴 ↑o 𝑥) = (𝐴 ↑o
∅)) |
33 | 32 | eleq2d 2893 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = ∅ → (𝐵 ∈ (𝐴 ↑o 𝑥) ↔ 𝐵 ∈ (𝐴 ↑o
∅))) |
34 | 33 | elrab 3586 |
. . . . . . . . . . . . . . 15
⊢ (∅
∈ {𝑥 ∈ On ∣
𝐵 ∈ (𝐴 ↑o 𝑥)} ↔ (∅ ∈ On ∧ 𝐵 ∈ (𝐴 ↑o
∅))) |
35 | 34 | simprbi 492 |
. . . . . . . . . . . . . 14
⊢ (∅
∈ {𝑥 ∈ On ∣
𝐵 ∈ (𝐴 ↑o 𝑥)} → 𝐵 ∈ (𝐴 ↑o
∅)) |
36 | | eldifi 3960 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ (On ∖
2o) → 𝐴
∈ On) |
37 | 36 | adantr 474 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → 𝐴 ∈ On) |
38 | | oe0 7870 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ On → (𝐴 ↑o ∅) =
1o) |
39 | 37, 38 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → (𝐴 ↑o ∅) =
1o) |
40 | 39 | eleq2d 2893 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → (𝐵 ∈ (𝐴 ↑o ∅) ↔ 𝐵 ∈
1o)) |
41 | | el1o 7847 |
. . . . . . . . . . . . . . 15
⊢ (𝐵 ∈ 1o ↔
𝐵 =
∅) |
42 | 40, 41 | syl6bb 279 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → (𝐵 ∈ (𝐴 ↑o ∅) ↔ 𝐵 = ∅)) |
43 | 35, 42 | syl5ib 236 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → (∅ ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} → 𝐵 = ∅)) |
44 | 31, 43 | syld 47 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → (∩ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} = ∅ → 𝐵 = ∅)) |
45 | 44 | necon3ad 3013 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → (𝐵 ≠ ∅ → ¬ ∩ {𝑥
∈ On ∣ 𝐵 ∈
(𝐴 ↑o 𝑥)} = ∅)) |
46 | 24, 45 | mpd 15 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → ¬ ∩
{𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} = ∅) |
47 | | limuni 6024 |
. . . . . . . . . . . . . . . . 17
⊢ (Lim
∩ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} → ∩ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} = ∪ ∩ {𝑥
∈ On ∣ 𝐵 ∈
(𝐴 ↑o 𝑥)}) |
48 | 47, 1 | syl6eqr 2880 |
. . . . . . . . . . . . . . . 16
⊢ (Lim
∩ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} → ∩ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} = 𝑋) |
49 | 48 | adantl 475 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ Lim ∩
{𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)}) → ∩
{𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} = 𝑋) |
50 | 29 | adantr 474 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ Lim ∩
{𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)}) → ∩
{𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)}) |
51 | 49, 50 | eqeltrrd 2908 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ Lim ∩
{𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)}) → 𝑋 ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)}) |
52 | | oveq2 6914 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑋 → (𝐴 ↑o 𝑦) = (𝐴 ↑o 𝑋)) |
53 | 52 | eleq2d 2893 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑋 → (𝐵 ∈ (𝐴 ↑o 𝑦) ↔ 𝐵 ∈ (𝐴 ↑o 𝑋))) |
54 | | oveq2 6914 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑦 → (𝐴 ↑o 𝑥) = (𝐴 ↑o 𝑦)) |
55 | 54 | eleq2d 2893 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑦 → (𝐵 ∈ (𝐴 ↑o 𝑥) ↔ 𝐵 ∈ (𝐴 ↑o 𝑦))) |
56 | 55 | cbvrabv 3413 |
. . . . . . . . . . . . . . . 16
⊢ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} = {𝑦 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑦)} |
57 | 53, 56 | elrab2 3590 |
. . . . . . . . . . . . . . 15
⊢ (𝑋 ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} ↔ (𝑋 ∈ On ∧ 𝐵 ∈ (𝐴 ↑o 𝑋))) |
58 | 57 | simprbi 492 |
. . . . . . . . . . . . . 14
⊢ (𝑋 ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} → 𝐵 ∈ (𝐴 ↑o 𝑋)) |
59 | 51, 58 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ Lim ∩
{𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)}) → 𝐵 ∈ (𝐴 ↑o 𝑋)) |
60 | 36 | ad2antrr 719 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ Lim ∩
{𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)}) → 𝐴 ∈ On) |
61 | | limeq 5976 |
. . . . . . . . . . . . . . . . 17
⊢ (∩ {𝑥
∈ On ∣ 𝐵 ∈
(𝐴 ↑o 𝑥)} = 𝑋 → (Lim ∩
{𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} ↔ Lim 𝑋)) |
62 | 48, 61 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (Lim
∩ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} → (Lim ∩
{𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} ↔ Lim 𝑋)) |
63 | 62 | ibi 259 |
. . . . . . . . . . . . . . 15
⊢ (Lim
∩ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} → Lim 𝑋) |
64 | 19, 63 | anim12i 608 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ Lim ∩
{𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)}) → (𝑋 ∈ On ∧ Lim 𝑋)) |
65 | | dif20el 7853 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ (On ∖
2o) → ∅ ∈ 𝐴) |
66 | 65 | ad2antrr 719 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ Lim ∩
{𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)}) → ∅ ∈ 𝐴) |
67 | | oelim 7882 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ On ∧ (𝑋 ∈ On ∧ Lim 𝑋)) ∧ ∅ ∈ 𝐴) → (𝐴 ↑o 𝑋) = ∪
𝑦 ∈ 𝑋 (𝐴 ↑o 𝑦)) |
68 | 60, 64, 66, 67 | syl21anc 873 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ Lim ∩
{𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)}) → (𝐴 ↑o 𝑋) = ∪
𝑦 ∈ 𝑋 (𝐴 ↑o 𝑦)) |
69 | 59, 68 | eleqtrd 2909 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ Lim ∩
{𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)}) → 𝐵 ∈ ∪
𝑦 ∈ 𝑋 (𝐴 ↑o 𝑦)) |
70 | | eliun 4745 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈ ∪ 𝑦 ∈ 𝑋 (𝐴 ↑o 𝑦) ↔ ∃𝑦 ∈ 𝑋 𝐵 ∈ (𝐴 ↑o 𝑦)) |
71 | 69, 70 | sylib 210 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ Lim ∩
{𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)}) → ∃𝑦 ∈ 𝑋 𝐵 ∈ (𝐴 ↑o 𝑦)) |
72 | 19 | adantr 474 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ Lim ∩
{𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)}) → 𝑋 ∈ On) |
73 | | onss 7252 |
. . . . . . . . . . . . . . 15
⊢ (𝑋 ∈ On → 𝑋 ⊆ On) |
74 | 72, 73 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ Lim ∩
{𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)}) → 𝑋 ⊆ On) |
75 | 74 | sselda 3828 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ Lim ∩
{𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)}) ∧ 𝑦 ∈ 𝑋) → 𝑦 ∈ On) |
76 | 49 | eleq2d 2893 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ Lim ∩
{𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)}) → (𝑦 ∈ ∩ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} ↔ 𝑦 ∈ 𝑋)) |
77 | 76 | biimpar 471 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ Lim ∩
{𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)}) ∧ 𝑦 ∈ 𝑋) → 𝑦 ∈ ∩ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)}) |
78 | 55 | onnminsb 7266 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ On → (𝑦 ∈ ∩ {𝑥
∈ On ∣ 𝐵 ∈
(𝐴 ↑o 𝑥)} → ¬ 𝐵 ∈ (𝐴 ↑o 𝑦))) |
79 | 75, 77, 78 | sylc 65 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ Lim ∩
{𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)}) ∧ 𝑦 ∈ 𝑋) → ¬ 𝐵 ∈ (𝐴 ↑o 𝑦)) |
80 | 79 | nrexdv 3210 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ Lim ∩
{𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)}) → ¬ ∃𝑦 ∈ 𝑋 𝐵 ∈ (𝐴 ↑o 𝑦)) |
81 | 71, 80 | pm2.65da 853 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → ¬ Lim ∩ {𝑥
∈ On ∣ 𝐵 ∈
(𝐴 ↑o 𝑥)}) |
82 | | ioran 1013 |
. . . . . . . . . 10
⊢ (¬
(∩ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} = ∅ ∨ Lim ∩ {𝑥
∈ On ∣ 𝐵 ∈
(𝐴 ↑o 𝑥)}) ↔ (¬ ∩ {𝑥
∈ On ∣ 𝐵 ∈
(𝐴 ↑o 𝑥)} = ∅ ∧ ¬ Lim
∩ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)})) |
83 | 46, 81, 82 | sylanbrc 580 |
. . . . . . . . 9
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → ¬ (∩
{𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} = ∅ ∨ Lim ∩ {𝑥
∈ On ∣ 𝐵 ∈
(𝐴 ↑o 𝑥)})) |
84 | | eloni 5974 |
. . . . . . . . . 10
⊢ (∩ {𝑥
∈ On ∣ 𝐵 ∈
(𝐴 ↑o 𝑥)} ∈ On → Ord ∩ {𝑥
∈ On ∣ 𝐵 ∈
(𝐴 ↑o 𝑥)}) |
85 | | unizlim 6080 |
. . . . . . . . . 10
⊢ (Ord
∩ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} → (∩
{𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} = ∪ ∩ {𝑥
∈ On ∣ 𝐵 ∈
(𝐴 ↑o 𝑥)} ↔ (∩ {𝑥
∈ On ∣ 𝐵 ∈
(𝐴 ↑o 𝑥)} = ∅ ∨ Lim ∩ {𝑥
∈ On ∣ 𝐵 ∈
(𝐴 ↑o 𝑥)}))) |
86 | 16, 84, 85 | 3syl 18 |
. . . . . . . . 9
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → (∩ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} = ∪ ∩ {𝑥
∈ On ∣ 𝐵 ∈
(𝐴 ↑o 𝑥)} ↔ (∩ {𝑥
∈ On ∣ 𝐵 ∈
(𝐴 ↑o 𝑥)} = ∅ ∨ Lim ∩ {𝑥
∈ On ∣ 𝐵 ∈
(𝐴 ↑o 𝑥)}))) |
87 | 83, 86 | mtbird 317 |
. . . . . . . 8
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → ¬ ∩
{𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} = ∪ ∩ {𝑥
∈ On ∣ 𝐵 ∈
(𝐴 ↑o 𝑥)}) |
88 | | orduniorsuc 7292 |
. . . . . . . . . 10
⊢ (Ord
∩ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} → (∩
{𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} = ∪ ∩ {𝑥
∈ On ∣ 𝐵 ∈
(𝐴 ↑o 𝑥)} ∨ ∩ {𝑥
∈ On ∣ 𝐵 ∈
(𝐴 ↑o 𝑥)} = suc ∪ ∩ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)})) |
89 | 16, 84, 88 | 3syl 18 |
. . . . . . . . 9
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → (∩ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} = ∪ ∩ {𝑥
∈ On ∣ 𝐵 ∈
(𝐴 ↑o 𝑥)} ∨ ∩ {𝑥
∈ On ∣ 𝐵 ∈
(𝐴 ↑o 𝑥)} = suc ∪ ∩ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)})) |
90 | 89 | ord 897 |
. . . . . . . 8
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → (¬ ∩
{𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} = ∪ ∩ {𝑥
∈ On ∣ 𝐵 ∈
(𝐴 ↑o 𝑥)} → ∩ {𝑥
∈ On ∣ 𝐵 ∈
(𝐴 ↑o 𝑥)} = suc ∪ ∩ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)})) |
91 | 87, 90 | mpd 15 |
. . . . . . 7
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → ∩ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} = suc ∪ ∩ {𝑥
∈ On ∣ 𝐵 ∈
(𝐴 ↑o 𝑥)}) |
92 | | suceq 6029 |
. . . . . . . 8
⊢ (𝑋 = ∪
∩ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} → suc 𝑋 = suc ∪ ∩ {𝑥
∈ On ∣ 𝐵 ∈
(𝐴 ↑o 𝑥)}) |
93 | 1, 92 | ax-mp 5 |
. . . . . . 7
⊢ suc 𝑋 = suc ∪ ∩ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} |
94 | 91, 93 | syl6reqr 2881 |
. . . . . 6
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → suc 𝑋 = ∩ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)}) |
95 | 21, 94 | eleqtrd 2909 |
. . . . 5
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → 𝑋 ∈ ∩ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)}) |
96 | 56 | inteqi 4702 |
. . . . 5
⊢ ∩ {𝑥
∈ On ∣ 𝐵 ∈
(𝐴 ↑o 𝑥)} = ∩ {𝑦
∈ On ∣ 𝐵 ∈
(𝐴 ↑o 𝑦)} |
97 | 95, 96 | syl6eleq 2917 |
. . . 4
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → 𝑋 ∈ ∩ {𝑦 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑦)}) |
98 | 53 | onnminsb 7266 |
. . . 4
⊢ (𝑋 ∈ On → (𝑋 ∈ ∩ {𝑦
∈ On ∣ 𝐵 ∈
(𝐴 ↑o 𝑦)} → ¬ 𝐵 ∈ (𝐴 ↑o 𝑋))) |
99 | 19, 97, 98 | sylc 65 |
. . 3
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → ¬ 𝐵 ∈ (𝐴 ↑o 𝑋)) |
100 | | oecl 7885 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝑋 ∈ On) → (𝐴 ↑o 𝑋) ∈ On) |
101 | 37, 19, 100 | syl2anc 581 |
. . . 4
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → (𝐴 ↑o 𝑋) ∈ On) |
102 | | ontri1 5998 |
. . . 4
⊢ (((𝐴 ↑o 𝑋) ∈ On ∧ 𝐵 ∈ On) → ((𝐴 ↑o 𝑋) ⊆ 𝐵 ↔ ¬ 𝐵 ∈ (𝐴 ↑o 𝑋))) |
103 | 101, 3, 102 | syl2anc 581 |
. . 3
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → ((𝐴 ↑o 𝑋) ⊆ 𝐵 ↔ ¬ 𝐵 ∈ (𝐴 ↑o 𝑋))) |
104 | 99, 103 | mpbird 249 |
. 2
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → (𝐴 ↑o 𝑋) ⊆ 𝐵) |
105 | 94, 29 | eqeltrd 2907 |
. . 3
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → suc 𝑋 ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)}) |
106 | | oveq2 6914 |
. . . . . 6
⊢ (𝑦 = suc 𝑋 → (𝐴 ↑o 𝑦) = (𝐴 ↑o suc 𝑋)) |
107 | 106 | eleq2d 2893 |
. . . . 5
⊢ (𝑦 = suc 𝑋 → (𝐵 ∈ (𝐴 ↑o 𝑦) ↔ 𝐵 ∈ (𝐴 ↑o suc 𝑋))) |
108 | 107, 56 | elrab2 3590 |
. . . 4
⊢ (suc
𝑋 ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} ↔ (suc 𝑋 ∈ On ∧ 𝐵 ∈ (𝐴 ↑o suc 𝑋))) |
109 | 108 | simprbi 492 |
. . 3
⊢ (suc
𝑋 ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} → 𝐵 ∈ (𝐴 ↑o suc 𝑋)) |
110 | 105, 109 | syl 17 |
. 2
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → 𝐵 ∈ (𝐴 ↑o suc 𝑋)) |
111 | 19, 104, 110 | 3jca 1164 |
1
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → (𝑋 ∈ On ∧ (𝐴 ↑o 𝑋) ⊆ 𝐵 ∧ 𝐵 ∈ (𝐴 ↑o suc 𝑋))) |