Metamath Proof Explorer

Theorem prproropf1olem1

Description: Lemma 1 for prproropf1o . (Contributed by AV, 12-Mar-2023)

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

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 1 prproropf1olem0 
 |-  ( W e. O <-> ( W = <. ( 1st ` W ) , ( 2nd ` W ) >. /\ ( ( 1st ` W ) e. V /\ ( 2nd ` W ) e. V ) /\ ( 1st ` W ) R ( 2nd ` W ) ) )
4 simpr2 
 |-  ( ( R Or V /\ ( W = <. ( 1st ` W ) , ( 2nd ` W ) >. /\ ( ( 1st ` W ) e. V /\ ( 2nd ` W ) e. V ) /\ ( 1st ` W ) R ( 2nd ` W ) ) ) -> ( ( 1st ` W ) e. V /\ ( 2nd ` W ) e. V ) )
5 prelpwi 
 |-  ( ( ( 1st ` W ) e. V /\ ( 2nd ` W ) e. V ) -> { ( 1st ` W ) , ( 2nd ` W ) } e. ~P V )
6 4 5 syl 
 |-  ( ( R Or V /\ ( W = <. ( 1st ` W ) , ( 2nd ` W ) >. /\ ( ( 1st ` W ) e. V /\ ( 2nd ` W ) e. V ) /\ ( 1st ` W ) R ( 2nd ` W ) ) ) -> { ( 1st ` W ) , ( 2nd ` W ) } e. ~P V )
7 sopo 
 |-  ( R Or V -> R Po V )
8 7 adantr 
 |-  ( ( R Or V /\ ( W = <. ( 1st ` W ) , ( 2nd ` W ) >. /\ ( ( 1st ` W ) e. V /\ ( 2nd ` W ) e. V ) /\ ( 1st ` W ) R ( 2nd ` W ) ) ) -> R Po V )
9 simpr3 
 |-  ( ( R Or V /\ ( W = <. ( 1st ` W ) , ( 2nd ` W ) >. /\ ( ( 1st ` W ) e. V /\ ( 2nd ` W ) e. V ) /\ ( 1st ` W ) R ( 2nd ` W ) ) ) -> ( 1st ` W ) R ( 2nd ` W ) )
10 po2ne 
 |-  ( ( R Po V /\ ( ( 1st ` W ) e. V /\ ( 2nd ` W ) e. V ) /\ ( 1st ` W ) R ( 2nd ` W ) ) -> ( 1st ` W ) =/= ( 2nd ` W ) )
11 8 4 9 10 syl3anc 
 |-  ( ( R Or V /\ ( W = <. ( 1st ` W ) , ( 2nd ` W ) >. /\ ( ( 1st ` W ) e. V /\ ( 2nd ` W ) e. V ) /\ ( 1st ` W ) R ( 2nd ` W ) ) ) -> ( 1st ` W ) =/= ( 2nd ` W ) )
12 fvex 
 |-  ( 1st ` W ) e. _V
13 fvex 
 |-  ( 2nd ` W ) e. _V
14 hashprg 
 |-  ( ( ( 1st ` W ) e. _V /\ ( 2nd ` W ) e. _V ) -> ( ( 1st ` W ) =/= ( 2nd ` W ) <-> ( # ` { ( 1st ` W ) , ( 2nd ` W ) } ) = 2 ) )
15 12 13 14 mp2an 
 |-  ( ( 1st ` W ) =/= ( 2nd ` W ) <-> ( # ` { ( 1st ` W ) , ( 2nd ` W ) } ) = 2 )
16 11 15 sylib 
 |-  ( ( R Or V /\ ( W = <. ( 1st ` W ) , ( 2nd ` W ) >. /\ ( ( 1st ` W ) e. V /\ ( 2nd ` W ) e. V ) /\ ( 1st ` W ) R ( 2nd ` W ) ) ) -> ( # ` { ( 1st ` W ) , ( 2nd ` W ) } ) = 2 )
17 6 16 jca 
 |-  ( ( R Or V /\ ( W = <. ( 1st ` W ) , ( 2nd ` W ) >. /\ ( ( 1st ` W ) e. V /\ ( 2nd ` W ) e. V ) /\ ( 1st ` W ) R ( 2nd ` W ) ) ) -> ( { ( 1st ` W ) , ( 2nd ` W ) } e. ~P V /\ ( # ` { ( 1st ` W ) , ( 2nd ` W ) } ) = 2 ) )
18 3 17 sylan2b 
 |-  ( ( R Or V /\ W e. O ) -> ( { ( 1st ` W ) , ( 2nd ` W ) } e. ~P V /\ ( # ` { ( 1st ` W ) , ( 2nd ` W ) } ) = 2 ) )
19 fveqeq2 
 |-  ( p = { ( 1st ` W ) , ( 2nd ` W ) } -> ( ( # ` p ) = 2 <-> ( # ` { ( 1st ` W ) , ( 2nd ` W ) } ) = 2 ) )
20 19 2 elrab2 
 |-  ( { ( 1st ` W ) , ( 2nd ` W ) } e. P <-> ( { ( 1st ` W ) , ( 2nd ` W ) } e. ~P V /\ ( # ` { ( 1st ` W ) , ( 2nd ` W ) } ) = 2 ) )
21 18 20 sylibr 
 |-  ( ( R Or V /\ W e. O ) -> { ( 1st ` W ) , ( 2nd ` W ) } e. P )