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