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