Step |
Hyp |
Ref |
Expression |
1 |
|
onelon |
⊢ ( ( 𝐵 ∈ On ∧ 𝐴 ∈ 𝐵 ) → 𝐴 ∈ On ) |
2 |
1
|
adantll |
⊢ ( ( ( 𝐶 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐴 ∈ 𝐵 ) → 𝐴 ∈ On ) |
3 |
|
eloni |
⊢ ( 𝐵 ∈ On → Ord 𝐵 ) |
4 |
|
ordsucss |
⊢ ( Ord 𝐵 → ( 𝐴 ∈ 𝐵 → suc 𝐴 ⊆ 𝐵 ) ) |
5 |
3 4
|
syl |
⊢ ( 𝐵 ∈ On → ( 𝐴 ∈ 𝐵 → suc 𝐴 ⊆ 𝐵 ) ) |
6 |
5
|
ad2antlr |
⊢ ( ( ( 𝐶 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐴 ∈ On ) → ( 𝐴 ∈ 𝐵 → suc 𝐴 ⊆ 𝐵 ) ) |
7 |
|
sucelon |
⊢ ( 𝐴 ∈ On ↔ suc 𝐴 ∈ On ) |
8 |
|
oveq2 |
⊢ ( 𝑥 = suc 𝐴 → ( 𝐶 +o 𝑥 ) = ( 𝐶 +o suc 𝐴 ) ) |
9 |
8
|
sseq2d |
⊢ ( 𝑥 = suc 𝐴 → ( ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝑥 ) ↔ ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o suc 𝐴 ) ) ) |
10 |
9
|
imbi2d |
⊢ ( 𝑥 = suc 𝐴 → ( ( 𝐶 ∈ On → ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝑥 ) ) ↔ ( 𝐶 ∈ On → ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o suc 𝐴 ) ) ) ) |
11 |
|
oveq2 |
⊢ ( 𝑥 = 𝑦 → ( 𝐶 +o 𝑥 ) = ( 𝐶 +o 𝑦 ) ) |
12 |
11
|
sseq2d |
⊢ ( 𝑥 = 𝑦 → ( ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝑥 ) ↔ ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝑦 ) ) ) |
13 |
12
|
imbi2d |
⊢ ( 𝑥 = 𝑦 → ( ( 𝐶 ∈ On → ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝑥 ) ) ↔ ( 𝐶 ∈ On → ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝑦 ) ) ) ) |
14 |
|
oveq2 |
⊢ ( 𝑥 = suc 𝑦 → ( 𝐶 +o 𝑥 ) = ( 𝐶 +o suc 𝑦 ) ) |
15 |
14
|
sseq2d |
⊢ ( 𝑥 = suc 𝑦 → ( ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝑥 ) ↔ ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o suc 𝑦 ) ) ) |
16 |
15
|
imbi2d |
⊢ ( 𝑥 = suc 𝑦 → ( ( 𝐶 ∈ On → ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝑥 ) ) ↔ ( 𝐶 ∈ On → ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o suc 𝑦 ) ) ) ) |
17 |
|
oveq2 |
⊢ ( 𝑥 = 𝐵 → ( 𝐶 +o 𝑥 ) = ( 𝐶 +o 𝐵 ) ) |
18 |
17
|
sseq2d |
⊢ ( 𝑥 = 𝐵 → ( ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝑥 ) ↔ ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝐵 ) ) ) |
19 |
18
|
imbi2d |
⊢ ( 𝑥 = 𝐵 → ( ( 𝐶 ∈ On → ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝑥 ) ) ↔ ( 𝐶 ∈ On → ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝐵 ) ) ) ) |
20 |
|
ssid |
⊢ ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o suc 𝐴 ) |
21 |
20
|
2a1i |
⊢ ( suc 𝐴 ∈ On → ( 𝐶 ∈ On → ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o suc 𝐴 ) ) ) |
22 |
|
sssucid |
⊢ ( 𝐶 +o 𝑦 ) ⊆ suc ( 𝐶 +o 𝑦 ) |
23 |
|
sstr2 |
⊢ ( ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝑦 ) → ( ( 𝐶 +o 𝑦 ) ⊆ suc ( 𝐶 +o 𝑦 ) → ( 𝐶 +o suc 𝐴 ) ⊆ suc ( 𝐶 +o 𝑦 ) ) ) |
24 |
22 23
|
mpi |
⊢ ( ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝑦 ) → ( 𝐶 +o suc 𝐴 ) ⊆ suc ( 𝐶 +o 𝑦 ) ) |
25 |
|
oasuc |
⊢ ( ( 𝐶 ∈ On ∧ 𝑦 ∈ On ) → ( 𝐶 +o suc 𝑦 ) = suc ( 𝐶 +o 𝑦 ) ) |
26 |
25
|
ancoms |
⊢ ( ( 𝑦 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐶 +o suc 𝑦 ) = suc ( 𝐶 +o 𝑦 ) ) |
27 |
26
|
sseq2d |
⊢ ( ( 𝑦 ∈ On ∧ 𝐶 ∈ On ) → ( ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o suc 𝑦 ) ↔ ( 𝐶 +o suc 𝐴 ) ⊆ suc ( 𝐶 +o 𝑦 ) ) ) |
28 |
24 27
|
syl5ibr |
⊢ ( ( 𝑦 ∈ On ∧ 𝐶 ∈ On ) → ( ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝑦 ) → ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o suc 𝑦 ) ) ) |
29 |
28
|
ex |
⊢ ( 𝑦 ∈ On → ( 𝐶 ∈ On → ( ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝑦 ) → ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o suc 𝑦 ) ) ) ) |
30 |
29
|
ad2antrr |
⊢ ( ( ( 𝑦 ∈ On ∧ suc 𝐴 ∈ On ) ∧ suc 𝐴 ⊆ 𝑦 ) → ( 𝐶 ∈ On → ( ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝑦 ) → ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o suc 𝑦 ) ) ) ) |
31 |
30
|
a2d |
⊢ ( ( ( 𝑦 ∈ On ∧ suc 𝐴 ∈ On ) ∧ suc 𝐴 ⊆ 𝑦 ) → ( ( 𝐶 ∈ On → ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝑦 ) ) → ( 𝐶 ∈ On → ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o suc 𝑦 ) ) ) ) |
32 |
|
sucssel |
⊢ ( 𝐴 ∈ On → ( suc 𝐴 ⊆ 𝑥 → 𝐴 ∈ 𝑥 ) ) |
33 |
7 32
|
sylbir |
⊢ ( suc 𝐴 ∈ On → ( suc 𝐴 ⊆ 𝑥 → 𝐴 ∈ 𝑥 ) ) |
34 |
|
limsuc |
⊢ ( Lim 𝑥 → ( 𝐴 ∈ 𝑥 ↔ suc 𝐴 ∈ 𝑥 ) ) |
35 |
34
|
biimpd |
⊢ ( Lim 𝑥 → ( 𝐴 ∈ 𝑥 → suc 𝐴 ∈ 𝑥 ) ) |
36 |
33 35
|
sylan9r |
⊢ ( ( Lim 𝑥 ∧ suc 𝐴 ∈ On ) → ( suc 𝐴 ⊆ 𝑥 → suc 𝐴 ∈ 𝑥 ) ) |
37 |
36
|
imp |
⊢ ( ( ( Lim 𝑥 ∧ suc 𝐴 ∈ On ) ∧ suc 𝐴 ⊆ 𝑥 ) → suc 𝐴 ∈ 𝑥 ) |
38 |
|
oveq2 |
⊢ ( 𝑦 = suc 𝐴 → ( 𝐶 +o 𝑦 ) = ( 𝐶 +o suc 𝐴 ) ) |
39 |
38
|
ssiun2s |
⊢ ( suc 𝐴 ∈ 𝑥 → ( 𝐶 +o suc 𝐴 ) ⊆ ∪ 𝑦 ∈ 𝑥 ( 𝐶 +o 𝑦 ) ) |
40 |
37 39
|
syl |
⊢ ( ( ( Lim 𝑥 ∧ suc 𝐴 ∈ On ) ∧ suc 𝐴 ⊆ 𝑥 ) → ( 𝐶 +o suc 𝐴 ) ⊆ ∪ 𝑦 ∈ 𝑥 ( 𝐶 +o 𝑦 ) ) |
41 |
40
|
adantr |
⊢ ( ( ( ( Lim 𝑥 ∧ suc 𝐴 ∈ On ) ∧ suc 𝐴 ⊆ 𝑥 ) ∧ 𝐶 ∈ On ) → ( 𝐶 +o suc 𝐴 ) ⊆ ∪ 𝑦 ∈ 𝑥 ( 𝐶 +o 𝑦 ) ) |
42 |
|
vex |
⊢ 𝑥 ∈ V |
43 |
|
oalim |
⊢ ( ( 𝐶 ∈ On ∧ ( 𝑥 ∈ V ∧ Lim 𝑥 ) ) → ( 𝐶 +o 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( 𝐶 +o 𝑦 ) ) |
44 |
42 43
|
mpanr1 |
⊢ ( ( 𝐶 ∈ On ∧ Lim 𝑥 ) → ( 𝐶 +o 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( 𝐶 +o 𝑦 ) ) |
45 |
44
|
ancoms |
⊢ ( ( Lim 𝑥 ∧ 𝐶 ∈ On ) → ( 𝐶 +o 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( 𝐶 +o 𝑦 ) ) |
46 |
45
|
adantlr |
⊢ ( ( ( Lim 𝑥 ∧ suc 𝐴 ∈ On ) ∧ 𝐶 ∈ On ) → ( 𝐶 +o 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( 𝐶 +o 𝑦 ) ) |
47 |
46
|
adantlr |
⊢ ( ( ( ( Lim 𝑥 ∧ suc 𝐴 ∈ On ) ∧ suc 𝐴 ⊆ 𝑥 ) ∧ 𝐶 ∈ On ) → ( 𝐶 +o 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( 𝐶 +o 𝑦 ) ) |
48 |
41 47
|
sseqtrrd |
⊢ ( ( ( ( Lim 𝑥 ∧ suc 𝐴 ∈ On ) ∧ suc 𝐴 ⊆ 𝑥 ) ∧ 𝐶 ∈ On ) → ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝑥 ) ) |
49 |
48
|
ex |
⊢ ( ( ( Lim 𝑥 ∧ suc 𝐴 ∈ On ) ∧ suc 𝐴 ⊆ 𝑥 ) → ( 𝐶 ∈ On → ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝑥 ) ) ) |
50 |
49
|
a1d |
⊢ ( ( ( Lim 𝑥 ∧ suc 𝐴 ∈ On ) ∧ suc 𝐴 ⊆ 𝑥 ) → ( ∀ 𝑦 ∈ 𝑥 ( suc 𝐴 ⊆ 𝑦 → ( 𝐶 ∈ On → ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝑦 ) ) ) → ( 𝐶 ∈ On → ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝑥 ) ) ) ) |
51 |
10 13 16 19 21 31 50
|
tfindsg |
⊢ ( ( ( 𝐵 ∈ On ∧ suc 𝐴 ∈ On ) ∧ suc 𝐴 ⊆ 𝐵 ) → ( 𝐶 ∈ On → ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝐵 ) ) ) |
52 |
51
|
exp31 |
⊢ ( 𝐵 ∈ On → ( suc 𝐴 ∈ On → ( suc 𝐴 ⊆ 𝐵 → ( 𝐶 ∈ On → ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝐵 ) ) ) ) ) |
53 |
7 52
|
syl5bi |
⊢ ( 𝐵 ∈ On → ( 𝐴 ∈ On → ( suc 𝐴 ⊆ 𝐵 → ( 𝐶 ∈ On → ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝐵 ) ) ) ) ) |
54 |
53
|
com4r |
⊢ ( 𝐶 ∈ On → ( 𝐵 ∈ On → ( 𝐴 ∈ On → ( suc 𝐴 ⊆ 𝐵 → ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝐵 ) ) ) ) ) |
55 |
54
|
imp31 |
⊢ ( ( ( 𝐶 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐴 ∈ On ) → ( suc 𝐴 ⊆ 𝐵 → ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝐵 ) ) ) |
56 |
|
oasuc |
⊢ ( ( 𝐶 ∈ On ∧ 𝐴 ∈ On ) → ( 𝐶 +o suc 𝐴 ) = suc ( 𝐶 +o 𝐴 ) ) |
57 |
56
|
sseq1d |
⊢ ( ( 𝐶 ∈ On ∧ 𝐴 ∈ On ) → ( ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝐵 ) ↔ suc ( 𝐶 +o 𝐴 ) ⊆ ( 𝐶 +o 𝐵 ) ) ) |
58 |
|
ovex |
⊢ ( 𝐶 +o 𝐴 ) ∈ V |
59 |
|
sucssel |
⊢ ( ( 𝐶 +o 𝐴 ) ∈ V → ( suc ( 𝐶 +o 𝐴 ) ⊆ ( 𝐶 +o 𝐵 ) → ( 𝐶 +o 𝐴 ) ∈ ( 𝐶 +o 𝐵 ) ) ) |
60 |
58 59
|
ax-mp |
⊢ ( suc ( 𝐶 +o 𝐴 ) ⊆ ( 𝐶 +o 𝐵 ) → ( 𝐶 +o 𝐴 ) ∈ ( 𝐶 +o 𝐵 ) ) |
61 |
57 60
|
syl6bi |
⊢ ( ( 𝐶 ∈ On ∧ 𝐴 ∈ On ) → ( ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝐵 ) → ( 𝐶 +o 𝐴 ) ∈ ( 𝐶 +o 𝐵 ) ) ) |
62 |
61
|
adantlr |
⊢ ( ( ( 𝐶 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐴 ∈ On ) → ( ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝐵 ) → ( 𝐶 +o 𝐴 ) ∈ ( 𝐶 +o 𝐵 ) ) ) |
63 |
6 55 62
|
3syld |
⊢ ( ( ( 𝐶 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐴 ∈ On ) → ( 𝐴 ∈ 𝐵 → ( 𝐶 +o 𝐴 ) ∈ ( 𝐶 +o 𝐵 ) ) ) |
64 |
63
|
imp |
⊢ ( ( ( ( 𝐶 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐴 ∈ On ) ∧ 𝐴 ∈ 𝐵 ) → ( 𝐶 +o 𝐴 ) ∈ ( 𝐶 +o 𝐵 ) ) |
65 |
64
|
an32s |
⊢ ( ( ( ( 𝐶 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐴 ∈ 𝐵 ) ∧ 𝐴 ∈ On ) → ( 𝐶 +o 𝐴 ) ∈ ( 𝐶 +o 𝐵 ) ) |
66 |
2 65
|
mpdan |
⊢ ( ( ( 𝐶 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐴 ∈ 𝐵 ) → ( 𝐶 +o 𝐴 ) ∈ ( 𝐶 +o 𝐵 ) ) |
67 |
66
|
ex |
⊢ ( ( 𝐶 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ∈ 𝐵 → ( 𝐶 +o 𝐴 ) ∈ ( 𝐶 +o 𝐵 ) ) ) |
68 |
67
|
ancoms |
⊢ ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐴 ∈ 𝐵 → ( 𝐶 +o 𝐴 ) ∈ ( 𝐶 +o 𝐵 ) ) ) |