Step |
Hyp |
Ref |
Expression |
1 |
|
opsrval.s |
|- S = ( I mPwSer R ) |
2 |
|
opsrval.o |
|- O = ( ( I ordPwSer R ) ` T ) |
3 |
|
opsrval.b |
|- B = ( Base ` S ) |
4 |
|
opsrval.q |
|- .< = ( lt ` R ) |
5 |
|
opsrval.c |
|- C = ( T |
6 |
|
opsrval.d |
|- D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |
7 |
|
opsrval.l |
|- .<_ = { <. x , y >. | ( { x , y } C_ B /\ ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w C z -> ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } |
8 |
|
opsrval.i |
|- ( ph -> I e. V ) |
9 |
|
opsrval.r |
|- ( ph -> R e. W ) |
10 |
|
opsrval.t |
|- ( ph -> T C_ ( I X. I ) ) |
11 |
8
|
elexd |
|- ( ph -> I e. _V ) |
12 |
9
|
elexd |
|- ( ph -> R e. _V ) |
13 |
8 8
|
xpexd |
|- ( ph -> ( I X. I ) e. _V ) |
14 |
|
pwexg |
|- ( ( I X. I ) e. _V -> ~P ( I X. I ) e. _V ) |
15 |
|
mptexg |
|- ( ~P ( I X. I ) e. _V -> ( r e. ~P ( I X. I ) |-> ( S sSet <. ( le ` ndx ) , { <. x , y >. | ( { x , y } C_ B /\ ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w ( r ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } >. ) ) e. _V ) |
16 |
13 14 15
|
3syl |
|- ( ph -> ( r e. ~P ( I X. I ) |-> ( S sSet <. ( le ` ndx ) , { <. x , y >. | ( { x , y } C_ B /\ ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w ( r ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } >. ) ) e. _V ) |
17 |
|
simpl |
|- ( ( i = I /\ s = R ) -> i = I ) |
18 |
17
|
sqxpeqd |
|- ( ( i = I /\ s = R ) -> ( i X. i ) = ( I X. I ) ) |
19 |
18
|
pweqd |
|- ( ( i = I /\ s = R ) -> ~P ( i X. i ) = ~P ( I X. I ) ) |
20 |
|
ovexd |
|- ( ( i = I /\ s = R ) -> ( i mPwSer s ) e. _V ) |
21 |
|
id |
|- ( p = ( i mPwSer s ) -> p = ( i mPwSer s ) ) |
22 |
|
oveq12 |
|- ( ( i = I /\ s = R ) -> ( i mPwSer s ) = ( I mPwSer R ) ) |
23 |
21 22
|
sylan9eqr |
|- ( ( ( i = I /\ s = R ) /\ p = ( i mPwSer s ) ) -> p = ( I mPwSer R ) ) |
24 |
23 1
|
eqtr4di |
|- ( ( ( i = I /\ s = R ) /\ p = ( i mPwSer s ) ) -> p = S ) |
25 |
24
|
fveq2d |
|- ( ( ( i = I /\ s = R ) /\ p = ( i mPwSer s ) ) -> ( Base ` p ) = ( Base ` S ) ) |
26 |
25 3
|
eqtr4di |
|- ( ( ( i = I /\ s = R ) /\ p = ( i mPwSer s ) ) -> ( Base ` p ) = B ) |
27 |
26
|
sseq2d |
|- ( ( ( i = I /\ s = R ) /\ p = ( i mPwSer s ) ) -> ( { x , y } C_ ( Base ` p ) <-> { x , y } C_ B ) ) |
28 |
|
ovex |
|- ( NN0 ^m i ) e. _V |
29 |
28
|
rabex |
|- { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } e. _V |
30 |
29
|
a1i |
|- ( ( ( i = I /\ s = R ) /\ p = ( i mPwSer s ) ) -> { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } e. _V ) |
31 |
17
|
adantr |
|- ( ( ( i = I /\ s = R ) /\ p = ( i mPwSer s ) ) -> i = I ) |
32 |
31
|
oveq2d |
|- ( ( ( i = I /\ s = R ) /\ p = ( i mPwSer s ) ) -> ( NN0 ^m i ) = ( NN0 ^m I ) ) |
33 |
|
rabeq |
|- ( ( NN0 ^m i ) = ( NN0 ^m I ) -> { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) |
34 |
32 33
|
syl |
|- ( ( ( i = I /\ s = R ) /\ p = ( i mPwSer s ) ) -> { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) |
35 |
34 6
|
eqtr4di |
|- ( ( ( i = I /\ s = R ) /\ p = ( i mPwSer s ) ) -> { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } = D ) |
36 |
|
simpr |
|- ( ( ( ( i = I /\ s = R ) /\ p = ( i mPwSer s ) ) /\ d = D ) -> d = D ) |
37 |
|
simpllr |
|- ( ( ( ( i = I /\ s = R ) /\ p = ( i mPwSer s ) ) /\ d = D ) -> s = R ) |
38 |
37
|
fveq2d |
|- ( ( ( ( i = I /\ s = R ) /\ p = ( i mPwSer s ) ) /\ d = D ) -> ( lt ` s ) = ( lt ` R ) ) |
39 |
38 4
|
eqtr4di |
|- ( ( ( ( i = I /\ s = R ) /\ p = ( i mPwSer s ) ) /\ d = D ) -> ( lt ` s ) = .< ) |
40 |
39
|
breqd |
|- ( ( ( ( i = I /\ s = R ) /\ p = ( i mPwSer s ) ) /\ d = D ) -> ( ( x ` z ) ( lt ` s ) ( y ` z ) <-> ( x ` z ) .< ( y ` z ) ) ) |
41 |
31
|
adantr |
|- ( ( ( ( i = I /\ s = R ) /\ p = ( i mPwSer s ) ) /\ d = D ) -> i = I ) |
42 |
41
|
oveq2d |
|- ( ( ( ( i = I /\ s = R ) /\ p = ( i mPwSer s ) ) /\ d = D ) -> ( r |
43 |
42
|
breqd |
|- ( ( ( ( i = I /\ s = R ) /\ p = ( i mPwSer s ) ) /\ d = D ) -> ( w ( r w ( r |
44 |
43
|
imbi1d |
|- ( ( ( ( i = I /\ s = R ) /\ p = ( i mPwSer s ) ) /\ d = D ) -> ( ( w ( r ( x ` w ) = ( y ` w ) ) <-> ( w ( r ( x ` w ) = ( y ` w ) ) ) ) |
45 |
36 44
|
raleqbidv |
|- ( ( ( ( i = I /\ s = R ) /\ p = ( i mPwSer s ) ) /\ d = D ) -> ( A. w e. d ( w ( r ( x ` w ) = ( y ` w ) ) <-> A. w e. D ( w ( r ( x ` w ) = ( y ` w ) ) ) ) |
46 |
40 45
|
anbi12d |
|- ( ( ( ( i = I /\ s = R ) /\ p = ( i mPwSer s ) ) /\ d = D ) -> ( ( ( x ` z ) ( lt ` s ) ( y ` z ) /\ A. w e. d ( w ( r ( x ` w ) = ( y ` w ) ) ) <-> ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w ( r ( x ` w ) = ( y ` w ) ) ) ) ) |
47 |
36 46
|
rexeqbidv |
|- ( ( ( ( i = I /\ s = R ) /\ p = ( i mPwSer s ) ) /\ d = D ) -> ( E. z e. d ( ( x ` z ) ( lt ` s ) ( y ` z ) /\ A. w e. d ( w ( r ( x ` w ) = ( y ` w ) ) ) <-> E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w ( r ( x ` w ) = ( y ` w ) ) ) ) ) |
48 |
30 35 47
|
sbcied2 |
|- ( ( ( i = I /\ s = R ) /\ p = ( i mPwSer s ) ) -> ( [. { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } / d ]. E. z e. d ( ( x ` z ) ( lt ` s ) ( y ` z ) /\ A. w e. d ( w ( r ( x ` w ) = ( y ` w ) ) ) <-> E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w ( r ( x ` w ) = ( y ` w ) ) ) ) ) |
49 |
48
|
orbi1d |
|- ( ( ( i = I /\ s = R ) /\ p = ( i mPwSer s ) ) -> ( ( [. { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } / d ]. E. z e. d ( ( x ` z ) ( lt ` s ) ( y ` z ) /\ A. w e. d ( w ( r ( x ` w ) = ( y ` w ) ) ) \/ x = y ) <-> ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w ( r ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) ) |
50 |
27 49
|
anbi12d |
|- ( ( ( i = I /\ s = R ) /\ p = ( i mPwSer s ) ) -> ( ( { x , y } C_ ( Base ` p ) /\ ( [. { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } / d ]. E. z e. d ( ( x ` z ) ( lt ` s ) ( y ` z ) /\ A. w e. d ( w ( r ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) <-> ( { x , y } C_ B /\ ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w ( r ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) ) ) |
51 |
50
|
opabbidv |
|- ( ( ( i = I /\ s = R ) /\ p = ( i mPwSer s ) ) -> { <. x , y >. | ( { x , y } C_ ( Base ` p ) /\ ( [. { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } / d ]. E. z e. d ( ( x ` z ) ( lt ` s ) ( y ` z ) /\ A. w e. d ( w ( r ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } = { <. x , y >. | ( { x , y } C_ B /\ ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w ( r ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } ) |
52 |
51
|
opeq2d |
|- ( ( ( i = I /\ s = R ) /\ p = ( i mPwSer s ) ) -> <. ( le ` ndx ) , { <. x , y >. | ( { x , y } C_ ( Base ` p ) /\ ( [. { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } / d ]. E. z e. d ( ( x ` z ) ( lt ` s ) ( y ` z ) /\ A. w e. d ( w ( r ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } >. = <. ( le ` ndx ) , { <. x , y >. | ( { x , y } C_ B /\ ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w ( r ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } >. ) |
53 |
24 52
|
oveq12d |
|- ( ( ( i = I /\ s = R ) /\ p = ( i mPwSer s ) ) -> ( p sSet <. ( le ` ndx ) , { <. x , y >. | ( { x , y } C_ ( Base ` p ) /\ ( [. { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } / d ]. E. z e. d ( ( x ` z ) ( lt ` s ) ( y ` z ) /\ A. w e. d ( w ( r ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } >. ) = ( S sSet <. ( le ` ndx ) , { <. x , y >. | ( { x , y } C_ B /\ ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w ( r ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } >. ) ) |
54 |
20 53
|
csbied |
|- ( ( i = I /\ s = R ) -> [_ ( i mPwSer s ) / p ]_ ( p sSet <. ( le ` ndx ) , { <. x , y >. | ( { x , y } C_ ( Base ` p ) /\ ( [. { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } / d ]. E. z e. d ( ( x ` z ) ( lt ` s ) ( y ` z ) /\ A. w e. d ( w ( r ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } >. ) = ( S sSet <. ( le ` ndx ) , { <. x , y >. | ( { x , y } C_ B /\ ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w ( r ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } >. ) ) |
55 |
19 54
|
mpteq12dv |
|- ( ( i = I /\ s = R ) -> ( r e. ~P ( i X. i ) |-> [_ ( i mPwSer s ) / p ]_ ( p sSet <. ( le ` ndx ) , { <. x , y >. | ( { x , y } C_ ( Base ` p ) /\ ( [. { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } / d ]. E. z e. d ( ( x ` z ) ( lt ` s ) ( y ` z ) /\ A. w e. d ( w ( r ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } >. ) ) = ( r e. ~P ( I X. I ) |-> ( S sSet <. ( le ` ndx ) , { <. x , y >. | ( { x , y } C_ B /\ ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w ( r ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } >. ) ) ) |
56 |
|
df-opsr |
|- ordPwSer = ( i e. _V , s e. _V |-> ( r e. ~P ( i X. i ) |-> [_ ( i mPwSer s ) / p ]_ ( p sSet <. ( le ` ndx ) , { <. x , y >. | ( { x , y } C_ ( Base ` p ) /\ ( [. { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } / d ]. E. z e. d ( ( x ` z ) ( lt ` s ) ( y ` z ) /\ A. w e. d ( w ( r ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } >. ) ) ) |
57 |
55 56
|
ovmpoga |
|- ( ( I e. _V /\ R e. _V /\ ( r e. ~P ( I X. I ) |-> ( S sSet <. ( le ` ndx ) , { <. x , y >. | ( { x , y } C_ B /\ ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w ( r ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } >. ) ) e. _V ) -> ( I ordPwSer R ) = ( r e. ~P ( I X. I ) |-> ( S sSet <. ( le ` ndx ) , { <. x , y >. | ( { x , y } C_ B /\ ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w ( r ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } >. ) ) ) |
58 |
11 12 16 57
|
syl3anc |
|- ( ph -> ( I ordPwSer R ) = ( r e. ~P ( I X. I ) |-> ( S sSet <. ( le ` ndx ) , { <. x , y >. | ( { x , y } C_ B /\ ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w ( r ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } >. ) ) ) |
59 |
|
simpr |
|- ( ( ph /\ r = T ) -> r = T ) |
60 |
59
|
oveq1d |
|- ( ( ph /\ r = T ) -> ( r |
61 |
60 5
|
eqtr4di |
|- ( ( ph /\ r = T ) -> ( r |
62 |
61
|
breqd |
|- ( ( ph /\ r = T ) -> ( w ( r w C z ) ) |
63 |
62
|
imbi1d |
|- ( ( ph /\ r = T ) -> ( ( w ( r ( x ` w ) = ( y ` w ) ) <-> ( w C z -> ( x ` w ) = ( y ` w ) ) ) ) |
64 |
63
|
ralbidv |
|- ( ( ph /\ r = T ) -> ( A. w e. D ( w ( r ( x ` w ) = ( y ` w ) ) <-> A. w e. D ( w C z -> ( x ` w ) = ( y ` w ) ) ) ) |
65 |
64
|
anbi2d |
|- ( ( ph /\ r = T ) -> ( ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w ( r ( x ` w ) = ( y ` w ) ) ) <-> ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w C z -> ( x ` w ) = ( y ` w ) ) ) ) ) |
66 |
65
|
rexbidv |
|- ( ( ph /\ r = T ) -> ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w ( r ( x ` w ) = ( y ` w ) ) ) <-> E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w C z -> ( x ` w ) = ( y ` w ) ) ) ) ) |
67 |
66
|
orbi1d |
|- ( ( ph /\ r = T ) -> ( ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w ( r ( x ` w ) = ( y ` w ) ) ) \/ x = y ) <-> ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w C z -> ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) ) |
68 |
67
|
anbi2d |
|- ( ( ph /\ r = T ) -> ( ( { x , y } C_ B /\ ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w ( r ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) <-> ( { x , y } C_ B /\ ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w C z -> ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) ) ) |
69 |
68
|
opabbidv |
|- ( ( ph /\ r = T ) -> { <. x , y >. | ( { x , y } C_ B /\ ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w ( r ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } = { <. x , y >. | ( { x , y } C_ B /\ ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w C z -> ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } ) |
70 |
69 7
|
eqtr4di |
|- ( ( ph /\ r = T ) -> { <. x , y >. | ( { x , y } C_ B /\ ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w ( r ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } = .<_ ) |
71 |
70
|
opeq2d |
|- ( ( ph /\ r = T ) -> <. ( le ` ndx ) , { <. x , y >. | ( { x , y } C_ B /\ ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w ( r ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } >. = <. ( le ` ndx ) , .<_ >. ) |
72 |
71
|
oveq2d |
|- ( ( ph /\ r = T ) -> ( S sSet <. ( le ` ndx ) , { <. x , y >. | ( { x , y } C_ B /\ ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w ( r ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } >. ) = ( S sSet <. ( le ` ndx ) , .<_ >. ) ) |
73 |
13 10
|
sselpwd |
|- ( ph -> T e. ~P ( I X. I ) ) |
74 |
|
ovexd |
|- ( ph -> ( S sSet <. ( le ` ndx ) , .<_ >. ) e. _V ) |
75 |
58 72 73 74
|
fvmptd |
|- ( ph -> ( ( I ordPwSer R ) ` T ) = ( S sSet <. ( le ` ndx ) , .<_ >. ) ) |
76 |
2 75
|
syl5eq |
|- ( ph -> O = ( S sSet <. ( le ` ndx ) , .<_ >. ) ) |