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 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 syl5eq
 |-  ( 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 syl5eq
 |-  ( 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 )