Metamath Proof Explorer

Theorem prproropf1olem3

Description: Lemma 3 for prproropf1o . (Contributed by AV, 13-Mar-2023)

Ref Expression
Hypotheses prproropf1o.o 
|- O = ( R i^i ( V X. V ) )
prproropf1o.p 
|- P = { p e. ~P V | ( # ` p ) = 2 }
prproropf1o.f 
|- F = ( p e. P |-> <. inf ( p , V , R ) , sup ( p , V , R ) >. )
Assertion prproropf1olem3 
|- ( ( R Or V /\ W e. O ) -> ( F ` { ( 1st ` W ) , ( 2nd ` W ) } ) = <. ( 1st ` W ) , ( 2nd ` W ) >. )

Proof

Step Hyp Ref Expression
1 prproropf1o.o 
 |-  O = ( R i^i ( V X. V ) )
2 prproropf1o.p 
 |-  P = { p e. ~P V | ( # ` p ) = 2 }
3 prproropf1o.f 
 |-  F = ( p e. P |-> <. inf ( p , V , R ) , sup ( p , V , R ) >. )
4 infeq1 
 |-  ( p = { ( 1st ` W ) , ( 2nd ` W ) } -> inf ( p , V , R ) = inf ( { ( 1st ` W ) , ( 2nd ` W ) } , V , R ) )
5 supeq1 
 |-  ( p = { ( 1st ` W ) , ( 2nd ` W ) } -> sup ( p , V , R ) = sup ( { ( 1st ` W ) , ( 2nd ` W ) } , V , R ) )
6 4 5 opeq12d 
 |-  ( p = { ( 1st ` W ) , ( 2nd ` W ) } -> <. inf ( p , V , R ) , sup ( p , V , R ) >. = <. inf ( { ( 1st ` W ) , ( 2nd ` W ) } , V , R ) , sup ( { ( 1st ` W ) , ( 2nd ` W ) } , V , R ) >. )
7 1 prproropf1olem0 
 |-  ( W e. O <-> ( W = <. ( 1st ` W ) , ( 2nd ` W ) >. /\ ( ( 1st ` W ) e. V /\ ( 2nd ` W ) e. V ) /\ ( 1st ` W ) R ( 2nd ` W ) ) )
8 simpl 
 |-  ( ( R Or V /\ ( ( ( 1st ` W ) e. V /\ ( 2nd ` W ) e. V ) /\ ( 1st ` W ) R ( 2nd ` W ) ) ) -> R Or V )
9 simprll 
 |-  ( ( R Or V /\ ( ( ( 1st ` W ) e. V /\ ( 2nd ` W ) e. V ) /\ ( 1st ` W ) R ( 2nd ` W ) ) ) -> ( 1st ` W ) e. V )
10 simprlr 
 |-  ( ( R Or V /\ ( ( ( 1st ` W ) e. V /\ ( 2nd ` W ) e. V ) /\ ( 1st ` W ) R ( 2nd ` W ) ) ) -> ( 2nd ` W ) e. V )
11 infpr 
 |-  ( ( R Or V /\ ( 1st ` W ) e. V /\ ( 2nd ` W ) e. V ) -> inf ( { ( 1st ` W ) , ( 2nd ` W ) } , V , R ) = if ( ( 1st ` W ) R ( 2nd ` W ) , ( 1st ` W ) , ( 2nd ` W ) ) )
12 8 9 10 11 syl3anc 
 |-  ( ( R Or V /\ ( ( ( 1st ` W ) e. V /\ ( 2nd ` W ) e. V ) /\ ( 1st ` W ) R ( 2nd ` W ) ) ) -> inf ( { ( 1st ` W ) , ( 2nd ` W ) } , V , R ) = if ( ( 1st ` W ) R ( 2nd ` W ) , ( 1st ` W ) , ( 2nd ` W ) ) )
13 iftrue 
 |-  ( ( 1st ` W ) R ( 2nd ` W ) -> if ( ( 1st ` W ) R ( 2nd ` W ) , ( 1st ` W ) , ( 2nd ` W ) ) = ( 1st ` W ) )
14 13 ad2antll 
 |-  ( ( R Or V /\ ( ( ( 1st ` W ) e. V /\ ( 2nd ` W ) e. V ) /\ ( 1st ` W ) R ( 2nd ` W ) ) ) -> if ( ( 1st ` W ) R ( 2nd ` W ) , ( 1st ` W ) , ( 2nd ` W ) ) = ( 1st ` W ) )
15 12 14 eqtrd 
 |-  ( ( R Or V /\ ( ( ( 1st ` W ) e. V /\ ( 2nd ` W ) e. V ) /\ ( 1st ` W ) R ( 2nd ` W ) ) ) -> inf ( { ( 1st ` W ) , ( 2nd ` W ) } , V , R ) = ( 1st ` W ) )
16 suppr 
 |-  ( ( R Or V /\ ( 1st ` W ) e. V /\ ( 2nd ` W ) e. V ) -> sup ( { ( 1st ` W ) , ( 2nd ` W ) } , V , R ) = if ( ( 2nd ` W ) R ( 1st ` W ) , ( 1st ` W ) , ( 2nd ` W ) ) )
17 8 9 10 16 syl3anc 
 |-  ( ( R Or V /\ ( ( ( 1st ` W ) e. V /\ ( 2nd ` W ) e. V ) /\ ( 1st ` W ) R ( 2nd ` W ) ) ) -> sup ( { ( 1st ` W ) , ( 2nd ` W ) } , V , R ) = if ( ( 2nd ` W ) R ( 1st ` W ) , ( 1st ` W ) , ( 2nd ` W ) ) )
18 soasym 
 |-  ( ( R Or V /\ ( ( 1st ` W ) e. V /\ ( 2nd ` W ) e. V ) ) -> ( ( 1st ` W ) R ( 2nd ` W ) -> -. ( 2nd ` W ) R ( 1st ` W ) ) )
19 18 impr 
 |-  ( ( R Or V /\ ( ( ( 1st ` W ) e. V /\ ( 2nd ` W ) e. V ) /\ ( 1st ` W ) R ( 2nd ` W ) ) ) -> -. ( 2nd ` W ) R ( 1st ` W ) )
20 19 iffalsed 
 |-  ( ( R Or V /\ ( ( ( 1st ` W ) e. V /\ ( 2nd ` W ) e. V ) /\ ( 1st ` W ) R ( 2nd ` W ) ) ) -> if ( ( 2nd ` W ) R ( 1st ` W ) , ( 1st ` W ) , ( 2nd ` W ) ) = ( 2nd ` W ) )
21 17 20 eqtrd 
 |-  ( ( R Or V /\ ( ( ( 1st ` W ) e. V /\ ( 2nd ` W ) e. V ) /\ ( 1st ` W ) R ( 2nd ` W ) ) ) -> sup ( { ( 1st ` W ) , ( 2nd ` W ) } , V , R ) = ( 2nd ` W ) )
22 15 21 opeq12d 
 |-  ( ( R Or V /\ ( ( ( 1st ` W ) e. V /\ ( 2nd ` W ) e. V ) /\ ( 1st ` W ) R ( 2nd ` W ) ) ) -> <. inf ( { ( 1st ` W ) , ( 2nd ` W ) } , V , R ) , sup ( { ( 1st ` W ) , ( 2nd ` W ) } , V , R ) >. = <. ( 1st ` W ) , ( 2nd ` W ) >. )
23 22 3adantr1 
 |-  ( ( R Or V /\ ( W = <. ( 1st ` W ) , ( 2nd ` W ) >. /\ ( ( 1st ` W ) e. V /\ ( 2nd ` W ) e. V ) /\ ( 1st ` W ) R ( 2nd ` W ) ) ) -> <. inf ( { ( 1st ` W ) , ( 2nd ` W ) } , V , R ) , sup ( { ( 1st ` W ) , ( 2nd ` W ) } , V , R ) >. = <. ( 1st ` W ) , ( 2nd ` W ) >. )
24 7 23 sylan2b 
 |-  ( ( R Or V /\ W e. O ) -> <. inf ( { ( 1st ` W ) , ( 2nd ` W ) } , V , R ) , sup ( { ( 1st ` W ) , ( 2nd ` W ) } , V , R ) >. = <. ( 1st ` W ) , ( 2nd ` W ) >. )
25 6 24 sylan9eqr 
 |-  ( ( ( R Or V /\ W e. O ) /\ p = { ( 1st ` W ) , ( 2nd ` W ) } ) -> <. inf ( p , V , R ) , sup ( p , V , R ) >. = <. ( 1st ` W ) , ( 2nd ` W ) >. )
26 1 2 prproropf1olem1 
 |-  ( ( R Or V /\ W e. O ) -> { ( 1st ` W ) , ( 2nd ` W ) } e. P )
27 opex 
 |-  <. ( 1st ` W ) , ( 2nd ` W ) >. e. _V
28 27 a1i 
 |-  ( ( R Or V /\ W e. O ) -> <. ( 1st ` W ) , ( 2nd ` W ) >. e. _V )
29 3 25 26 28 fvmptd2 
 |-  ( ( R Or V /\ W e. O ) -> ( F ` { ( 1st ` W ) , ( 2nd ` W ) } ) = <. ( 1st ` W ) , ( 2nd ` W ) >. )