Definition df-opsr 19360

Description: Define a total order on the set of all power series in s from the index set i given a wellordering r of i and a totally ordered base ring s. (Contributed by Mario Carneiro, 8-Feb-2015.)

Assertion

Ref	Expression
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 <bag i ) z -> ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } >. ) ) )

Distinct variable group:   h, d, i, p, r, s, w, x, y, z

Detailed syntax breakdown of Definition df-opsr

Step	Hyp	Ref	Expression
1		copws 19355	. 2 class ordPwSer
2		vi	. . 3 setvar i
3		vs	. . 3 setvar s
4		cvv 3200	. . 3 class _V
5		vr	. . . 4 setvar r
6	2	cv 1482	. . . . . 6 class i
7	6, 6	cxp 5112	. . . . 5 class ( i X. i )
8	7	cpw 4158	. . . 4 class ~P ( i X. i )
9		vp	. . . . 5 setvar p
10	3	cv 1482	. . . . . 6 class s
11		cmps 19351	. . . . . 6 class mPwSer
12	6, 10, 11	co 6650	. . . . 5 class ( i mPwSer s )
13	9	cv 1482	. . . . . 6 class p
14		cnx 15854	. . . . . . . 8 class ndx
15		cple 15948	. . . . . . . 8 class le
16	14, 15	cfv 5888	. . . . . . 7 class ( le ` ndx )
17		vx	. . . . . . . . . . . 12 setvar x
18	17	cv 1482	. . . . . . . . . . 11 class x
19		vy	. . . . . . . . . . . 12 setvar y
20	19	cv 1482	. . . . . . . . . . 11 class y
21	18, 20	cpr 4179	. . . . . . . . . 10 class { x , y }
22		cbs 15857	. . . . . . . . . . 11 class Base
23	13, 22	cfv 5888	. . . . . . . . . 10 class ( Base ` p )
24	21, 23	wss 3574	. . . . . . . . 9 wff { x , y } C_ ( Base ` p )
25		vz	. . . . . . . . . . . . . . . 16 setvar z
26	25	cv 1482	. . . . . . . . . . . . . . 15 class z
27	26, 18	cfv 5888	. . . . . . . . . . . . . 14 class ( x ` z )
28	26, 20	cfv 5888	. . . . . . . . . . . . . 14 class ( y ` z )
29		cplt 16941	. . . . . . . . . . . . . . 15 class lt
30	10, 29	cfv 5888	. . . . . . . . . . . . . 14 class ( lt ` s )
31	27, 28, 30	wbr 4653	. . . . . . . . . . . . 13 wff ( x ` z ) ( lt ` s ) ( y ` z )
32		vw	. . . . . . . . . . . . . . . . 17 setvar w
33	32	cv 1482	. . . . . . . . . . . . . . . 16 class w
34	5	cv 1482	. . . . . . . . . . . . . . . . 17 class r
35		cltb 19354	. . . . . . . . . . . . . . . . 17 class <bag
36	34, 6, 35	co 6650	. . . . . . . . . . . . . . . 16 class ( r <bag i )
37	33, 26, 36	wbr 4653	. . . . . . . . . . . . . . 15 wff w ( r <bag i ) z
38	33, 18	cfv 5888	. . . . . . . . . . . . . . . 16 class ( x ` w )
39	33, 20	cfv 5888	. . . . . . . . . . . . . . . 16 class ( y ` w )
40	38, 39	wceq 1483	. . . . . . . . . . . . . . 15 wff ( x ` w ) = ( y ` w )
41	37, 40	wi 4	. . . . . . . . . . . . . 14 wff ( w ( r <bag i ) z -> ( x ` w ) = ( y ` w ) )
42		vd	. . . . . . . . . . . . . . 15 setvar d
43	42	cv 1482	. . . . . . . . . . . . . 14 class d
44	41, 32, 43	wral 2912	. . . . . . . . . . . . 13 wff A. w e. d ( w ( r <bag i ) z -> ( x ` w ) = ( y ` w ) )
45	31, 44	wa 384	. . . . . . . . . . . 12 wff ( ( x ` z ) ( lt ` s ) ( y ` z ) /\ A. w e. d ( w ( r <bag i ) z -> ( x ` w ) = ( y ` w ) ) )
46	45, 25, 43	wrex 2913	. . . . . . . . . . 11 wff E. z e. d ( ( x ` z ) ( lt ` s ) ( y ` z ) /\ A. w e. d ( w ( r <bag i ) z -> ( x ` w ) = ( y ` w ) ) )
47		vh	. . . . . . . . . . . . . . . 16 setvar h
48	47	cv 1482	. . . . . . . . . . . . . . 15 class h
49	48	ccnv 5113	. . . . . . . . . . . . . 14 class `' h
50		cn 11020	. . . . . . . . . . . . . 14 class NN
51	49, 50	cima 5117	. . . . . . . . . . . . 13 class ( `' h " NN )
52		cfn 7955	. . . . . . . . . . . . 13 class Fin
53	51, 52	wcel 1990	. . . . . . . . . . . 12 wff ( `' h " NN ) e. Fin
54		cn0 11292	. . . . . . . . . . . . 13 class NN0
55		cmap 7857	. . . . . . . . . . . . 13 class ^m
56	54, 6, 55	co 6650	. . . . . . . . . . . 12 class ( NN0 ^m i )
57	53, 47, 56	crab 2916	. . . . . . . . . . 11 class { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin }
58	46, 42, 57	wsbc 3435	. . . . . . . . . 10 wff [. { 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 ) ) )
59	17, 19	weq 1874	. . . . . . . . . 10 wff x = y
60	58, 59	wo 383	. . . . . . . . 9 wff ( [. { 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 )
61	24, 60	wa 384	. . . . . . . 8 wff ( { 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 ) )
62	61, 17, 19	copab 4712	. . . . . . 7 class { <. 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 ) ) }
63	16, 62	cop 4183	. . . . . 6 class <. ( 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 ) ) } >.
64		csts 15855	. . . . . 6 class sSet
65	13, 63, 64	co 6650	. . . . 5 class ( 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 ) ) } >. )
66	9, 12, 65	csb 3533	. . . 4 class [_ ( 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 ) ) } >. )
67	5, 8, 66	cmpt 4729	. . 3 class ( 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 ) ) } >. ) )
68	2, 3, 4, 4, 67	cmpt2 6652	. 2 class ( 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 ) ) } >. ) ) )
69	1, 68	wceq 1483	1 wff 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 ) ) } >. ) ) )

This definition is referenced by:  reldmopsr  19473  opsrval  19474