Metamath Proof Explorer

Theorem prproropf1olem2

Description: Lemma 2 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 }
Assertion prproropf1olem2 
|- ( ( R Or V /\ X e. P ) -> <. inf ( X , V , R ) , sup ( X , V , R ) >. e. O )

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 2 prpair 
 |-  ( X e. P <-> E. a e. V E. b e. V ( X = { a , b } /\ a =/= b ) )
4 simpll 
 |-  ( ( ( R Or V /\ ( a e. V /\ b e. V ) ) /\ ( X = { a , b } /\ a =/= b ) ) -> R Or V )
5 simplrl 
 |-  ( ( ( R Or V /\ ( a e. V /\ b e. V ) ) /\ ( X = { a , b } /\ a =/= b ) ) -> a e. V )
6 simplrr 
 |-  ( ( ( R Or V /\ ( a e. V /\ b e. V ) ) /\ ( X = { a , b } /\ a =/= b ) ) -> b e. V )
7 simprr 
 |-  ( ( ( R Or V /\ ( a e. V /\ b e. V ) ) /\ ( X = { a , b } /\ a =/= b ) ) -> a =/= b )
8 infsupprpr 
 |-  ( ( R Or V /\ ( a e. V /\ b e. V /\ a =/= b ) ) -> inf ( { a , b } , V , R ) R sup ( { a , b } , V , R ) )
9 4 5 6 7 8 syl13anc 
 |-  ( ( ( R Or V /\ ( a e. V /\ b e. V ) ) /\ ( X = { a , b } /\ a =/= b ) ) -> inf ( { a , b } , V , R ) R sup ( { a , b } , V , R ) )
10 df-br 
 |-  ( inf ( { a , b } , V , R ) R sup ( { a , b } , V , R ) <-> <. inf ( { a , b } , V , R ) , sup ( { a , b } , V , R ) >. e. R )
11 9 10 sylib 
 |-  ( ( ( R Or V /\ ( a e. V /\ b e. V ) ) /\ ( X = { a , b } /\ a =/= b ) ) -> <. inf ( { a , b } , V , R ) , sup ( { a , b } , V , R ) >. e. R )
12 infpr 
 |-  ( ( R Or V /\ a e. V /\ b e. V ) -> inf ( { a , b } , V , R ) = if ( a R b , a , b ) )
13 ifcl 
 |-  ( ( a e. V /\ b e. V ) -> if ( a R b , a , b ) e. V )
14 13 3adant1 
 |-  ( ( R Or V /\ a e. V /\ b e. V ) -> if ( a R b , a , b ) e. V )
15 12 14 eqeltrd 
 |-  ( ( R Or V /\ a e. V /\ b e. V ) -> inf ( { a , b } , V , R ) e. V )
16 suppr 
 |-  ( ( R Or V /\ a e. V /\ b e. V ) -> sup ( { a , b } , V , R ) = if ( b R a , a , b ) )
17 ifcl 
 |-  ( ( a e. V /\ b e. V ) -> if ( b R a , a , b ) e. V )
18 17 3adant1 
 |-  ( ( R Or V /\ a e. V /\ b e. V ) -> if ( b R a , a , b ) e. V )
19 16 18 eqeltrd 
 |-  ( ( R Or V /\ a e. V /\ b e. V ) -> sup ( { a , b } , V , R ) e. V )
20 15 19 jca 
 |-  ( ( R Or V /\ a e. V /\ b e. V ) -> ( inf ( { a , b } , V , R ) e. V /\ sup ( { a , b } , V , R ) e. V ) )
21 20 3expb 
 |-  ( ( R Or V /\ ( a e. V /\ b e. V ) ) -> ( inf ( { a , b } , V , R ) e. V /\ sup ( { a , b } , V , R ) e. V ) )
22 21 adantr 
 |-  ( ( ( R Or V /\ ( a e. V /\ b e. V ) ) /\ ( X = { a , b } /\ a =/= b ) ) -> ( inf ( { a , b } , V , R ) e. V /\ sup ( { a , b } , V , R ) e. V ) )
23 opelxp 
 |-  ( <. inf ( { a , b } , V , R ) , sup ( { a , b } , V , R ) >. e. ( V X. V ) <-> ( inf ( { a , b } , V , R ) e. V /\ sup ( { a , b } , V , R ) e. V ) )
24 22 23 sylibr 
 |-  ( ( ( R Or V /\ ( a e. V /\ b e. V ) ) /\ ( X = { a , b } /\ a =/= b ) ) -> <. inf ( { a , b } , V , R ) , sup ( { a , b } , V , R ) >. e. ( V X. V ) )
25 11 24 elind 
 |-  ( ( ( R Or V /\ ( a e. V /\ b e. V ) ) /\ ( X = { a , b } /\ a =/= b ) ) -> <. inf ( { a , b } , V , R ) , sup ( { a , b } , V , R ) >. e. ( R i^i ( V X. V ) ) )
26 infeq1 
 |-  ( X = { a , b } -> inf ( X , V , R ) = inf ( { a , b } , V , R ) )
27 supeq1 
 |-  ( X = { a , b } -> sup ( X , V , R ) = sup ( { a , b } , V , R ) )
28 26 27 opeq12d 
 |-  ( X = { a , b } -> <. inf ( X , V , R ) , sup ( X , V , R ) >. = <. inf ( { a , b } , V , R ) , sup ( { a , b } , V , R ) >. )
29 28 eleq1d 
 |-  ( X = { a , b } -> ( <. inf ( X , V , R ) , sup ( X , V , R ) >. e. ( R i^i ( V X. V ) ) <-> <. inf ( { a , b } , V , R ) , sup ( { a , b } , V , R ) >. e. ( R i^i ( V X. V ) ) ) )
30 29 ad2antrl 
 |-  ( ( ( R Or V /\ ( a e. V /\ b e. V ) ) /\ ( X = { a , b } /\ a =/= b ) ) -> ( <. inf ( X , V , R ) , sup ( X , V , R ) >. e. ( R i^i ( V X. V ) ) <-> <. inf ( { a , b } , V , R ) , sup ( { a , b } , V , R ) >. e. ( R i^i ( V X. V ) ) ) )
31 25 30 mpbird 
 |-  ( ( ( R Or V /\ ( a e. V /\ b e. V ) ) /\ ( X = { a , b } /\ a =/= b ) ) -> <. inf ( X , V , R ) , sup ( X , V , R ) >. e. ( R i^i ( V X. V ) ) )
32 31 ex 
 |-  ( ( R Or V /\ ( a e. V /\ b e. V ) ) -> ( ( X = { a , b } /\ a =/= b ) -> <. inf ( X , V , R ) , sup ( X , V , R ) >. e. ( R i^i ( V X. V ) ) ) )
33 32 rexlimdvva 
 |-  ( R Or V -> ( E. a e. V E. b e. V ( X = { a , b } /\ a =/= b ) -> <. inf ( X , V , R ) , sup ( X , V , R ) >. e. ( R i^i ( V X. V ) ) ) )
34 3 33 syl5bi 
 |-  ( R Or V -> ( X e. P -> <. inf ( X , V , R ) , sup ( X , V , R ) >. e. ( R i^i ( V X. V ) ) ) )
35 34 imp 
 |-  ( ( R Or V /\ X e. P ) -> <. inf ( X , V , R ) , sup ( X , V , R ) >. e. ( R i^i ( V X. V ) ) )
36 35 1 eleqtrrdi 
 |-  ( ( R Or V /\ X e. P ) -> <. inf ( X , V , R ) , sup ( X , V , R ) >. e. O )