This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 biimtrid 
 |-  ( 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 imbitrrdi 
 |-  ( 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 6 1 4 opsrbas 
 |-  ( ph -> ( Base ` S ) = ( Base ` O ) )
78 7 77 eqtr2id 
 |-  ( ph -> ( Base ` O ) = B )
79 76 78 soeq12d 
 |-  ( ph -> ( ( lt ` O ) Or ( Base ` O ) <-> ( { <. x , y >. | ps } i^i ( B X. B ) ) Or B ) )
80 30 79 mpbird 
 |-  ( ph -> ( lt ` O ) Or ( Base ` O ) )
81 78 reseq2d 
 |-  ( ph -> ( _I |` ( Base ` O ) ) = ( _I |` B ) )
82 ssun2 
 |-  ( _I |` B ) C_ ( ( { <. x , y >. | ps } i^i ( B X. B ) ) u. ( _I |` B ) )
83 81 82 eqsstrdi 
 |-  ( ph -> ( _I |` ( Base ` O ) ) C_ ( ( { <. x , y >. | ps } i^i ( B X. B ) ) u. ( _I |` B ) ) )
84 83 42 sseqtrrd 
 |-  ( ph -> ( _I |` ( Base ` O ) ) C_ .<_ )
85 eqid 
 |-  ( Base ` O ) = ( Base ` O )
86 85 12 32 tosso 
 |-  ( O e. _V -> ( O e. Toset <-> ( ( lt ` O ) Or ( Base ` O ) /\ ( _I |` ( Base ` O ) ) C_ .<_ ) ) )
87 31 86 ax-mp 
 |-  ( O e. Toset <-> ( ( lt ` O ) Or ( Base ` O ) /\ ( _I |` ( Base ` O ) ) C_ .<_ ) )
88 80 84 87 sylanbrc 
 |-  ( ph -> O e. Toset )