Step |
Hyp |
Ref |
Expression |
1 |
|
limelon |
⊢ ( ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) → 𝐵 ∈ On ) |
2 |
|
0ellim |
⊢ ( Lim 𝐵 → ∅ ∈ 𝐵 ) |
3 |
2
|
adantl |
⊢ ( ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) → ∅ ∈ 𝐵 ) |
4 |
|
oe0m1 |
⊢ ( 𝐵 ∈ On → ( ∅ ∈ 𝐵 ↔ ( ∅ ↑o 𝐵 ) = ∅ ) ) |
5 |
4
|
biimpa |
⊢ ( ( 𝐵 ∈ On ∧ ∅ ∈ 𝐵 ) → ( ∅ ↑o 𝐵 ) = ∅ ) |
6 |
1 3 5
|
syl2anc |
⊢ ( ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) → ( ∅ ↑o 𝐵 ) = ∅ ) |
7 |
|
eldif |
⊢ ( 𝑥 ∈ ( 𝐵 ∖ 1o ) ↔ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 1o ) ) |
8 |
|
limord |
⊢ ( Lim 𝐵 → Ord 𝐵 ) |
9 |
|
ordelon |
⊢ ( ( Ord 𝐵 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ On ) |
10 |
8 9
|
sylan |
⊢ ( ( Lim 𝐵 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ On ) |
11 |
|
on0eln0 |
⊢ ( 𝑥 ∈ On → ( ∅ ∈ 𝑥 ↔ 𝑥 ≠ ∅ ) ) |
12 |
|
el1o |
⊢ ( 𝑥 ∈ 1o ↔ 𝑥 = ∅ ) |
13 |
12
|
necon3bbii |
⊢ ( ¬ 𝑥 ∈ 1o ↔ 𝑥 ≠ ∅ ) |
14 |
11 13
|
bitr4di |
⊢ ( 𝑥 ∈ On → ( ∅ ∈ 𝑥 ↔ ¬ 𝑥 ∈ 1o ) ) |
15 |
|
oe0m1 |
⊢ ( 𝑥 ∈ On → ( ∅ ∈ 𝑥 ↔ ( ∅ ↑o 𝑥 ) = ∅ ) ) |
16 |
15
|
biimpd |
⊢ ( 𝑥 ∈ On → ( ∅ ∈ 𝑥 → ( ∅ ↑o 𝑥 ) = ∅ ) ) |
17 |
14 16
|
sylbird |
⊢ ( 𝑥 ∈ On → ( ¬ 𝑥 ∈ 1o → ( ∅ ↑o 𝑥 ) = ∅ ) ) |
18 |
10 17
|
syl |
⊢ ( ( Lim 𝐵 ∧ 𝑥 ∈ 𝐵 ) → ( ¬ 𝑥 ∈ 1o → ( ∅ ↑o 𝑥 ) = ∅ ) ) |
19 |
18
|
impr |
⊢ ( ( Lim 𝐵 ∧ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 1o ) ) → ( ∅ ↑o 𝑥 ) = ∅ ) |
20 |
7 19
|
sylan2b |
⊢ ( ( Lim 𝐵 ∧ 𝑥 ∈ ( 𝐵 ∖ 1o ) ) → ( ∅ ↑o 𝑥 ) = ∅ ) |
21 |
20
|
iuneq2dv |
⊢ ( Lim 𝐵 → ∪ 𝑥 ∈ ( 𝐵 ∖ 1o ) ( ∅ ↑o 𝑥 ) = ∪ 𝑥 ∈ ( 𝐵 ∖ 1o ) ∅ ) |
22 |
|
df-1o |
⊢ 1o = suc ∅ |
23 |
|
limsuc |
⊢ ( Lim 𝐵 → ( ∅ ∈ 𝐵 ↔ suc ∅ ∈ 𝐵 ) ) |
24 |
2 23
|
mpbid |
⊢ ( Lim 𝐵 → suc ∅ ∈ 𝐵 ) |
25 |
22 24
|
eqeltrid |
⊢ ( Lim 𝐵 → 1o ∈ 𝐵 ) |
26 |
|
1on |
⊢ 1o ∈ On |
27 |
26
|
onirri |
⊢ ¬ 1o ∈ 1o |
28 |
|
eldif |
⊢ ( 1o ∈ ( 𝐵 ∖ 1o ) ↔ ( 1o ∈ 𝐵 ∧ ¬ 1o ∈ 1o ) ) |
29 |
25 27 28
|
sylanblrc |
⊢ ( Lim 𝐵 → 1o ∈ ( 𝐵 ∖ 1o ) ) |
30 |
|
ne0i |
⊢ ( 1o ∈ ( 𝐵 ∖ 1o ) → ( 𝐵 ∖ 1o ) ≠ ∅ ) |
31 |
|
iunconst |
⊢ ( ( 𝐵 ∖ 1o ) ≠ ∅ → ∪ 𝑥 ∈ ( 𝐵 ∖ 1o ) ∅ = ∅ ) |
32 |
29 30 31
|
3syl |
⊢ ( Lim 𝐵 → ∪ 𝑥 ∈ ( 𝐵 ∖ 1o ) ∅ = ∅ ) |
33 |
21 32
|
eqtrd |
⊢ ( Lim 𝐵 → ∪ 𝑥 ∈ ( 𝐵 ∖ 1o ) ( ∅ ↑o 𝑥 ) = ∅ ) |
34 |
33
|
adantl |
⊢ ( ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) → ∪ 𝑥 ∈ ( 𝐵 ∖ 1o ) ( ∅ ↑o 𝑥 ) = ∅ ) |
35 |
6 34
|
eqtr4d |
⊢ ( ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) → ( ∅ ↑o 𝐵 ) = ∪ 𝑥 ∈ ( 𝐵 ∖ 1o ) ( ∅ ↑o 𝑥 ) ) |
36 |
|
oveq1 |
⊢ ( 𝐴 = ∅ → ( 𝐴 ↑o 𝐵 ) = ( ∅ ↑o 𝐵 ) ) |
37 |
|
oveq1 |
⊢ ( 𝐴 = ∅ → ( 𝐴 ↑o 𝑥 ) = ( ∅ ↑o 𝑥 ) ) |
38 |
37
|
iuneq2d |
⊢ ( 𝐴 = ∅ → ∪ 𝑥 ∈ ( 𝐵 ∖ 1o ) ( 𝐴 ↑o 𝑥 ) = ∪ 𝑥 ∈ ( 𝐵 ∖ 1o ) ( ∅ ↑o 𝑥 ) ) |
39 |
36 38
|
eqeq12d |
⊢ ( 𝐴 = ∅ → ( ( 𝐴 ↑o 𝐵 ) = ∪ 𝑥 ∈ ( 𝐵 ∖ 1o ) ( 𝐴 ↑o 𝑥 ) ↔ ( ∅ ↑o 𝐵 ) = ∪ 𝑥 ∈ ( 𝐵 ∖ 1o ) ( ∅ ↑o 𝑥 ) ) ) |
40 |
35 39
|
syl5ibr |
⊢ ( 𝐴 = ∅ → ( ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) → ( 𝐴 ↑o 𝐵 ) = ∪ 𝑥 ∈ ( 𝐵 ∖ 1o ) ( 𝐴 ↑o 𝑥 ) ) ) |
41 |
40
|
impcom |
⊢ ( ( ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ∧ 𝐴 = ∅ ) → ( 𝐴 ↑o 𝐵 ) = ∪ 𝑥 ∈ ( 𝐵 ∖ 1o ) ( 𝐴 ↑o 𝑥 ) ) |
42 |
|
oelim |
⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) ∧ ∅ ∈ 𝐴 ) → ( 𝐴 ↑o 𝐵 ) = ∪ 𝑦 ∈ 𝐵 ( 𝐴 ↑o 𝑦 ) ) |
43 |
|
limsuc |
⊢ ( Lim 𝐵 → ( 𝑦 ∈ 𝐵 ↔ suc 𝑦 ∈ 𝐵 ) ) |
44 |
43
|
biimpa |
⊢ ( ( Lim 𝐵 ∧ 𝑦 ∈ 𝐵 ) → suc 𝑦 ∈ 𝐵 ) |
45 |
|
nsuceq0 |
⊢ suc 𝑦 ≠ ∅ |
46 |
|
dif1o |
⊢ ( suc 𝑦 ∈ ( 𝐵 ∖ 1o ) ↔ ( suc 𝑦 ∈ 𝐵 ∧ suc 𝑦 ≠ ∅ ) ) |
47 |
44 45 46
|
sylanblrc |
⊢ ( ( Lim 𝐵 ∧ 𝑦 ∈ 𝐵 ) → suc 𝑦 ∈ ( 𝐵 ∖ 1o ) ) |
48 |
47
|
ex |
⊢ ( Lim 𝐵 → ( 𝑦 ∈ 𝐵 → suc 𝑦 ∈ ( 𝐵 ∖ 1o ) ) ) |
49 |
48
|
ad2antlr |
⊢ ( ( ( 𝐴 ∈ On ∧ Lim 𝐵 ) ∧ ∅ ∈ 𝐴 ) → ( 𝑦 ∈ 𝐵 → suc 𝑦 ∈ ( 𝐵 ∖ 1o ) ) ) |
50 |
|
sssucid |
⊢ 𝑦 ⊆ suc 𝑦 |
51 |
|
ordelon |
⊢ ( ( Ord 𝐵 ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ On ) |
52 |
8 51
|
sylan |
⊢ ( ( Lim 𝐵 ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ On ) |
53 |
|
suceloni |
⊢ ( 𝑦 ∈ On → suc 𝑦 ∈ On ) |
54 |
52 53
|
jccir |
⊢ ( ( Lim 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑦 ∈ On ∧ suc 𝑦 ∈ On ) ) |
55 |
|
id |
⊢ ( ( 𝑦 ∈ On ∧ suc 𝑦 ∈ On ∧ 𝐴 ∈ On ) → ( 𝑦 ∈ On ∧ suc 𝑦 ∈ On ∧ 𝐴 ∈ On ) ) |
56 |
55
|
3expa |
⊢ ( ( ( 𝑦 ∈ On ∧ suc 𝑦 ∈ On ) ∧ 𝐴 ∈ On ) → ( 𝑦 ∈ On ∧ suc 𝑦 ∈ On ∧ 𝐴 ∈ On ) ) |
57 |
56
|
ancoms |
⊢ ( ( 𝐴 ∈ On ∧ ( 𝑦 ∈ On ∧ suc 𝑦 ∈ On ) ) → ( 𝑦 ∈ On ∧ suc 𝑦 ∈ On ∧ 𝐴 ∈ On ) ) |
58 |
54 57
|
sylan2 |
⊢ ( ( 𝐴 ∈ On ∧ ( Lim 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑦 ∈ On ∧ suc 𝑦 ∈ On ∧ 𝐴 ∈ On ) ) |
59 |
58
|
anassrs |
⊢ ( ( ( 𝐴 ∈ On ∧ Lim 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑦 ∈ On ∧ suc 𝑦 ∈ On ∧ 𝐴 ∈ On ) ) |
60 |
|
oewordi |
⊢ ( ( ( 𝑦 ∈ On ∧ suc 𝑦 ∈ On ∧ 𝐴 ∈ On ) ∧ ∅ ∈ 𝐴 ) → ( 𝑦 ⊆ suc 𝑦 → ( 𝐴 ↑o 𝑦 ) ⊆ ( 𝐴 ↑o suc 𝑦 ) ) ) |
61 |
59 60
|
sylan |
⊢ ( ( ( ( 𝐴 ∈ On ∧ Lim 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ∅ ∈ 𝐴 ) → ( 𝑦 ⊆ suc 𝑦 → ( 𝐴 ↑o 𝑦 ) ⊆ ( 𝐴 ↑o suc 𝑦 ) ) ) |
62 |
61
|
an32s |
⊢ ( ( ( ( 𝐴 ∈ On ∧ Lim 𝐵 ) ∧ ∅ ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑦 ⊆ suc 𝑦 → ( 𝐴 ↑o 𝑦 ) ⊆ ( 𝐴 ↑o suc 𝑦 ) ) ) |
63 |
50 62
|
mpi |
⊢ ( ( ( ( 𝐴 ∈ On ∧ Lim 𝐵 ) ∧ ∅ ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝐴 ↑o 𝑦 ) ⊆ ( 𝐴 ↑o suc 𝑦 ) ) |
64 |
63
|
ex |
⊢ ( ( ( 𝐴 ∈ On ∧ Lim 𝐵 ) ∧ ∅ ∈ 𝐴 ) → ( 𝑦 ∈ 𝐵 → ( 𝐴 ↑o 𝑦 ) ⊆ ( 𝐴 ↑o suc 𝑦 ) ) ) |
65 |
49 64
|
jcad |
⊢ ( ( ( 𝐴 ∈ On ∧ Lim 𝐵 ) ∧ ∅ ∈ 𝐴 ) → ( 𝑦 ∈ 𝐵 → ( suc 𝑦 ∈ ( 𝐵 ∖ 1o ) ∧ ( 𝐴 ↑o 𝑦 ) ⊆ ( 𝐴 ↑o suc 𝑦 ) ) ) ) |
66 |
|
oveq2 |
⊢ ( 𝑥 = suc 𝑦 → ( 𝐴 ↑o 𝑥 ) = ( 𝐴 ↑o suc 𝑦 ) ) |
67 |
66
|
sseq2d |
⊢ ( 𝑥 = suc 𝑦 → ( ( 𝐴 ↑o 𝑦 ) ⊆ ( 𝐴 ↑o 𝑥 ) ↔ ( 𝐴 ↑o 𝑦 ) ⊆ ( 𝐴 ↑o suc 𝑦 ) ) ) |
68 |
67
|
rspcev |
⊢ ( ( suc 𝑦 ∈ ( 𝐵 ∖ 1o ) ∧ ( 𝐴 ↑o 𝑦 ) ⊆ ( 𝐴 ↑o suc 𝑦 ) ) → ∃ 𝑥 ∈ ( 𝐵 ∖ 1o ) ( 𝐴 ↑o 𝑦 ) ⊆ ( 𝐴 ↑o 𝑥 ) ) |
69 |
65 68
|
syl6 |
⊢ ( ( ( 𝐴 ∈ On ∧ Lim 𝐵 ) ∧ ∅ ∈ 𝐴 ) → ( 𝑦 ∈ 𝐵 → ∃ 𝑥 ∈ ( 𝐵 ∖ 1o ) ( 𝐴 ↑o 𝑦 ) ⊆ ( 𝐴 ↑o 𝑥 ) ) ) |
70 |
69
|
ralrimiv |
⊢ ( ( ( 𝐴 ∈ On ∧ Lim 𝐵 ) ∧ ∅ ∈ 𝐴 ) → ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ ( 𝐵 ∖ 1o ) ( 𝐴 ↑o 𝑦 ) ⊆ ( 𝐴 ↑o 𝑥 ) ) |
71 |
|
iunss2 |
⊢ ( ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ ( 𝐵 ∖ 1o ) ( 𝐴 ↑o 𝑦 ) ⊆ ( 𝐴 ↑o 𝑥 ) → ∪ 𝑦 ∈ 𝐵 ( 𝐴 ↑o 𝑦 ) ⊆ ∪ 𝑥 ∈ ( 𝐵 ∖ 1o ) ( 𝐴 ↑o 𝑥 ) ) |
72 |
70 71
|
syl |
⊢ ( ( ( 𝐴 ∈ On ∧ Lim 𝐵 ) ∧ ∅ ∈ 𝐴 ) → ∪ 𝑦 ∈ 𝐵 ( 𝐴 ↑o 𝑦 ) ⊆ ∪ 𝑥 ∈ ( 𝐵 ∖ 1o ) ( 𝐴 ↑o 𝑥 ) ) |
73 |
|
difss |
⊢ ( 𝐵 ∖ 1o ) ⊆ 𝐵 |
74 |
|
iunss1 |
⊢ ( ( 𝐵 ∖ 1o ) ⊆ 𝐵 → ∪ 𝑥 ∈ ( 𝐵 ∖ 1o ) ( 𝐴 ↑o 𝑥 ) ⊆ ∪ 𝑥 ∈ 𝐵 ( 𝐴 ↑o 𝑥 ) ) |
75 |
73 74
|
ax-mp |
⊢ ∪ 𝑥 ∈ ( 𝐵 ∖ 1o ) ( 𝐴 ↑o 𝑥 ) ⊆ ∪ 𝑥 ∈ 𝐵 ( 𝐴 ↑o 𝑥 ) |
76 |
|
oveq2 |
⊢ ( 𝑥 = 𝑦 → ( 𝐴 ↑o 𝑥 ) = ( 𝐴 ↑o 𝑦 ) ) |
77 |
76
|
cbviunv |
⊢ ∪ 𝑥 ∈ 𝐵 ( 𝐴 ↑o 𝑥 ) = ∪ 𝑦 ∈ 𝐵 ( 𝐴 ↑o 𝑦 ) |
78 |
75 77
|
sseqtri |
⊢ ∪ 𝑥 ∈ ( 𝐵 ∖ 1o ) ( 𝐴 ↑o 𝑥 ) ⊆ ∪ 𝑦 ∈ 𝐵 ( 𝐴 ↑o 𝑦 ) |
79 |
78
|
a1i |
⊢ ( ( ( 𝐴 ∈ On ∧ Lim 𝐵 ) ∧ ∅ ∈ 𝐴 ) → ∪ 𝑥 ∈ ( 𝐵 ∖ 1o ) ( 𝐴 ↑o 𝑥 ) ⊆ ∪ 𝑦 ∈ 𝐵 ( 𝐴 ↑o 𝑦 ) ) |
80 |
72 79
|
eqssd |
⊢ ( ( ( 𝐴 ∈ On ∧ Lim 𝐵 ) ∧ ∅ ∈ 𝐴 ) → ∪ 𝑦 ∈ 𝐵 ( 𝐴 ↑o 𝑦 ) = ∪ 𝑥 ∈ ( 𝐵 ∖ 1o ) ( 𝐴 ↑o 𝑥 ) ) |
81 |
80
|
adantlrl |
⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) ∧ ∅ ∈ 𝐴 ) → ∪ 𝑦 ∈ 𝐵 ( 𝐴 ↑o 𝑦 ) = ∪ 𝑥 ∈ ( 𝐵 ∖ 1o ) ( 𝐴 ↑o 𝑥 ) ) |
82 |
42 81
|
eqtrd |
⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) ∧ ∅ ∈ 𝐴 ) → ( 𝐴 ↑o 𝐵 ) = ∪ 𝑥 ∈ ( 𝐵 ∖ 1o ) ( 𝐴 ↑o 𝑥 ) ) |
83 |
41 82
|
oe0lem |
⊢ ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) → ( 𝐴 ↑o 𝐵 ) = ∪ 𝑥 ∈ ( 𝐵 ∖ 1o ) ( 𝐴 ↑o 𝑥 ) ) |