Step |
Hyp |
Ref |
Expression |
1 |
|
oveq2 |
|- ( x = suc A -> ( C ^o x ) = ( C ^o suc A ) ) |
2 |
1
|
eleq2d |
|- ( x = suc A -> ( ( C ^o A ) e. ( C ^o x ) <-> ( C ^o A ) e. ( C ^o suc A ) ) ) |
3 |
2
|
imbi2d |
|- ( x = suc A -> ( ( C e. ( On \ 2o ) -> ( C ^o A ) e. ( C ^o x ) ) <-> ( C e. ( On \ 2o ) -> ( C ^o A ) e. ( C ^o suc A ) ) ) ) |
4 |
|
oveq2 |
|- ( x = y -> ( C ^o x ) = ( C ^o y ) ) |
5 |
4
|
eleq2d |
|- ( x = y -> ( ( C ^o A ) e. ( C ^o x ) <-> ( C ^o A ) e. ( C ^o y ) ) ) |
6 |
5
|
imbi2d |
|- ( x = y -> ( ( C e. ( On \ 2o ) -> ( C ^o A ) e. ( C ^o x ) ) <-> ( C e. ( On \ 2o ) -> ( C ^o A ) e. ( C ^o y ) ) ) ) |
7 |
|
oveq2 |
|- ( x = suc y -> ( C ^o x ) = ( C ^o suc y ) ) |
8 |
7
|
eleq2d |
|- ( x = suc y -> ( ( C ^o A ) e. ( C ^o x ) <-> ( C ^o A ) e. ( C ^o suc y ) ) ) |
9 |
8
|
imbi2d |
|- ( x = suc y -> ( ( C e. ( On \ 2o ) -> ( C ^o A ) e. ( C ^o x ) ) <-> ( C e. ( On \ 2o ) -> ( C ^o A ) e. ( C ^o suc y ) ) ) ) |
10 |
|
oveq2 |
|- ( x = B -> ( C ^o x ) = ( C ^o B ) ) |
11 |
10
|
eleq2d |
|- ( x = B -> ( ( C ^o A ) e. ( C ^o x ) <-> ( C ^o A ) e. ( C ^o B ) ) ) |
12 |
11
|
imbi2d |
|- ( x = B -> ( ( C e. ( On \ 2o ) -> ( C ^o A ) e. ( C ^o x ) ) <-> ( C e. ( On \ 2o ) -> ( C ^o A ) e. ( C ^o B ) ) ) ) |
13 |
|
eldifi |
|- ( C e. ( On \ 2o ) -> C e. On ) |
14 |
|
oecl |
|- ( ( C e. On /\ A e. On ) -> ( C ^o A ) e. On ) |
15 |
13 14
|
sylan |
|- ( ( C e. ( On \ 2o ) /\ A e. On ) -> ( C ^o A ) e. On ) |
16 |
|
om1 |
|- ( ( C ^o A ) e. On -> ( ( C ^o A ) .o 1o ) = ( C ^o A ) ) |
17 |
15 16
|
syl |
|- ( ( C e. ( On \ 2o ) /\ A e. On ) -> ( ( C ^o A ) .o 1o ) = ( C ^o A ) ) |
18 |
|
ondif2 |
|- ( C e. ( On \ 2o ) <-> ( C e. On /\ 1o e. C ) ) |
19 |
18
|
simprbi |
|- ( C e. ( On \ 2o ) -> 1o e. C ) |
20 |
19
|
adantr |
|- ( ( C e. ( On \ 2o ) /\ A e. On ) -> 1o e. C ) |
21 |
13
|
adantr |
|- ( ( C e. ( On \ 2o ) /\ A e. On ) -> C e. On ) |
22 |
|
simpr |
|- ( ( C e. ( On \ 2o ) /\ A e. On ) -> A e. On ) |
23 |
|
dif20el |
|- ( C e. ( On \ 2o ) -> (/) e. C ) |
24 |
23
|
adantr |
|- ( ( C e. ( On \ 2o ) /\ A e. On ) -> (/) e. C ) |
25 |
|
oen0 |
|- ( ( ( C e. On /\ A e. On ) /\ (/) e. C ) -> (/) e. ( C ^o A ) ) |
26 |
21 22 24 25
|
syl21anc |
|- ( ( C e. ( On \ 2o ) /\ A e. On ) -> (/) e. ( C ^o A ) ) |
27 |
|
omordi |
|- ( ( ( C e. On /\ ( C ^o A ) e. On ) /\ (/) e. ( C ^o A ) ) -> ( 1o e. C -> ( ( C ^o A ) .o 1o ) e. ( ( C ^o A ) .o C ) ) ) |
28 |
21 15 26 27
|
syl21anc |
|- ( ( C e. ( On \ 2o ) /\ A e. On ) -> ( 1o e. C -> ( ( C ^o A ) .o 1o ) e. ( ( C ^o A ) .o C ) ) ) |
29 |
20 28
|
mpd |
|- ( ( C e. ( On \ 2o ) /\ A e. On ) -> ( ( C ^o A ) .o 1o ) e. ( ( C ^o A ) .o C ) ) |
30 |
17 29
|
eqeltrrd |
|- ( ( C e. ( On \ 2o ) /\ A e. On ) -> ( C ^o A ) e. ( ( C ^o A ) .o C ) ) |
31 |
|
oesuc |
|- ( ( C e. On /\ A e. On ) -> ( C ^o suc A ) = ( ( C ^o A ) .o C ) ) |
32 |
13 31
|
sylan |
|- ( ( C e. ( On \ 2o ) /\ A e. On ) -> ( C ^o suc A ) = ( ( C ^o A ) .o C ) ) |
33 |
30 32
|
eleqtrrd |
|- ( ( C e. ( On \ 2o ) /\ A e. On ) -> ( C ^o A ) e. ( C ^o suc A ) ) |
34 |
33
|
expcom |
|- ( A e. On -> ( C e. ( On \ 2o ) -> ( C ^o A ) e. ( C ^o suc A ) ) ) |
35 |
|
oecl |
|- ( ( C e. On /\ y e. On ) -> ( C ^o y ) e. On ) |
36 |
13 35
|
sylan |
|- ( ( C e. ( On \ 2o ) /\ y e. On ) -> ( C ^o y ) e. On ) |
37 |
|
om1 |
|- ( ( C ^o y ) e. On -> ( ( C ^o y ) .o 1o ) = ( C ^o y ) ) |
38 |
36 37
|
syl |
|- ( ( C e. ( On \ 2o ) /\ y e. On ) -> ( ( C ^o y ) .o 1o ) = ( C ^o y ) ) |
39 |
19
|
adantr |
|- ( ( C e. ( On \ 2o ) /\ y e. On ) -> 1o e. C ) |
40 |
13
|
adantr |
|- ( ( C e. ( On \ 2o ) /\ y e. On ) -> C e. On ) |
41 |
|
simpr |
|- ( ( C e. ( On \ 2o ) /\ y e. On ) -> y e. On ) |
42 |
23
|
adantr |
|- ( ( C e. ( On \ 2o ) /\ y e. On ) -> (/) e. C ) |
43 |
|
oen0 |
|- ( ( ( C e. On /\ y e. On ) /\ (/) e. C ) -> (/) e. ( C ^o y ) ) |
44 |
40 41 42 43
|
syl21anc |
|- ( ( C e. ( On \ 2o ) /\ y e. On ) -> (/) e. ( C ^o y ) ) |
45 |
|
omordi |
|- ( ( ( C e. On /\ ( C ^o y ) e. On ) /\ (/) e. ( C ^o y ) ) -> ( 1o e. C -> ( ( C ^o y ) .o 1o ) e. ( ( C ^o y ) .o C ) ) ) |
46 |
40 36 44 45
|
syl21anc |
|- ( ( C e. ( On \ 2o ) /\ y e. On ) -> ( 1o e. C -> ( ( C ^o y ) .o 1o ) e. ( ( C ^o y ) .o C ) ) ) |
47 |
39 46
|
mpd |
|- ( ( C e. ( On \ 2o ) /\ y e. On ) -> ( ( C ^o y ) .o 1o ) e. ( ( C ^o y ) .o C ) ) |
48 |
38 47
|
eqeltrrd |
|- ( ( C e. ( On \ 2o ) /\ y e. On ) -> ( C ^o y ) e. ( ( C ^o y ) .o C ) ) |
49 |
|
oesuc |
|- ( ( C e. On /\ y e. On ) -> ( C ^o suc y ) = ( ( C ^o y ) .o C ) ) |
50 |
13 49
|
sylan |
|- ( ( C e. ( On \ 2o ) /\ y e. On ) -> ( C ^o suc y ) = ( ( C ^o y ) .o C ) ) |
51 |
48 50
|
eleqtrrd |
|- ( ( C e. ( On \ 2o ) /\ y e. On ) -> ( C ^o y ) e. ( C ^o suc y ) ) |
52 |
|
suceloni |
|- ( y e. On -> suc y e. On ) |
53 |
|
oecl |
|- ( ( C e. On /\ suc y e. On ) -> ( C ^o suc y ) e. On ) |
54 |
13 52 53
|
syl2an |
|- ( ( C e. ( On \ 2o ) /\ y e. On ) -> ( C ^o suc y ) e. On ) |
55 |
|
ontr1 |
|- ( ( C ^o suc y ) e. On -> ( ( ( C ^o A ) e. ( C ^o y ) /\ ( C ^o y ) e. ( C ^o suc y ) ) -> ( C ^o A ) e. ( C ^o suc y ) ) ) |
56 |
54 55
|
syl |
|- ( ( C e. ( On \ 2o ) /\ y e. On ) -> ( ( ( C ^o A ) e. ( C ^o y ) /\ ( C ^o y ) e. ( C ^o suc y ) ) -> ( C ^o A ) e. ( C ^o suc y ) ) ) |
57 |
51 56
|
mpan2d |
|- ( ( C e. ( On \ 2o ) /\ y e. On ) -> ( ( C ^o A ) e. ( C ^o y ) -> ( C ^o A ) e. ( C ^o suc y ) ) ) |
58 |
57
|
expcom |
|- ( y e. On -> ( C e. ( On \ 2o ) -> ( ( C ^o A ) e. ( C ^o y ) -> ( C ^o A ) e. ( C ^o suc y ) ) ) ) |
59 |
58
|
adantr |
|- ( ( y e. On /\ A e. y ) -> ( C e. ( On \ 2o ) -> ( ( C ^o A ) e. ( C ^o y ) -> ( C ^o A ) e. ( C ^o suc y ) ) ) ) |
60 |
59
|
a2d |
|- ( ( y e. On /\ A e. y ) -> ( ( C e. ( On \ 2o ) -> ( C ^o A ) e. ( C ^o y ) ) -> ( C e. ( On \ 2o ) -> ( C ^o A ) e. ( C ^o suc y ) ) ) ) |
61 |
|
bi2.04 |
|- ( ( A e. y -> ( C e. ( On \ 2o ) -> ( C ^o A ) e. ( C ^o y ) ) ) <-> ( C e. ( On \ 2o ) -> ( A e. y -> ( C ^o A ) e. ( C ^o y ) ) ) ) |
62 |
61
|
ralbii |
|- ( A. y e. x ( A e. y -> ( C e. ( On \ 2o ) -> ( C ^o A ) e. ( C ^o y ) ) ) <-> A. y e. x ( C e. ( On \ 2o ) -> ( A e. y -> ( C ^o A ) e. ( C ^o y ) ) ) ) |
63 |
|
r19.21v |
|- ( A. y e. x ( C e. ( On \ 2o ) -> ( A e. y -> ( C ^o A ) e. ( C ^o y ) ) ) <-> ( C e. ( On \ 2o ) -> A. y e. x ( A e. y -> ( C ^o A ) e. ( C ^o y ) ) ) ) |
64 |
62 63
|
bitri |
|- ( A. y e. x ( A e. y -> ( C e. ( On \ 2o ) -> ( C ^o A ) e. ( C ^o y ) ) ) <-> ( C e. ( On \ 2o ) -> A. y e. x ( A e. y -> ( C ^o A ) e. ( C ^o y ) ) ) ) |
65 |
|
limsuc |
|- ( Lim x -> ( A e. x <-> suc A e. x ) ) |
66 |
65
|
biimpa |
|- ( ( Lim x /\ A e. x ) -> suc A e. x ) |
67 |
|
elex |
|- ( suc A e. x -> suc A e. _V ) |
68 |
|
sucexb |
|- ( A e. _V <-> suc A e. _V ) |
69 |
|
sucidg |
|- ( A e. _V -> A e. suc A ) |
70 |
68 69
|
sylbir |
|- ( suc A e. _V -> A e. suc A ) |
71 |
67 70
|
syl |
|- ( suc A e. x -> A e. suc A ) |
72 |
|
eleq2 |
|- ( y = suc A -> ( A e. y <-> A e. suc A ) ) |
73 |
|
oveq2 |
|- ( y = suc A -> ( C ^o y ) = ( C ^o suc A ) ) |
74 |
73
|
eleq2d |
|- ( y = suc A -> ( ( C ^o A ) e. ( C ^o y ) <-> ( C ^o A ) e. ( C ^o suc A ) ) ) |
75 |
72 74
|
imbi12d |
|- ( y = suc A -> ( ( A e. y -> ( C ^o A ) e. ( C ^o y ) ) <-> ( A e. suc A -> ( C ^o A ) e. ( C ^o suc A ) ) ) ) |
76 |
75
|
rspcv |
|- ( suc A e. x -> ( A. y e. x ( A e. y -> ( C ^o A ) e. ( C ^o y ) ) -> ( A e. suc A -> ( C ^o A ) e. ( C ^o suc A ) ) ) ) |
77 |
71 76
|
mpid |
|- ( suc A e. x -> ( A. y e. x ( A e. y -> ( C ^o A ) e. ( C ^o y ) ) -> ( C ^o A ) e. ( C ^o suc A ) ) ) |
78 |
77
|
anc2li |
|- ( suc A e. x -> ( A. y e. x ( A e. y -> ( C ^o A ) e. ( C ^o y ) ) -> ( suc A e. x /\ ( C ^o A ) e. ( C ^o suc A ) ) ) ) |
79 |
73
|
eliuni |
|- ( ( suc A e. x /\ ( C ^o A ) e. ( C ^o suc A ) ) -> ( C ^o A ) e. U_ y e. x ( C ^o y ) ) |
80 |
78 79
|
syl6 |
|- ( suc A e. x -> ( A. y e. x ( A e. y -> ( C ^o A ) e. ( C ^o y ) ) -> ( C ^o A ) e. U_ y e. x ( C ^o y ) ) ) |
81 |
66 80
|
syl |
|- ( ( Lim x /\ A e. x ) -> ( A. y e. x ( A e. y -> ( C ^o A ) e. ( C ^o y ) ) -> ( C ^o A ) e. U_ y e. x ( C ^o y ) ) ) |
82 |
81
|
adantr |
|- ( ( ( Lim x /\ A e. x ) /\ C e. ( On \ 2o ) ) -> ( A. y e. x ( A e. y -> ( C ^o A ) e. ( C ^o y ) ) -> ( C ^o A ) e. U_ y e. x ( C ^o y ) ) ) |
83 |
13
|
adantl |
|- ( ( Lim x /\ C e. ( On \ 2o ) ) -> C e. On ) |
84 |
|
simpl |
|- ( ( Lim x /\ C e. ( On \ 2o ) ) -> Lim x ) |
85 |
23
|
adantl |
|- ( ( Lim x /\ C e. ( On \ 2o ) ) -> (/) e. C ) |
86 |
|
vex |
|- x e. _V |
87 |
|
oelim |
|- ( ( ( C e. On /\ ( x e. _V /\ Lim x ) ) /\ (/) e. C ) -> ( C ^o x ) = U_ y e. x ( C ^o y ) ) |
88 |
86 87
|
mpanlr1 |
|- ( ( ( C e. On /\ Lim x ) /\ (/) e. C ) -> ( C ^o x ) = U_ y e. x ( C ^o y ) ) |
89 |
83 84 85 88
|
syl21anc |
|- ( ( Lim x /\ C e. ( On \ 2o ) ) -> ( C ^o x ) = U_ y e. x ( C ^o y ) ) |
90 |
89
|
adantlr |
|- ( ( ( Lim x /\ A e. x ) /\ C e. ( On \ 2o ) ) -> ( C ^o x ) = U_ y e. x ( C ^o y ) ) |
91 |
90
|
eleq2d |
|- ( ( ( Lim x /\ A e. x ) /\ C e. ( On \ 2o ) ) -> ( ( C ^o A ) e. ( C ^o x ) <-> ( C ^o A ) e. U_ y e. x ( C ^o y ) ) ) |
92 |
82 91
|
sylibrd |
|- ( ( ( Lim x /\ A e. x ) /\ C e. ( On \ 2o ) ) -> ( A. y e. x ( A e. y -> ( C ^o A ) e. ( C ^o y ) ) -> ( C ^o A ) e. ( C ^o x ) ) ) |
93 |
92
|
ex |
|- ( ( Lim x /\ A e. x ) -> ( C e. ( On \ 2o ) -> ( A. y e. x ( A e. y -> ( C ^o A ) e. ( C ^o y ) ) -> ( C ^o A ) e. ( C ^o x ) ) ) ) |
94 |
93
|
a2d |
|- ( ( Lim x /\ A e. x ) -> ( ( C e. ( On \ 2o ) -> A. y e. x ( A e. y -> ( C ^o A ) e. ( C ^o y ) ) ) -> ( C e. ( On \ 2o ) -> ( C ^o A ) e. ( C ^o x ) ) ) ) |
95 |
64 94
|
syl5bi |
|- ( ( Lim x /\ A e. x ) -> ( A. y e. x ( A e. y -> ( C e. ( On \ 2o ) -> ( C ^o A ) e. ( C ^o y ) ) ) -> ( C e. ( On \ 2o ) -> ( C ^o A ) e. ( C ^o x ) ) ) ) |
96 |
3 6 9 12 34 60 95
|
tfindsg2 |
|- ( ( B e. On /\ A e. B ) -> ( C e. ( On \ 2o ) -> ( C ^o A ) e. ( C ^o B ) ) ) |
97 |
96
|
impancom |
|- ( ( B e. On /\ C e. ( On \ 2o ) ) -> ( A e. B -> ( C ^o A ) e. ( C ^o B ) ) ) |