Theorem opsrval 19474

Description: The value of the "ordered power series" function. This is the same as mPwSer psrval 19362, but with the addition of a well-order on I we can turn a strict order on R into a strict order on the power series structure. (Contributed by Mario Carneiro, 8-Feb-2015.)

Hypotheses

Ref	Expression
opsrval.s	|- S = ( I mPwSer R )
opsrval.o	|- O = ( ( I ordPwSer R ) ` T )
opsrval.b	|- B = ( Base ` S )
opsrval.q	|- .< = ( lt ` R )
opsrval.c	|- C = ( T <bag I )
opsrval.d	|- D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
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 ) ) }
opsrval.i	|- ( ph -> I e. V )
opsrval.r	|- ( ph -> R e. W )
opsrval.t	|- ( ph -> T C_ ( I X. I ) )

Assertion

Ref	Expression
opsrval	|- ( ph -> O = ( S sSet <. ( le ` ndx ) , .<_ >. ) )

Distinct variable groups:   w, h, x, y, z, I   ph, w, x, y, z   w, D, z   w, T, x, y, z   w, R, x, y, z

Allowed substitution hints:   ph( h)   B( x, y, z, w, h)   C( x, y, z, w, h)   D( x, y, h)   R( h)   S( x, y, z, w, h)   .< ( x, y, z, w, h)   T( h)   .<_ ( x, y, z, w, h)   O( x, y, z, w, h)   V( x, y, z, w, h)   W( x, y, z, w, h)

Proof of Theorem opsrval

Dummy variables r i p s d are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		opsrval.o	. 2 |- O = ( ( I ordPwSer R ) ` T )
2		opsrval.i	. . . . 5 |- ( ph -> I e. V )
3		elex 3212	. . . . 5 |- ( I e. V -> I e. _V )
4	2, 3	syl 17	. . . 4 |- ( ph -> I e. _V )
5		opsrval.r	. . . . 5 |- ( ph -> R e. W )
6		elex 3212	. . . . 5 |- ( R e. W -> R e. _V )
7	5, 6	syl 17	. . . 4 |- ( ph -> R e. _V )
8		xpexg 6960	. . . . . 6 |- ( ( I e. V /\ I e. V ) -> ( I X. I ) e. _V )
9	2, 2, 8	syl2anc 693	. . . . 5 |- ( ph -> ( I X. I ) e. _V )
10		pwexg 4850	. . . . 5 |- ( ( I X. I ) e. _V -> ~P ( I X. I ) e. _V )
11		mptexg 6484	. . . . 5 |- ( ~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 <bag I ) z -> ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } >. ) ) e. _V )
12	9, 10, 11	3syl 18	. . . 4 |- ( 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 <bag I ) z -> ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } >. ) ) e. _V )
13		simpl 473	. . . . . . . 8 |- ( ( i = I /\ s = R ) -> i = I )
14	13	sqxpeqd 5141	. . . . . . 7 |- ( ( i = I /\ s = R ) -> ( i X. i ) = ( I X. I ) )
15	14	pweqd 4163	. . . . . 6 |- ( ( i = I /\ s = R ) -> ~P ( i X. i ) = ~P ( I X. I ) )
16		ovexd 6680	. . . . . . 7 |- ( ( i = I /\ s = R ) -> ( i mPwSer s ) e. _V )
17		id 22	. . . . . . . . . 10 |- ( p = ( i mPwSer s ) -> p = ( i mPwSer s ) )
18		oveq12 6659	. . . . . . . . . 10 |- ( ( i = I /\ s = R ) -> ( i mPwSer s ) = ( I mPwSer R ) )
19	17, 18	sylan9eqr 2678	. . . . . . . . 9 |- ( ( ( i = I /\ s = R ) /\ p = ( i mPwSer s ) ) -> p = ( I mPwSer R ) )
20		opsrval.s	. . . . . . . . 9 |- S = ( I mPwSer R )
21	19, 20	syl6eqr 2674	. . . . . . . 8 |- ( ( ( i = I /\ s = R ) /\ p = ( i mPwSer s ) ) -> p = S )
22	21	fveq2d 6195	. . . . . . . . . . . . 13 |- ( ( ( i = I /\ s = R ) /\ p = ( i mPwSer s ) ) -> ( Base ` p ) = ( Base ` S ) )
23		opsrval.b	. . . . . . . . . . . . 13 |- B = ( Base ` S )
24	22, 23	syl6eqr 2674	. . . . . . . . . . . 12 |- ( ( ( i = I /\ s = R ) /\ p = ( i mPwSer s ) ) -> ( Base ` p ) = B )
25	24	sseq2d 3633	. . . . . . . . . . 11 |- ( ( ( i = I /\ s = R ) /\ p = ( i mPwSer s ) ) -> ( { x , y } C_ ( Base ` p ) <-> { x , y } C_ B ) )
26		ovex 6678	. . . . . . . . . . . . . . 15 |- ( NN0 ^m i ) e. _V
27	26	rabex 4813	. . . . . . . . . . . . . 14 |- { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } e. _V
28	27	a1i 11	. . . . . . . . . . . . 13 |- ( ( ( i = I /\ s = R ) /\ p = ( i mPwSer s ) ) -> { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } e. _V )
29	13	adantr 481	. . . . . . . . . . . . . . . 16 |- ( ( ( i = I /\ s = R ) /\ p = ( i mPwSer s ) ) -> i = I )
30	29	oveq2d 6666	. . . . . . . . . . . . . . 15 |- ( ( ( i = I /\ s = R ) /\ p = ( i mPwSer s ) ) -> ( NN0 ^m i ) = ( NN0 ^m I ) )
31		rabeq 3192	. . . . . . . . . . . . . . 15 |- ( ( NN0 ^m i ) = ( NN0 ^m I ) -> { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
32	30, 31	syl 17	. . . . . . . . . . . . . 14 |- ( ( ( 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 } )
33		opsrval.d	. . . . . . . . . . . . . 14 |- D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
34	32, 33	syl6eqr 2674	. . . . . . . . . . . . 13 |- ( ( ( i = I /\ s = R ) /\ p = ( i mPwSer s ) ) -> { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } = D )
35		simpr 477	. . . . . . . . . . . . . 14 |- ( ( ( ( i = I /\ s = R ) /\ p = ( i mPwSer s ) ) /\ d = D ) -> d = D )
36		simpllr 799	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( i = I /\ s = R ) /\ p = ( i mPwSer s ) ) /\ d = D ) -> s = R )
37	36	fveq2d 6195	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( i = I /\ s = R ) /\ p = ( i mPwSer s ) ) /\ d = D ) -> ( lt ` s ) = ( lt ` R ) )
38		opsrval.q	. . . . . . . . . . . . . . . . 17 |- .< = ( lt ` R )
39	37, 38	syl6eqr 2674	. . . . . . . . . . . . . . . 16 |- ( ( ( ( i = I /\ s = R ) /\ p = ( i mPwSer s ) ) /\ d = D ) -> ( lt ` s ) = .< )
40	39	breqd 4664	. . . . . . . . . . . . . . 15 |- ( ( ( ( i = I /\ s = R ) /\ p = ( i mPwSer s ) ) /\ d = D ) -> ( ( x ` z ) ( lt ` s ) ( y ` z ) <-> ( x ` z ) .< ( y ` z ) ) )
41	29	adantr 481	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( i = I /\ s = R ) /\ p = ( i mPwSer s ) ) /\ d = D ) -> i = I )
42	41	oveq2d 6666	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( i = I /\ s = R ) /\ p = ( i mPwSer s ) ) /\ d = D ) -> ( r <bag i ) = ( r <bag I ) )
43	42	breqd 4664	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( i = I /\ s = R ) /\ p = ( i mPwSer s ) ) /\ d = D ) -> ( w ( r <bag i ) z <-> w ( r <bag I ) z ) )
44	43	imbi1d 331	. . . . . . . . . . . . . . . 16 |- ( ( ( ( i = I /\ s = R ) /\ p = ( i mPwSer s ) ) /\ d = D ) -> ( ( w ( r <bag i ) z -> ( x ` w ) = ( y ` w ) ) <-> ( w ( r <bag I ) z -> ( x ` w ) = ( y ` w ) ) ) )
45	35, 44	raleqbidv 3152	. . . . . . . . . . . . . . 15 |- ( ( ( ( i = I /\ s = R ) /\ p = ( i mPwSer s ) ) /\ d = D ) -> ( A. w e. d ( w ( r <bag i ) z -> ( x ` w ) = ( y ` w ) ) <-> A. w e. D ( w ( r <bag I ) z -> ( x ` w ) = ( y ` w ) ) ) )
46	40, 45	anbi12d 747	. . . . . . . . . . . . . 14 |- ( ( ( ( i = I /\ s = R ) /\ p = ( i mPwSer s ) ) /\ d = D ) -> ( ( ( x ` z ) ( lt ` s ) ( y ` z ) /\ A. w e. d ( w ( r <bag i ) z -> ( x ` w ) = ( y ` w ) ) ) <-> ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w ( r <bag I ) z -> ( x ` w ) = ( y ` w ) ) ) ) )
47	35, 46	rexeqbidv 3153	. . . . . . . . . . . . 13 |- ( ( ( ( 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 <bag i ) z -> ( x ` w ) = ( y ` w ) ) ) <-> E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w ( r <bag I ) z -> ( x ` w ) = ( y ` w ) ) ) ) )
48	28, 34, 47	sbcied2 3473	. . . . . . . . . . . 12 |- ( ( ( 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 <bag i ) z -> ( x ` w ) = ( y ` w ) ) ) <-> E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w ( r <bag I ) z -> ( x ` w ) = ( y ` w ) ) ) ) )
49	48	orbi1d 739	. . . . . . . . . . 11 |- ( ( ( 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 <bag i ) z -> ( x ` w ) = ( y ` w ) ) ) \/ x = y ) <-> ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w ( r <bag I ) z -> ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) )
50	25, 49	anbi12d 747	. . . . . . . . . 10 |- ( ( ( 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 <bag i ) z -> ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) <-> ( { x , y } C_ B /\ ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w ( r <bag I ) z -> ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) ) )
51	50	opabbidv 4716	. . . . . . . . 9 |- ( ( ( 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 <bag i ) z -> ( 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 <bag I ) z -> ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } )
52	51	opeq2d 4409	. . . . . . . 8 |- ( ( ( 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 <bag i ) z -> ( 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 <bag I ) z -> ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } >. )
53	21, 52	oveq12d 6668	. . . . . . 7 |- ( ( ( 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 <bag i ) z -> ( 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 <bag I ) z -> ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } >. ) )
54	16, 53	csbied 3560	. . . . . 6 |- ( ( 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 <bag i ) z -> ( 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 <bag I ) z -> ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } >. ) )
55	15, 54	mpteq12dv 4733	. . . . 5 |- ( ( 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 <bag i ) z -> ( 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 <bag I ) z -> ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } >. ) ) )
56		df-opsr 19360	. . . . 5 |- 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 <bag i ) z -> ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } >. ) ) )
57	55, 56	ovmpt2ga 6790	. . . 4 |- ( ( 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 <bag I ) z -> ( 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 <bag I ) z -> ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } >. ) ) )
58	4, 7, 12, 57	syl3anc 1326	. . 3 |- ( 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 <bag I ) z -> ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } >. ) ) )
59		simpr 477	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ r = T ) -> r = T )
60	59	oveq1d 6665	. . . . . . . . . . . . . . 15 |- ( ( ph /\ r = T ) -> ( r <bag I ) = ( T <bag I ) )
61		opsrval.c	. . . . . . . . . . . . . . 15 |- C = ( T <bag I )
62	60, 61	syl6eqr 2674	. . . . . . . . . . . . . 14 |- ( ( ph /\ r = T ) -> ( r <bag I ) = C )
63	62	breqd 4664	. . . . . . . . . . . . 13 |- ( ( ph /\ r = T ) -> ( w ( r <bag I ) z <-> w C z ) )
64	63	imbi1d 331	. . . . . . . . . . . 12 |- ( ( ph /\ r = T ) -> ( ( w ( r <bag I ) z -> ( x ` w ) = ( y ` w ) ) <-> ( w C z -> ( x ` w ) = ( y ` w ) ) ) )
65	64	ralbidv 2986	. . . . . . . . . . 11 |- ( ( ph /\ r = T ) -> ( A. w e. D ( w ( r <bag I ) z -> ( x ` w ) = ( y ` w ) ) <-> A. w e. D ( w C z -> ( x ` w ) = ( y ` w ) ) ) )
66	65	anbi2d 740	. . . . . . . . . 10 |- ( ( ph /\ r = T ) -> ( ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w ( r <bag I ) z -> ( x ` w ) = ( y ` w ) ) ) <-> ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w C z -> ( x ` w ) = ( y ` w ) ) ) ) )
67	66	rexbidv 3052	. . . . . . . . 9 |- ( ( ph /\ r = T ) -> ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w ( r <bag I ) z -> ( x ` w ) = ( y ` w ) ) ) <-> E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w C z -> ( x ` w ) = ( y ` w ) ) ) ) )
68	67	orbi1d 739	. . . . . . . 8 |- ( ( ph /\ r = T ) -> ( ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w ( r <bag I ) z -> ( 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 ) ) )
69	68	anbi2d 740	. . . . . . 7 |- ( ( ph /\ r = T ) -> ( ( { x , y } C_ B /\ ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w ( r <bag I ) z -> ( 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 ) ) ) )
70	69	opabbidv 4716	. . . . . 6 |- ( ( ph /\ r = T ) -> { <. x , y >. | ( { x , y } C_ B /\ ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w ( r <bag I ) z -> ( 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 ) ) } )
71		opsrval.l	. . . . . 6 |- .<_ = { <. 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 ) ) }
72	70, 71	syl6eqr 2674	. . . . 5 |- ( ( ph /\ r = T ) -> { <. x , y >. | ( { x , y } C_ B /\ ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w ( r <bag I ) z -> ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } = .<_ )
73	72	opeq2d 4409	. . . 4 |- ( ( 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 <bag I ) z -> ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } >. = <. ( le ` ndx ) , .<_ >. )
74	73	oveq2d 6666	. . 3 |- ( ( 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 <bag I ) z -> ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } >. ) = ( S sSet <. ( le ` ndx ) , .<_ >. ) )
75		opsrval.t	. . . 4 |- ( ph -> T C_ ( I X. I ) )
76		elpw2g 4827	. . . . 5 |- ( ( I X. I ) e. _V -> ( T e. ~P ( I X. I ) <-> T C_ ( I X. I ) ) )
77	9, 76	syl 17	. . . 4 |- ( ph -> ( T e. ~P ( I X. I ) <-> T C_ ( I X. I ) ) )
78	75, 77	mpbird 247	. . 3 |- ( ph -> T e. ~P ( I X. I ) )
79		ovexd 6680	. . 3 |- ( ph -> ( S sSet <. ( le ` ndx ) , .<_ >. ) e. _V )
80	58, 74, 78, 79	fvmptd 6288	. 2 |- ( ph -> ( ( I ordPwSer R ) ` T ) = ( S sSet <. ( le ` ndx ) , .<_ >. ) )
81	1, 80	syl5eq 2668	1 |- ( ph -> O = ( S sSet <. ( le ` ndx ) , .<_ >. ) )

Syntax hints:   -> wi 4   <-> wb 196   \/ wo 383   /\ wa 384   = wceq 1483   e. wcel 1990   A.wral 2912   E.wrex 2913   {crab 2916   _Vcvv 3200   [.wsbc 3435   [_csb 3533   C_ wss 3574   ~Pcpw 4158   {cpr 4179   <.cop 4183   class class class wbr 4653   {copab 4712   |-> cmpt 4729   X. cxp 5112   `'ccnv 5113   "cima 5117   ` cfv 5888  (class class class)co 6650   ^m cmap 7857   Fincfn 7955   NNcn 11020   NN0cn0 11292   ndxcnx 15854   sSet csts 15855   Basecbs 15857   lecple 15948   ltcplt 16941   mPwSer cmps 19351   <_bag cltb 19354   ordPwSer copws 19355

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-opsr 19360

This theorem is referenced by:  opsrle  19475  opsrval2  19476