Metamath Proof Explorer

Theorem opsrtoslem1

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 opsrtoslem1 
|- ( ph -> .<_ = ( ( { <. x , y >. | ps } i^i ( B X. B ) ) u. ( _I |` B ) ) )

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 6 1 7 8 9 10 12 4 opsrle 
 |-  ( ph -> .<_ = { <. x , y >. | ( { x , y } C_ B /\ ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w C z -> ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } )
14 unopab 
 |-  ( { <. x , y >. | ( { x , y } C_ B /\ ps ) } u. { <. x , y >. | ( { x , y } C_ B /\ x = y ) } ) = { <. x , y >. | ( ( { x , y } C_ B /\ ps ) \/ ( { x , y } C_ B /\ x = y ) ) }
15 inopab 
 |-  ( { <. x , y >. | ps } i^i { <. x , y >. | ( x e. B /\ y e. B ) } ) = { <. x , y >. | ( ps /\ ( x e. B /\ y e. B ) ) }
16 df-xp 
 |-  ( B X. B ) = { <. x , y >. | ( x e. B /\ y e. B ) }
17 16 ineq2i 
 |-  ( { <. x , y >. | ps } i^i ( B X. B ) ) = ( { <. x , y >. | ps } i^i { <. x , y >. | ( x e. B /\ y e. B ) } )
18 vex 
 |-  x e. _V
19 vex 
 |-  y e. _V
20 18 19 prss 
 |-  ( ( x e. B /\ y e. B ) <-> { x , y } C_ B )
21 20 anbi1i 
 |-  ( ( ( x e. B /\ y e. B ) /\ ps ) <-> ( { x , y } C_ B /\ ps ) )
22 ancom 
 |-  ( ( ( x e. B /\ y e. B ) /\ ps ) <-> ( ps /\ ( x e. B /\ y e. B ) ) )
23 21 22 bitr3i 
 |-  ( ( { x , y } C_ B /\ ps ) <-> ( ps /\ ( x e. B /\ y e. B ) ) )
24 23 opabbii 
 |-  { <. x , y >. | ( { x , y } C_ B /\ ps ) } = { <. x , y >. | ( ps /\ ( x e. B /\ y e. B ) ) }
25 15 17 24 3eqtr4i 
 |-  ( { <. x , y >. | ps } i^i ( B X. B ) ) = { <. x , y >. | ( { x , y } C_ B /\ ps ) }
26 opabresid 
 |-  ( _I |` B ) = { <. x , y >. | ( x e. B /\ y = x ) }
27 equcom 
 |-  ( x = y <-> y = x )
28 27 anbi2i 
 |-  ( ( x e. B /\ x = y ) <-> ( x e. B /\ y = x ) )
29 eleq1w 
 |-  ( x = y -> ( x e. B <-> y e. B ) )
30 29 biimpac 
 |-  ( ( x e. B /\ x = y ) -> y e. B )
31 30 pm4.71i 
 |-  ( ( x e. B /\ x = y ) <-> ( ( x e. B /\ x = y ) /\ y e. B ) )
32 28 31 bitr3i 
 |-  ( ( x e. B /\ y = x ) <-> ( ( x e. B /\ x = y ) /\ y e. B ) )
33 an32 
 |-  ( ( ( x e. B /\ x = y ) /\ y e. B ) <-> ( ( x e. B /\ y e. B ) /\ x = y ) )
34 20 anbi1i 
 |-  ( ( ( x e. B /\ y e. B ) /\ x = y ) <-> ( { x , y } C_ B /\ x = y ) )
35 32 33 34 3bitri 
 |-  ( ( x e. B /\ y = x ) <-> ( { x , y } C_ B /\ x = y ) )
36 35 opabbii 
 |-  { <. x , y >. | ( x e. B /\ y = x ) } = { <. x , y >. | ( { x , y } C_ B /\ x = y ) }
37 26 36 eqtri 
 |-  ( _I |` B ) = { <. x , y >. | ( { x , y } C_ B /\ x = y ) }
38 25 37 uneq12i 
 |-  ( ( { <. x , y >. | ps } i^i ( B X. B ) ) u. ( _I |` B ) ) = ( { <. x , y >. | ( { x , y } C_ B /\ ps ) } u. { <. x , y >. | ( { x , y } C_ B /\ x = y ) } )
39 11 orbi1i 
 |-  ( ( ps \/ x = y ) <-> ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w C z -> ( x ` w ) = ( y ` w ) ) ) \/ x = y ) )
40 39 anbi2i 
 |-  ( ( { x , y } C_ B /\ ( ps \/ x = y ) ) <-> ( { x , y } C_ B /\ ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w C z -> ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) )
41 andi 
 |-  ( ( { x , y } C_ B /\ ( ps \/ x = y ) ) <-> ( ( { x , y } C_ B /\ ps ) \/ ( { x , y } C_ B /\ x = y ) ) )
42 40 41 bitr3i 
 |-  ( ( { x , y } C_ B /\ ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w C z -> ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) <-> ( ( { x , y } C_ B /\ ps ) \/ ( { x , y } C_ B /\ x = y ) ) )
43 42 opabbii 
 |-  { <. x , y >. | ( { x , y } C_ B /\ ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w C z -> ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } = { <. x , y >. | ( ( { x , y } C_ B /\ ps ) \/ ( { x , y } C_ B /\ x = y ) ) }
44 14 38 43 3eqtr4ri 
 |-  { <. x , y >. | ( { x , y } C_ B /\ ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w C z -> ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } = ( ( { <. x , y >. | ps } i^i ( B X. B ) ) u. ( _I |` B ) )
45 13 44 syl6eq 
 |-  ( ph -> .<_ = ( ( { <. x , y >. | ps } i^i ( B X. B ) ) u. ( _I |` B ) ) )