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