Theorem opsrtoslem2

Description: Lemma for opsrtos . (Contributed by Mario Carneiro, 8-Feb-2015)

	Ref	Expression
Hypotheses	opsrso.o	|- O = ( ( I ordPwSer R ) ` T )
	opsrso.i	|- ( ph -> I e. V )
	opsrso.r	|- ( ph -> R e. Toset )
	opsrso.t	|- ( ph -> T C_ ( I X. I ) )
	opsrso.w	|- ( ph -> T We I )
	opsrtoslem.s	|- S = ( I mPwSer R )
	opsrtoslem.b	|- B = ( Base ` S )
	opsrtoslem.q	|- .< = ( lt ` R )
	opsrtoslem.c	|- C = ( T
	opsrtoslem.d	|- D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
	opsrtoslem.ps	|- ( ps <-> E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w C z -> ( x ` w ) = ( y ` w ) ) ) )
	opsrtoslem.l	|- .<_ = ( le ` O )
Assertion	opsrtoslem2	|- ( ph -> O e. Toset )

Proof

Step	Hyp	Ref	Expression
1		opsrso.o	|- O = ( ( I ordPwSer R ) ` T )
2		opsrso.i	|- ( ph -> I e. V )
3		opsrso.r	|- ( ph -> R e. Toset )
4		opsrso.t	|- ( ph -> T C_ ( I X. I ) )
5		opsrso.w	|- ( ph -> T We I )
6		opsrtoslem.s	|- S = ( I mPwSer R )
7		opsrtoslem.b	|- B = ( Base ` S )
8		opsrtoslem.q	|- .< = ( lt ` R )
9		opsrtoslem.c	|- C = ( T
10		opsrtoslem.d	|- D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
11		opsrtoslem.ps	|- ( ps <-> E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w C z -> ( x ` w ) = ( y ` w ) ) ) )
12		opsrtoslem.l	|- .<_ = ( le ` O )
13		ovex	|- ( NN0 ^m I ) e. _V
14	10 13	rabex2	|- D e. _V
15	2 2	xpexd	|- ( ph -> ( I X. I ) e. _V )
16	15 4	ssexd	|- ( ph -> T e. _V )
17	9 10 2 16 5	ltbwe	|- ( ph -> C We D )
18		eqid	|- ( Base ` R ) = ( Base ` R )
19		eqid	|- ( le ` R ) = ( le ` R )
20	18 19 8	tosso	|- ( R e. Toset -> ( R e. Toset <-> ( .< Or ( Base ` R ) /\ ( _I |` ( Base ` R ) ) C_ ( le ` R ) ) ) )
21	20	ibi	|- ( R e. Toset -> ( .< Or ( Base ` R ) /\ ( _I |` ( Base ` R ) ) C_ ( le ` R ) ) )
22	3 21	syl	|- ( ph -> ( .< Or ( Base ` R ) /\ ( _I |` ( Base ` R ) ) C_ ( le ` R ) ) )
23	22	simpld	|- ( ph -> .< Or ( Base ` R ) )
24	11	opabbii	|- { <. x , y >. | ps } = { <. x , y >. | E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w C z -> ( x ` w ) = ( y ` w ) ) ) }
25	24	wemapso	|- ( ( D e. _V /\ C We D /\ .< Or ( Base ` R ) ) -> { <. x , y >. | ps } Or ( ( Base ` R ) ^m D ) )
26	14 17 23 25	mp3an2i	|- ( ph -> { <. x , y >. | ps } Or ( ( Base ` R ) ^m D ) )
27	6 18 10 7 2	psrbas	|- ( ph -> B = ( ( Base ` R ) ^m D ) )
28		soeq2	|- ( B = ( ( Base ` R ) ^m D ) -> ( { <. x , y >. | ps } Or B <-> { <. x , y >. | ps } Or ( ( Base ` R ) ^m D ) ) )
29	27 28	syl	|- ( ph -> ( { <. x , y >. | ps } Or B <-> { <. x , y >. | ps } Or ( ( Base ` R ) ^m D ) ) )
30	26 29	mpbird	|- ( ph -> { <. x , y >. | ps } Or B )
31		soinxp	|- ( { <. x , y >. | ps } Or B <-> ( { <. x , y >. | ps } i^i ( B X. B ) ) Or B )
32	30 31	sylib	|- ( ph -> ( { <. x , y >. | ps } i^i ( B X. B ) ) Or B )
33	1	fvexi	|- O e. _V
34		eqid	|- ( lt ` O ) = ( lt ` O )
35	12 34	pltfval	|- ( O e. _V -> ( lt ` O ) = ( .<_ \ _I ) )
36	33 35	ax-mp	|- ( lt ` O ) = ( .<_ \ _I )
37		difundir	|- ( ( ( { <. x , y >. | ps } i^i ( B X. B ) ) u. ( _I |` B ) ) \ _I ) = ( ( ( { <. x , y >. | ps } i^i ( B X. B ) ) \ _I ) u. ( ( _I |` B ) \ _I ) )
38		resss	|- ( _I |` B ) C_ _I
39		ssdif0	|- ( ( _I |` B ) C_ _I <-> ( ( _I |` B ) \ _I ) = (/) )
40	38 39	mpbi	|- ( ( _I |` B ) \ _I ) = (/)
41	40	uneq2i	|- ( ( ( { <. x , y >. | ps } i^i ( B X. B ) ) \ _I ) u. ( ( _I |` B ) \ _I ) ) = ( ( ( { <. x , y >. | ps } i^i ( B X. B ) ) \ _I ) u. (/) )
42		un0	|- ( ( ( { <. x , y >. | ps } i^i ( B X. B ) ) \ _I ) u. (/) ) = ( ( { <. x , y >. | ps } i^i ( B X. B ) ) \ _I )
43	37 41 42	3eqtri	|- ( ( ( { <. x , y >. | ps } i^i ( B X. B ) ) u. ( _I |` B ) ) \ _I ) = ( ( { <. x , y >. | ps } i^i ( B X. B ) ) \ _I )
44	1 2 3 4 5 6 7 8 9 10 11 12	opsrtoslem1	|- ( ph -> .<_ = ( ( { <. x , y >. | ps } i^i ( B X. B ) ) u. ( _I |` B ) ) )
45	44	difeq1d	|- ( ph -> ( .<_ \ _I ) = ( ( ( { <. x , y >. | ps } i^i ( B X. B ) ) u. ( _I |` B ) ) \ _I ) )
46		relinxp	|- Rel ( { <. x , y >. | ps } i^i ( B X. B ) )
47	46	a1i	|- ( ph -> Rel ( { <. x , y >. | ps } i^i ( B X. B ) ) )
48		df-br	|- ( a _I b <-> <. a , b >. e. _I )
49		vex	|- b e. _V
50	49	ideq	|- ( a _I b <-> a = b )
51	48 50	bitr3i	|- ( <. a , b >. e. _I <-> a = b )
52		brin	|- ( a ( { <. x , y >. | ps } i^i ( B X. B ) ) a <-> ( a { <. x , y >. | ps } a /\ a ( B X. B ) a ) )
53	52	simprbi	|- ( a ( { <. x , y >. | ps } i^i ( B X. B ) ) a -> a ( B X. B ) a )
54		brxp	|- ( a ( B X. B ) a <-> ( a e. B /\ a e. B ) )
55	54	simprbi	|- ( a ( B X. B ) a -> a e. B )
56	53 55	syl	|- ( a ( { <. x , y >. | ps } i^i ( B X. B ) ) a -> a e. B )
57		sonr	|- ( ( ( { <. x , y >. | ps } i^i ( B X. B ) ) Or B /\ a e. B ) -> -. a ( { <. x , y >. | ps } i^i ( B X. B ) ) a )
58	57	ex	|- ( ( { <. x , y >. | ps } i^i ( B X. B ) ) Or B -> ( a e. B -> -. a ( { <. x , y >. | ps } i^i ( B X. B ) ) a ) )
59	32 56 58	syl2im	|- ( ph -> ( a ( { <. x , y >. | ps } i^i ( B X. B ) ) a -> -. a ( { <. x , y >. | ps } i^i ( B X. B ) ) a ) )
60	59	pm2.01d	|- ( ph -> -. a ( { <. x , y >. | ps } i^i ( B X. B ) ) a )
61		breq2	|- ( a = b -> ( a ( { <. x , y >. | ps } i^i ( B X. B ) ) a <-> a ( { <. x , y >. | ps } i^i ( B X. B ) ) b ) )
62		df-br	|- ( a ( { <. x , y >. | ps } i^i ( B X. B ) ) b <-> <. a , b >. e. ( { <. x , y >. | ps } i^i ( B X. B ) ) )
63	61 62	syl6bb	|- ( a = b -> ( a ( { <. x , y >. | ps } i^i ( B X. B ) ) a <-> <. a , b >. e. ( { <. x , y >. | ps } i^i ( B X. B ) ) ) )
64	63	notbid	|- ( a = b -> ( -. a ( { <. x , y >. | ps } i^i ( B X. B ) ) a <-> -. <. a , b >. e. ( { <. x , y >. | ps } i^i ( B X. B ) ) ) )
65	60 64	syl5ibcom	|- ( ph -> ( a = b -> -. <. a , b >. e. ( { <. x , y >. | ps } i^i ( B X. B ) ) ) )
66	51 65	syl5bi	|- ( ph -> ( <. a , b >. e. _I -> -. <. a , b >. e. ( { <. x , y >. | ps } i^i ( B X. B ) ) ) )
67	66	con2d	|- ( ph -> ( <. a , b >. e. ( { <. x , y >. | ps } i^i ( B X. B ) ) -> -. <. a , b >. e. _I ) )
68		opex	|- <. a , b >. e. _V
69		eldif	|- ( <. a , b >. e. ( _V \ _I ) <-> ( <. a , b >. e. _V /\ -. <. a , b >. e. _I ) )
70	68 69	mpbiran	|- ( <. a , b >. e. ( _V \ _I ) <-> -. <. a , b >. e. _I )
71	67 70	syl6ibr	|- ( ph -> ( <. a , b >. e. ( { <. x , y >. | ps } i^i ( B X. B ) ) -> <. a , b >. e. ( _V \ _I ) ) )
72	47 71	relssdv	|- ( ph -> ( { <. x , y >. | ps } i^i ( B X. B ) ) C_ ( _V \ _I ) )
73		disj2	|- ( ( ( { <. x , y >. | ps } i^i ( B X. B ) ) i^i _I ) = (/) <-> ( { <. x , y >. | ps } i^i ( B X. B ) ) C_ ( _V \ _I ) )
74	72 73	sylibr	|- ( ph -> ( ( { <. x , y >. | ps } i^i ( B X. B ) ) i^i _I ) = (/) )
75		disj3	|- ( ( ( { <. x , y >. | ps } i^i ( B X. B ) ) i^i _I ) = (/) <-> ( { <. x , y >. | ps } i^i ( B X. B ) ) = ( ( { <. x , y >. | ps } i^i ( B X. B ) ) \ _I ) )
76	74 75	sylib	|- ( ph -> ( { <. x , y >. | ps } i^i ( B X. B ) ) = ( ( { <. x , y >. | ps } i^i ( B X. B ) ) \ _I ) )
77	43 45 76	3eqtr4a	|- ( ph -> ( .<_ \ _I ) = ( { <. x , y >. | ps } i^i ( B X. B ) ) )
78	36 77	syl5eq	|- ( ph -> ( lt ` O ) = ( { <. x , y >. | ps } i^i ( B X. B ) ) )
79		soeq1	|- ( ( lt ` O ) = ( { <. x , y >. | ps } i^i ( B X. B ) ) -> ( ( lt ` O ) Or B <-> ( { <. x , y >. | ps } i^i ( B X. B ) ) Or B ) )
80	78 79	syl	|- ( ph -> ( ( lt ` O ) Or B <-> ( { <. x , y >. | ps } i^i ( B X. B ) ) Or B ) )
81	32 80	mpbird	|- ( ph -> ( lt ` O ) Or B )
82	6 1 4	opsrbas	|- ( ph -> ( Base ` S ) = ( Base ` O ) )
83	7 82	syl5eq	|- ( ph -> B = ( Base ` O ) )
84		soeq2	|- ( B = ( Base ` O ) -> ( ( lt ` O ) Or B <-> ( lt ` O ) Or ( Base ` O ) ) )
85	83 84	syl	|- ( ph -> ( ( lt ` O ) Or B <-> ( lt ` O ) Or ( Base ` O ) ) )
86	81 85	mpbid	|- ( ph -> ( lt ` O ) Or ( Base ` O ) )
87	83	reseq2d	|- ( ph -> ( _I |` B ) = ( _I |` ( Base ` O ) ) )
88		ssun2	|- ( _I |` B ) C_ ( ( { <. x , y >. | ps } i^i ( B X. B ) ) u. ( _I |` B ) )
89	87 88	eqsstrrdi	|- ( ph -> ( _I |` ( Base ` O ) ) C_ ( ( { <. x , y >. | ps } i^i ( B X. B ) ) u. ( _I |` B ) ) )
90	89 44	sseqtrrd	|- ( ph -> ( _I |` ( Base ` O ) ) C_ .<_ )
91		eqid	|- ( Base ` O ) = ( Base ` O )
92	91 12 34	tosso	|- ( O e. _V -> ( O e. Toset <-> ( ( lt ` O ) Or ( Base ` O ) /\ ( _I |` ( Base ` O ) ) C_ .<_ ) ) )
93	33 92	ax-mp	|- ( O e. Toset <-> ( ( lt ` O ) Or ( Base ` O ) /\ ( _I |` ( Base ` O ) ) C_ .<_ ) )
94	86 90 93	sylanbrc	|- ( ph -> O e. Toset )