| Step |
Hyp |
Ref |
Expression |
| 1 |
|
n0i |
⊢ ( 𝐴 ∈ ( ω ↑o 𝐶 ) → ¬ ( ω ↑o 𝐶 ) = ∅ ) |
| 2 |
|
fnoe |
⊢ ↑o Fn ( On × On ) |
| 3 |
|
fndm |
⊢ ( ↑o Fn ( On × On ) → dom ↑o = ( On × On ) ) |
| 4 |
2 3
|
ax-mp |
⊢ dom ↑o = ( On × On ) |
| 5 |
4
|
ndmov |
⊢ ( ¬ ( ω ∈ On ∧ 𝐶 ∈ On ) → ( ω ↑o 𝐶 ) = ∅ ) |
| 6 |
1 5
|
nsyl2 |
⊢ ( 𝐴 ∈ ( ω ↑o 𝐶 ) → ( ω ∈ On ∧ 𝐶 ∈ On ) ) |
| 7 |
6
|
ad2antrr |
⊢ ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) → ( ω ∈ On ∧ 𝐶 ∈ On ) ) |
| 8 |
|
oecl |
⊢ ( ( ω ∈ On ∧ 𝐶 ∈ On ) → ( ω ↑o 𝐶 ) ∈ On ) |
| 9 |
7 8
|
syl |
⊢ ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) → ( ω ↑o 𝐶 ) ∈ On ) |
| 10 |
|
simplr |
⊢ ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) → 𝐵 ∈ On ) |
| 11 |
|
simpr |
⊢ ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) → ( ω ↑o 𝐶 ) ⊆ 𝐵 ) |
| 12 |
|
oawordeu |
⊢ ( ( ( ( ω ↑o 𝐶 ) ∈ On ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) → ∃! 𝑥 ∈ On ( ( ω ↑o 𝐶 ) +o 𝑥 ) = 𝐵 ) |
| 13 |
9 10 11 12
|
syl21anc |
⊢ ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) → ∃! 𝑥 ∈ On ( ( ω ↑o 𝐶 ) +o 𝑥 ) = 𝐵 ) |
| 14 |
|
reurex |
⊢ ( ∃! 𝑥 ∈ On ( ( ω ↑o 𝐶 ) +o 𝑥 ) = 𝐵 → ∃ 𝑥 ∈ On ( ( ω ↑o 𝐶 ) +o 𝑥 ) = 𝐵 ) |
| 15 |
13 14
|
syl |
⊢ ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) → ∃ 𝑥 ∈ On ( ( ω ↑o 𝐶 ) +o 𝑥 ) = 𝐵 ) |
| 16 |
|
simpll |
⊢ ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) → 𝐴 ∈ ( ω ↑o 𝐶 ) ) |
| 17 |
|
onelon |
⊢ ( ( ( ω ↑o 𝐶 ) ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝐶 ) ) → 𝐴 ∈ On ) |
| 18 |
9 16 17
|
syl2anc |
⊢ ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) → 𝐴 ∈ On ) |
| 19 |
18
|
adantr |
⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ 𝑥 ∈ On ) → 𝐴 ∈ On ) |
| 20 |
9
|
adantr |
⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ 𝑥 ∈ On ) → ( ω ↑o 𝐶 ) ∈ On ) |
| 21 |
|
simpr |
⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ 𝑥 ∈ On ) → 𝑥 ∈ On ) |
| 22 |
|
oaass |
⊢ ( ( 𝐴 ∈ On ∧ ( ω ↑o 𝐶 ) ∈ On ∧ 𝑥 ∈ On ) → ( ( 𝐴 +o ( ω ↑o 𝐶 ) ) +o 𝑥 ) = ( 𝐴 +o ( ( ω ↑o 𝐶 ) +o 𝑥 ) ) ) |
| 23 |
19 20 21 22
|
syl3anc |
⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ 𝑥 ∈ On ) → ( ( 𝐴 +o ( ω ↑o 𝐶 ) ) +o 𝑥 ) = ( 𝐴 +o ( ( ω ↑o 𝐶 ) +o 𝑥 ) ) ) |
| 24 |
7
|
simprd |
⊢ ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) → 𝐶 ∈ On ) |
| 25 |
|
eloni |
⊢ ( 𝐶 ∈ On → Ord 𝐶 ) |
| 26 |
24 25
|
syl |
⊢ ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) → Ord 𝐶 ) |
| 27 |
|
ordzsl |
⊢ ( Ord 𝐶 ↔ ( 𝐶 = ∅ ∨ ∃ 𝑥 ∈ On 𝐶 = suc 𝑥 ∨ Lim 𝐶 ) ) |
| 28 |
26 27
|
sylib |
⊢ ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) → ( 𝐶 = ∅ ∨ ∃ 𝑥 ∈ On 𝐶 = suc 𝑥 ∨ Lim 𝐶 ) ) |
| 29 |
|
simplll |
⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ 𝐶 = ∅ ) → 𝐴 ∈ ( ω ↑o 𝐶 ) ) |
| 30 |
|
oveq2 |
⊢ ( 𝐶 = ∅ → ( ω ↑o 𝐶 ) = ( ω ↑o ∅ ) ) |
| 31 |
7
|
simpld |
⊢ ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) → ω ∈ On ) |
| 32 |
|
oe0 |
⊢ ( ω ∈ On → ( ω ↑o ∅ ) = 1o ) |
| 33 |
31 32
|
syl |
⊢ ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) → ( ω ↑o ∅ ) = 1o ) |
| 34 |
30 33
|
sylan9eqr |
⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ 𝐶 = ∅ ) → ( ω ↑o 𝐶 ) = 1o ) |
| 35 |
29 34
|
eleqtrd |
⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ 𝐶 = ∅ ) → 𝐴 ∈ 1o ) |
| 36 |
|
el1o |
⊢ ( 𝐴 ∈ 1o ↔ 𝐴 = ∅ ) |
| 37 |
35 36
|
sylib |
⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ 𝐶 = ∅ ) → 𝐴 = ∅ ) |
| 38 |
37
|
oveq1d |
⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ 𝐶 = ∅ ) → ( 𝐴 +o ( ω ↑o 𝐶 ) ) = ( ∅ +o ( ω ↑o 𝐶 ) ) ) |
| 39 |
9
|
adantr |
⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ 𝐶 = ∅ ) → ( ω ↑o 𝐶 ) ∈ On ) |
| 40 |
|
oa0r |
⊢ ( ( ω ↑o 𝐶 ) ∈ On → ( ∅ +o ( ω ↑o 𝐶 ) ) = ( ω ↑o 𝐶 ) ) |
| 41 |
39 40
|
syl |
⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ 𝐶 = ∅ ) → ( ∅ +o ( ω ↑o 𝐶 ) ) = ( ω ↑o 𝐶 ) ) |
| 42 |
38 41
|
eqtrd |
⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ 𝐶 = ∅ ) → ( 𝐴 +o ( ω ↑o 𝐶 ) ) = ( ω ↑o 𝐶 ) ) |
| 43 |
42
|
ex |
⊢ ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) → ( 𝐶 = ∅ → ( 𝐴 +o ( ω ↑o 𝐶 ) ) = ( ω ↑o 𝐶 ) ) ) |
| 44 |
31
|
adantr |
⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) → ω ∈ On ) |
| 45 |
|
simprl |
⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) → 𝑥 ∈ On ) |
| 46 |
|
oecl |
⊢ ( ( ω ∈ On ∧ 𝑥 ∈ On ) → ( ω ↑o 𝑥 ) ∈ On ) |
| 47 |
44 45 46
|
syl2anc |
⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) → ( ω ↑o 𝑥 ) ∈ On ) |
| 48 |
|
limom |
⊢ Lim ω |
| 49 |
44 48
|
jctir |
⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) → ( ω ∈ On ∧ Lim ω ) ) |
| 50 |
|
simplll |
⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) → 𝐴 ∈ ( ω ↑o 𝐶 ) ) |
| 51 |
|
simprr |
⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) → 𝐶 = suc 𝑥 ) |
| 52 |
51
|
oveq2d |
⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) → ( ω ↑o 𝐶 ) = ( ω ↑o suc 𝑥 ) ) |
| 53 |
|
oesuc |
⊢ ( ( ω ∈ On ∧ 𝑥 ∈ On ) → ( ω ↑o suc 𝑥 ) = ( ( ω ↑o 𝑥 ) ·o ω ) ) |
| 54 |
44 45 53
|
syl2anc |
⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) → ( ω ↑o suc 𝑥 ) = ( ( ω ↑o 𝑥 ) ·o ω ) ) |
| 55 |
52 54
|
eqtrd |
⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) → ( ω ↑o 𝐶 ) = ( ( ω ↑o 𝑥 ) ·o ω ) ) |
| 56 |
50 55
|
eleqtrd |
⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) → 𝐴 ∈ ( ( ω ↑o 𝑥 ) ·o ω ) ) |
| 57 |
|
omordlim |
⊢ ( ( ( ( ω ↑o 𝑥 ) ∈ On ∧ ( ω ∈ On ∧ Lim ω ) ) ∧ 𝐴 ∈ ( ( ω ↑o 𝑥 ) ·o ω ) ) → ∃ 𝑦 ∈ ω 𝐴 ∈ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ) |
| 58 |
47 49 56 57
|
syl21anc |
⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) → ∃ 𝑦 ∈ ω 𝐴 ∈ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ) |
| 59 |
47
|
adantr |
⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) ∧ ( 𝑦 ∈ ω ∧ 𝐴 ∈ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ) ) → ( ω ↑o 𝑥 ) ∈ On ) |
| 60 |
|
nnon |
⊢ ( 𝑦 ∈ ω → 𝑦 ∈ On ) |
| 61 |
60
|
ad2antrl |
⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) ∧ ( 𝑦 ∈ ω ∧ 𝐴 ∈ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ) ) → 𝑦 ∈ On ) |
| 62 |
|
omcl |
⊢ ( ( ( ω ↑o 𝑥 ) ∈ On ∧ 𝑦 ∈ On ) → ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ∈ On ) |
| 63 |
59 61 62
|
syl2anc |
⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) ∧ ( 𝑦 ∈ ω ∧ 𝐴 ∈ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ) ) → ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ∈ On ) |
| 64 |
|
eloni |
⊢ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ∈ On → Ord ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ) |
| 65 |
63 64
|
syl |
⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) ∧ ( 𝑦 ∈ ω ∧ 𝐴 ∈ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ) ) → Ord ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ) |
| 66 |
|
simprr |
⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) ∧ ( 𝑦 ∈ ω ∧ 𝐴 ∈ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ) ) → 𝐴 ∈ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ) |
| 67 |
|
ordelss |
⊢ ( ( Ord ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ∧ 𝐴 ∈ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ) → 𝐴 ⊆ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ) |
| 68 |
65 66 67
|
syl2anc |
⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) ∧ ( 𝑦 ∈ ω ∧ 𝐴 ∈ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ) ) → 𝐴 ⊆ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ) |
| 69 |
18
|
ad2antrr |
⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) ∧ ( 𝑦 ∈ ω ∧ 𝐴 ∈ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ) ) → 𝐴 ∈ On ) |
| 70 |
9
|
ad2antrr |
⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) ∧ ( 𝑦 ∈ ω ∧ 𝐴 ∈ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ) ) → ( ω ↑o 𝐶 ) ∈ On ) |
| 71 |
|
oawordri |
⊢ ( ( 𝐴 ∈ On ∧ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ∈ On ∧ ( ω ↑o 𝐶 ) ∈ On ) → ( 𝐴 ⊆ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) → ( 𝐴 +o ( ω ↑o 𝐶 ) ) ⊆ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o ( ω ↑o 𝐶 ) ) ) ) |
| 72 |
69 63 70 71
|
syl3anc |
⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) ∧ ( 𝑦 ∈ ω ∧ 𝐴 ∈ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ) ) → ( 𝐴 ⊆ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) → ( 𝐴 +o ( ω ↑o 𝐶 ) ) ⊆ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o ( ω ↑o 𝐶 ) ) ) ) |
| 73 |
68 72
|
mpd |
⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) ∧ ( 𝑦 ∈ ω ∧ 𝐴 ∈ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ) ) → ( 𝐴 +o ( ω ↑o 𝐶 ) ) ⊆ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o ( ω ↑o 𝐶 ) ) ) |
| 74 |
44
|
adantr |
⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) ∧ ( 𝑦 ∈ ω ∧ 𝐴 ∈ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ) ) → ω ∈ On ) |
| 75 |
|
odi |
⊢ ( ( ( ω ↑o 𝑥 ) ∈ On ∧ 𝑦 ∈ On ∧ ω ∈ On ) → ( ( ω ↑o 𝑥 ) ·o ( 𝑦 +o ω ) ) = ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o ( ( ω ↑o 𝑥 ) ·o ω ) ) ) |
| 76 |
59 61 74 75
|
syl3anc |
⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) ∧ ( 𝑦 ∈ ω ∧ 𝐴 ∈ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ) ) → ( ( ω ↑o 𝑥 ) ·o ( 𝑦 +o ω ) ) = ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o ( ( ω ↑o 𝑥 ) ·o ω ) ) ) |
| 77 |
|
simprl |
⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) ∧ ( 𝑦 ∈ ω ∧ 𝐴 ∈ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ) ) → 𝑦 ∈ ω ) |
| 78 |
|
oaabslem |
⊢ ( ( ω ∈ On ∧ 𝑦 ∈ ω ) → ( 𝑦 +o ω ) = ω ) |
| 79 |
74 77 78
|
syl2anc |
⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) ∧ ( 𝑦 ∈ ω ∧ 𝐴 ∈ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ) ) → ( 𝑦 +o ω ) = ω ) |
| 80 |
79
|
oveq2d |
⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) ∧ ( 𝑦 ∈ ω ∧ 𝐴 ∈ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ) ) → ( ( ω ↑o 𝑥 ) ·o ( 𝑦 +o ω ) ) = ( ( ω ↑o 𝑥 ) ·o ω ) ) |
| 81 |
76 80
|
eqtr3d |
⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) ∧ ( 𝑦 ∈ ω ∧ 𝐴 ∈ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ) ) → ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o ( ( ω ↑o 𝑥 ) ·o ω ) ) = ( ( ω ↑o 𝑥 ) ·o ω ) ) |
| 82 |
55
|
adantr |
⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) ∧ ( 𝑦 ∈ ω ∧ 𝐴 ∈ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ) ) → ( ω ↑o 𝐶 ) = ( ( ω ↑o 𝑥 ) ·o ω ) ) |
| 83 |
82
|
oveq2d |
⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) ∧ ( 𝑦 ∈ ω ∧ 𝐴 ∈ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ) ) → ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o ( ω ↑o 𝐶 ) ) = ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o ( ( ω ↑o 𝑥 ) ·o ω ) ) ) |
| 84 |
81 83 82
|
3eqtr4d |
⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) ∧ ( 𝑦 ∈ ω ∧ 𝐴 ∈ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ) ) → ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o ( ω ↑o 𝐶 ) ) = ( ω ↑o 𝐶 ) ) |
| 85 |
73 84
|
sseqtrd |
⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) ∧ ( 𝑦 ∈ ω ∧ 𝐴 ∈ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ) ) → ( 𝐴 +o ( ω ↑o 𝐶 ) ) ⊆ ( ω ↑o 𝐶 ) ) |
| 86 |
58 85
|
rexlimddv |
⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) → ( 𝐴 +o ( ω ↑o 𝐶 ) ) ⊆ ( ω ↑o 𝐶 ) ) |
| 87 |
|
oaword2 |
⊢ ( ( ( ω ↑o 𝐶 ) ∈ On ∧ 𝐴 ∈ On ) → ( ω ↑o 𝐶 ) ⊆ ( 𝐴 +o ( ω ↑o 𝐶 ) ) ) |
| 88 |
9 18 87
|
syl2anc |
⊢ ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) → ( ω ↑o 𝐶 ) ⊆ ( 𝐴 +o ( ω ↑o 𝐶 ) ) ) |
| 89 |
88
|
adantr |
⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) → ( ω ↑o 𝐶 ) ⊆ ( 𝐴 +o ( ω ↑o 𝐶 ) ) ) |
| 90 |
86 89
|
eqssd |
⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) → ( 𝐴 +o ( ω ↑o 𝐶 ) ) = ( ω ↑o 𝐶 ) ) |
| 91 |
90
|
rexlimdvaa |
⊢ ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) → ( ∃ 𝑥 ∈ On 𝐶 = suc 𝑥 → ( 𝐴 +o ( ω ↑o 𝐶 ) ) = ( ω ↑o 𝐶 ) ) ) |
| 92 |
|
simplll |
⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) → 𝐴 ∈ ( ω ↑o 𝐶 ) ) |
| 93 |
31
|
adantr |
⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) → ω ∈ On ) |
| 94 |
24
|
adantr |
⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) → 𝐶 ∈ On ) |
| 95 |
|
simpr |
⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) → Lim 𝐶 ) |
| 96 |
|
oelim2 |
⊢ ( ( ω ∈ On ∧ ( 𝐶 ∈ On ∧ Lim 𝐶 ) ) → ( ω ↑o 𝐶 ) = ∪ 𝑥 ∈ ( 𝐶 ∖ 1o ) ( ω ↑o 𝑥 ) ) |
| 97 |
93 94 95 96
|
syl12anc |
⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) → ( ω ↑o 𝐶 ) = ∪ 𝑥 ∈ ( 𝐶 ∖ 1o ) ( ω ↑o 𝑥 ) ) |
| 98 |
92 97
|
eleqtrd |
⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) → 𝐴 ∈ ∪ 𝑥 ∈ ( 𝐶 ∖ 1o ) ( ω ↑o 𝑥 ) ) |
| 99 |
|
eliun |
⊢ ( 𝐴 ∈ ∪ 𝑥 ∈ ( 𝐶 ∖ 1o ) ( ω ↑o 𝑥 ) ↔ ∃ 𝑥 ∈ ( 𝐶 ∖ 1o ) 𝐴 ∈ ( ω ↑o 𝑥 ) ) |
| 100 |
98 99
|
sylib |
⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) → ∃ 𝑥 ∈ ( 𝐶 ∖ 1o ) 𝐴 ∈ ( ω ↑o 𝑥 ) ) |
| 101 |
|
eldifi |
⊢ ( 𝑥 ∈ ( 𝐶 ∖ 1o ) → 𝑥 ∈ 𝐶 ) |
| 102 |
18
|
ad2antrr |
⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) → 𝐴 ∈ On ) |
| 103 |
9
|
ad2antrr |
⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) → ( ω ↑o 𝐶 ) ∈ On ) |
| 104 |
93
|
adantr |
⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) → ω ∈ On ) |
| 105 |
|
1onn |
⊢ 1o ∈ ω |
| 106 |
|
ondif2 |
⊢ ( ω ∈ ( On ∖ 2o ) ↔ ( ω ∈ On ∧ 1o ∈ ω ) ) |
| 107 |
104 105 106
|
sylanblrc |
⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) → ω ∈ ( On ∖ 2o ) ) |
| 108 |
94
|
adantr |
⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) → 𝐶 ∈ On ) |
| 109 |
|
simplr |
⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) → Lim 𝐶 ) |
| 110 |
|
oelimcl |
⊢ ( ( ω ∈ ( On ∖ 2o ) ∧ ( 𝐶 ∈ On ∧ Lim 𝐶 ) ) → Lim ( ω ↑o 𝐶 ) ) |
| 111 |
107 108 109 110
|
syl12anc |
⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) → Lim ( ω ↑o 𝐶 ) ) |
| 112 |
|
oalim |
⊢ ( ( 𝐴 ∈ On ∧ ( ( ω ↑o 𝐶 ) ∈ On ∧ Lim ( ω ↑o 𝐶 ) ) ) → ( 𝐴 +o ( ω ↑o 𝐶 ) ) = ∪ 𝑦 ∈ ( ω ↑o 𝐶 ) ( 𝐴 +o 𝑦 ) ) |
| 113 |
102 103 111 112
|
syl12anc |
⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) → ( 𝐴 +o ( ω ↑o 𝐶 ) ) = ∪ 𝑦 ∈ ( ω ↑o 𝐶 ) ( 𝐴 +o 𝑦 ) ) |
| 114 |
|
oelim2 |
⊢ ( ( ω ∈ On ∧ ( 𝐶 ∈ On ∧ Lim 𝐶 ) ) → ( ω ↑o 𝐶 ) = ∪ 𝑧 ∈ ( 𝐶 ∖ 1o ) ( ω ↑o 𝑧 ) ) |
| 115 |
93 94 95 114
|
syl12anc |
⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) → ( ω ↑o 𝐶 ) = ∪ 𝑧 ∈ ( 𝐶 ∖ 1o ) ( ω ↑o 𝑧 ) ) |
| 116 |
115
|
eleq2d |
⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) → ( 𝑦 ∈ ( ω ↑o 𝐶 ) ↔ 𝑦 ∈ ∪ 𝑧 ∈ ( 𝐶 ∖ 1o ) ( ω ↑o 𝑧 ) ) ) |
| 117 |
|
eliun |
⊢ ( 𝑦 ∈ ∪ 𝑧 ∈ ( 𝐶 ∖ 1o ) ( ω ↑o 𝑧 ) ↔ ∃ 𝑧 ∈ ( 𝐶 ∖ 1o ) 𝑦 ∈ ( ω ↑o 𝑧 ) ) |
| 118 |
116 117
|
bitrdi |
⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) → ( 𝑦 ∈ ( ω ↑o 𝐶 ) ↔ ∃ 𝑧 ∈ ( 𝐶 ∖ 1o ) 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) |
| 119 |
118
|
adantr |
⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) → ( 𝑦 ∈ ( ω ↑o 𝐶 ) ↔ ∃ 𝑧 ∈ ( 𝐶 ∖ 1o ) 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) |
| 120 |
|
eldifi |
⊢ ( 𝑧 ∈ ( 𝐶 ∖ 1o ) → 𝑧 ∈ 𝐶 ) |
| 121 |
104
|
adantr |
⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ω ∈ On ) |
| 122 |
108
|
adantr |
⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → 𝐶 ∈ On ) |
| 123 |
|
simplrl |
⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → 𝑥 ∈ 𝐶 ) |
| 124 |
|
onelon |
⊢ ( ( 𝐶 ∈ On ∧ 𝑥 ∈ 𝐶 ) → 𝑥 ∈ On ) |
| 125 |
122 123 124
|
syl2anc |
⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → 𝑥 ∈ On ) |
| 126 |
121 125 46
|
syl2anc |
⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ( ω ↑o 𝑥 ) ∈ On ) |
| 127 |
|
eloni |
⊢ ( ( ω ↑o 𝑥 ) ∈ On → Ord ( ω ↑o 𝑥 ) ) |
| 128 |
126 127
|
syl |
⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → Ord ( ω ↑o 𝑥 ) ) |
| 129 |
|
simplrr |
⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → 𝐴 ∈ ( ω ↑o 𝑥 ) ) |
| 130 |
|
ordelss |
⊢ ( ( Ord ( ω ↑o 𝑥 ) ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) → 𝐴 ⊆ ( ω ↑o 𝑥 ) ) |
| 131 |
128 129 130
|
syl2anc |
⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → 𝐴 ⊆ ( ω ↑o 𝑥 ) ) |
| 132 |
|
ssun1 |
⊢ 𝑥 ⊆ ( 𝑥 ∪ 𝑧 ) |
| 133 |
26
|
ad3antrrr |
⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → Ord 𝐶 ) |
| 134 |
|
simprl |
⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → 𝑧 ∈ 𝐶 ) |
| 135 |
|
ordunel |
⊢ ( ( Ord 𝐶 ∧ 𝑥 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶 ) → ( 𝑥 ∪ 𝑧 ) ∈ 𝐶 ) |
| 136 |
133 123 134 135
|
syl3anc |
⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ( 𝑥 ∪ 𝑧 ) ∈ 𝐶 ) |
| 137 |
|
onelon |
⊢ ( ( 𝐶 ∈ On ∧ ( 𝑥 ∪ 𝑧 ) ∈ 𝐶 ) → ( 𝑥 ∪ 𝑧 ) ∈ On ) |
| 138 |
122 136 137
|
syl2anc |
⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ( 𝑥 ∪ 𝑧 ) ∈ On ) |
| 139 |
|
peano1 |
⊢ ∅ ∈ ω |
| 140 |
139
|
a1i |
⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ∅ ∈ ω ) |
| 141 |
|
oewordi |
⊢ ( ( ( 𝑥 ∈ On ∧ ( 𝑥 ∪ 𝑧 ) ∈ On ∧ ω ∈ On ) ∧ ∅ ∈ ω ) → ( 𝑥 ⊆ ( 𝑥 ∪ 𝑧 ) → ( ω ↑o 𝑥 ) ⊆ ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ) ) |
| 142 |
125 138 121 140 141
|
syl31anc |
⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ( 𝑥 ⊆ ( 𝑥 ∪ 𝑧 ) → ( ω ↑o 𝑥 ) ⊆ ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ) ) |
| 143 |
132 142
|
mpi |
⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ( ω ↑o 𝑥 ) ⊆ ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ) |
| 144 |
131 143
|
sstrd |
⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → 𝐴 ⊆ ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ) |
| 145 |
102
|
adantr |
⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → 𝐴 ∈ On ) |
| 146 |
|
oecl |
⊢ ( ( ω ∈ On ∧ ( 𝑥 ∪ 𝑧 ) ∈ On ) → ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ∈ On ) |
| 147 |
121 138 146
|
syl2anc |
⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ∈ On ) |
| 148 |
|
onelon |
⊢ ( ( 𝐶 ∈ On ∧ 𝑧 ∈ 𝐶 ) → 𝑧 ∈ On ) |
| 149 |
122 134 148
|
syl2anc |
⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → 𝑧 ∈ On ) |
| 150 |
|
oecl |
⊢ ( ( ω ∈ On ∧ 𝑧 ∈ On ) → ( ω ↑o 𝑧 ) ∈ On ) |
| 151 |
121 149 150
|
syl2anc |
⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ( ω ↑o 𝑧 ) ∈ On ) |
| 152 |
|
simprr |
⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → 𝑦 ∈ ( ω ↑o 𝑧 ) ) |
| 153 |
|
onelon |
⊢ ( ( ( ω ↑o 𝑧 ) ∈ On ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) → 𝑦 ∈ On ) |
| 154 |
151 152 153
|
syl2anc |
⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → 𝑦 ∈ On ) |
| 155 |
|
oawordri |
⊢ ( ( 𝐴 ∈ On ∧ ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ∈ On ∧ 𝑦 ∈ On ) → ( 𝐴 ⊆ ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) → ( 𝐴 +o 𝑦 ) ⊆ ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) +o 𝑦 ) ) ) |
| 156 |
145 147 154 155
|
syl3anc |
⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ( 𝐴 ⊆ ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) → ( 𝐴 +o 𝑦 ) ⊆ ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) +o 𝑦 ) ) ) |
| 157 |
144 156
|
mpd |
⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ( 𝐴 +o 𝑦 ) ⊆ ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) +o 𝑦 ) ) |
| 158 |
|
eloni |
⊢ ( ( ω ↑o 𝑧 ) ∈ On → Ord ( ω ↑o 𝑧 ) ) |
| 159 |
151 158
|
syl |
⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → Ord ( ω ↑o 𝑧 ) ) |
| 160 |
|
ordelss |
⊢ ( ( Ord ( ω ↑o 𝑧 ) ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) → 𝑦 ⊆ ( ω ↑o 𝑧 ) ) |
| 161 |
159 152 160
|
syl2anc |
⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → 𝑦 ⊆ ( ω ↑o 𝑧 ) ) |
| 162 |
|
ssun2 |
⊢ 𝑧 ⊆ ( 𝑥 ∪ 𝑧 ) |
| 163 |
|
oewordi |
⊢ ( ( ( 𝑧 ∈ On ∧ ( 𝑥 ∪ 𝑧 ) ∈ On ∧ ω ∈ On ) ∧ ∅ ∈ ω ) → ( 𝑧 ⊆ ( 𝑥 ∪ 𝑧 ) → ( ω ↑o 𝑧 ) ⊆ ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ) ) |
| 164 |
149 138 121 140 163
|
syl31anc |
⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ( 𝑧 ⊆ ( 𝑥 ∪ 𝑧 ) → ( ω ↑o 𝑧 ) ⊆ ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ) ) |
| 165 |
162 164
|
mpi |
⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ( ω ↑o 𝑧 ) ⊆ ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ) |
| 166 |
161 165
|
sstrd |
⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → 𝑦 ⊆ ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ) |
| 167 |
|
oaword |
⊢ ( ( 𝑦 ∈ On ∧ ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ∈ On ∧ ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ∈ On ) → ( 𝑦 ⊆ ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ↔ ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) +o 𝑦 ) ⊆ ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) +o ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ) ) ) |
| 168 |
154 147 147 167
|
syl3anc |
⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ( 𝑦 ⊆ ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ↔ ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) +o 𝑦 ) ⊆ ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) +o ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ) ) ) |
| 169 |
166 168
|
mpbid |
⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) +o 𝑦 ) ⊆ ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) +o ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ) ) |
| 170 |
157 169
|
sstrd |
⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ( 𝐴 +o 𝑦 ) ⊆ ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) +o ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ) ) |
| 171 |
|
ordom |
⊢ Ord ω |
| 172 |
|
ordsucss |
⊢ ( Ord ω → ( 1o ∈ ω → suc 1o ⊆ ω ) ) |
| 173 |
171 105 172
|
mp2 |
⊢ suc 1o ⊆ ω |
| 174 |
|
1on |
⊢ 1o ∈ On |
| 175 |
|
suceloni |
⊢ ( 1o ∈ On → suc 1o ∈ On ) |
| 176 |
174 175
|
mp1i |
⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → suc 1o ∈ On ) |
| 177 |
|
omwordi |
⊢ ( ( suc 1o ∈ On ∧ ω ∈ On ∧ ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ∈ On ) → ( suc 1o ⊆ ω → ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ·o suc 1o ) ⊆ ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ·o ω ) ) ) |
| 178 |
176 121 147 177
|
syl3anc |
⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ( suc 1o ⊆ ω → ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ·o suc 1o ) ⊆ ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ·o ω ) ) ) |
| 179 |
173 178
|
mpi |
⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ·o suc 1o ) ⊆ ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ·o ω ) ) |
| 180 |
174
|
a1i |
⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → 1o ∈ On ) |
| 181 |
|
omsuc |
⊢ ( ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ∈ On ∧ 1o ∈ On ) → ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ·o suc 1o ) = ( ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ·o 1o ) +o ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ) ) |
| 182 |
147 180 181
|
syl2anc |
⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ·o suc 1o ) = ( ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ·o 1o ) +o ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ) ) |
| 183 |
|
om1 |
⊢ ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ∈ On → ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ·o 1o ) = ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ) |
| 184 |
147 183
|
syl |
⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ·o 1o ) = ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ) |
| 185 |
184
|
oveq1d |
⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ( ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ·o 1o ) +o ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ) = ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) +o ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ) ) |
| 186 |
182 185
|
eqtr2d |
⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) +o ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ) = ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ·o suc 1o ) ) |
| 187 |
|
oesuc |
⊢ ( ( ω ∈ On ∧ ( 𝑥 ∪ 𝑧 ) ∈ On ) → ( ω ↑o suc ( 𝑥 ∪ 𝑧 ) ) = ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ·o ω ) ) |
| 188 |
121 138 187
|
syl2anc |
⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ( ω ↑o suc ( 𝑥 ∪ 𝑧 ) ) = ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ·o ω ) ) |
| 189 |
179 186 188
|
3sstr4d |
⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) +o ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ) ⊆ ( ω ↑o suc ( 𝑥 ∪ 𝑧 ) ) ) |
| 190 |
170 189
|
sstrd |
⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ( 𝐴 +o 𝑦 ) ⊆ ( ω ↑o suc ( 𝑥 ∪ 𝑧 ) ) ) |
| 191 |
|
ordsucss |
⊢ ( Ord 𝐶 → ( ( 𝑥 ∪ 𝑧 ) ∈ 𝐶 → suc ( 𝑥 ∪ 𝑧 ) ⊆ 𝐶 ) ) |
| 192 |
133 136 191
|
sylc |
⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → suc ( 𝑥 ∪ 𝑧 ) ⊆ 𝐶 ) |
| 193 |
|
suceloni |
⊢ ( ( 𝑥 ∪ 𝑧 ) ∈ On → suc ( 𝑥 ∪ 𝑧 ) ∈ On ) |
| 194 |
138 193
|
syl |
⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → suc ( 𝑥 ∪ 𝑧 ) ∈ On ) |
| 195 |
|
oewordi |
⊢ ( ( ( suc ( 𝑥 ∪ 𝑧 ) ∈ On ∧ 𝐶 ∈ On ∧ ω ∈ On ) ∧ ∅ ∈ ω ) → ( suc ( 𝑥 ∪ 𝑧 ) ⊆ 𝐶 → ( ω ↑o suc ( 𝑥 ∪ 𝑧 ) ) ⊆ ( ω ↑o 𝐶 ) ) ) |
| 196 |
194 122 121 140 195
|
syl31anc |
⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ( suc ( 𝑥 ∪ 𝑧 ) ⊆ 𝐶 → ( ω ↑o suc ( 𝑥 ∪ 𝑧 ) ) ⊆ ( ω ↑o 𝐶 ) ) ) |
| 197 |
192 196
|
mpd |
⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ( ω ↑o suc ( 𝑥 ∪ 𝑧 ) ) ⊆ ( ω ↑o 𝐶 ) ) |
| 198 |
190 197
|
sstrd |
⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ( 𝐴 +o 𝑦 ) ⊆ ( ω ↑o 𝐶 ) ) |
| 199 |
198
|
expr |
⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ 𝑧 ∈ 𝐶 ) → ( 𝑦 ∈ ( ω ↑o 𝑧 ) → ( 𝐴 +o 𝑦 ) ⊆ ( ω ↑o 𝐶 ) ) ) |
| 200 |
120 199
|
sylan2 |
⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ 𝑧 ∈ ( 𝐶 ∖ 1o ) ) → ( 𝑦 ∈ ( ω ↑o 𝑧 ) → ( 𝐴 +o 𝑦 ) ⊆ ( ω ↑o 𝐶 ) ) ) |
| 201 |
200
|
rexlimdva |
⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) → ( ∃ 𝑧 ∈ ( 𝐶 ∖ 1o ) 𝑦 ∈ ( ω ↑o 𝑧 ) → ( 𝐴 +o 𝑦 ) ⊆ ( ω ↑o 𝐶 ) ) ) |
| 202 |
119 201
|
sylbid |
⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) → ( 𝑦 ∈ ( ω ↑o 𝐶 ) → ( 𝐴 +o 𝑦 ) ⊆ ( ω ↑o 𝐶 ) ) ) |
| 203 |
202
|
ralrimiv |
⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) → ∀ 𝑦 ∈ ( ω ↑o 𝐶 ) ( 𝐴 +o 𝑦 ) ⊆ ( ω ↑o 𝐶 ) ) |
| 204 |
|
iunss |
⊢ ( ∪ 𝑦 ∈ ( ω ↑o 𝐶 ) ( 𝐴 +o 𝑦 ) ⊆ ( ω ↑o 𝐶 ) ↔ ∀ 𝑦 ∈ ( ω ↑o 𝐶 ) ( 𝐴 +o 𝑦 ) ⊆ ( ω ↑o 𝐶 ) ) |
| 205 |
203 204
|
sylibr |
⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) → ∪ 𝑦 ∈ ( ω ↑o 𝐶 ) ( 𝐴 +o 𝑦 ) ⊆ ( ω ↑o 𝐶 ) ) |
| 206 |
113 205
|
eqsstrd |
⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) → ( 𝐴 +o ( ω ↑o 𝐶 ) ) ⊆ ( ω ↑o 𝐶 ) ) |
| 207 |
206
|
expr |
⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ 𝑥 ∈ 𝐶 ) → ( 𝐴 ∈ ( ω ↑o 𝑥 ) → ( 𝐴 +o ( ω ↑o 𝐶 ) ) ⊆ ( ω ↑o 𝐶 ) ) ) |
| 208 |
101 207
|
sylan2 |
⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ 𝑥 ∈ ( 𝐶 ∖ 1o ) ) → ( 𝐴 ∈ ( ω ↑o 𝑥 ) → ( 𝐴 +o ( ω ↑o 𝐶 ) ) ⊆ ( ω ↑o 𝐶 ) ) ) |
| 209 |
208
|
rexlimdva |
⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) → ( ∃ 𝑥 ∈ ( 𝐶 ∖ 1o ) 𝐴 ∈ ( ω ↑o 𝑥 ) → ( 𝐴 +o ( ω ↑o 𝐶 ) ) ⊆ ( ω ↑o 𝐶 ) ) ) |
| 210 |
100 209
|
mpd |
⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) → ( 𝐴 +o ( ω ↑o 𝐶 ) ) ⊆ ( ω ↑o 𝐶 ) ) |
| 211 |
88
|
adantr |
⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) → ( ω ↑o 𝐶 ) ⊆ ( 𝐴 +o ( ω ↑o 𝐶 ) ) ) |
| 212 |
210 211
|
eqssd |
⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) → ( 𝐴 +o ( ω ↑o 𝐶 ) ) = ( ω ↑o 𝐶 ) ) |
| 213 |
212
|
ex |
⊢ ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) → ( Lim 𝐶 → ( 𝐴 +o ( ω ↑o 𝐶 ) ) = ( ω ↑o 𝐶 ) ) ) |
| 214 |
43 91 213
|
3jaod |
⊢ ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) → ( ( 𝐶 = ∅ ∨ ∃ 𝑥 ∈ On 𝐶 = suc 𝑥 ∨ Lim 𝐶 ) → ( 𝐴 +o ( ω ↑o 𝐶 ) ) = ( ω ↑o 𝐶 ) ) ) |
| 215 |
28 214
|
mpd |
⊢ ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) → ( 𝐴 +o ( ω ↑o 𝐶 ) ) = ( ω ↑o 𝐶 ) ) |
| 216 |
215
|
adantr |
⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ 𝑥 ∈ On ) → ( 𝐴 +o ( ω ↑o 𝐶 ) ) = ( ω ↑o 𝐶 ) ) |
| 217 |
216
|
oveq1d |
⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ 𝑥 ∈ On ) → ( ( 𝐴 +o ( ω ↑o 𝐶 ) ) +o 𝑥 ) = ( ( ω ↑o 𝐶 ) +o 𝑥 ) ) |
| 218 |
23 217
|
eqtr3d |
⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ 𝑥 ∈ On ) → ( 𝐴 +o ( ( ω ↑o 𝐶 ) +o 𝑥 ) ) = ( ( ω ↑o 𝐶 ) +o 𝑥 ) ) |
| 219 |
|
oveq2 |
⊢ ( ( ( ω ↑o 𝐶 ) +o 𝑥 ) = 𝐵 → ( 𝐴 +o ( ( ω ↑o 𝐶 ) +o 𝑥 ) ) = ( 𝐴 +o 𝐵 ) ) |
| 220 |
|
id |
⊢ ( ( ( ω ↑o 𝐶 ) +o 𝑥 ) = 𝐵 → ( ( ω ↑o 𝐶 ) +o 𝑥 ) = 𝐵 ) |
| 221 |
219 220
|
eqeq12d |
⊢ ( ( ( ω ↑o 𝐶 ) +o 𝑥 ) = 𝐵 → ( ( 𝐴 +o ( ( ω ↑o 𝐶 ) +o 𝑥 ) ) = ( ( ω ↑o 𝐶 ) +o 𝑥 ) ↔ ( 𝐴 +o 𝐵 ) = 𝐵 ) ) |
| 222 |
218 221
|
syl5ibcom |
⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ 𝑥 ∈ On ) → ( ( ( ω ↑o 𝐶 ) +o 𝑥 ) = 𝐵 → ( 𝐴 +o 𝐵 ) = 𝐵 ) ) |
| 223 |
222
|
rexlimdva |
⊢ ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) → ( ∃ 𝑥 ∈ On ( ( ω ↑o 𝐶 ) +o 𝑥 ) = 𝐵 → ( 𝐴 +o 𝐵 ) = 𝐵 ) ) |
| 224 |
15 223
|
mpd |
⊢ ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) → ( 𝐴 +o 𝐵 ) = 𝐵 ) |