Metamath Proof Explorer

Theorem prproropf1olem0

Description: Lemma 0 for prproropf1o . Remark: O , the set of ordered ordered pairs, i.e., ordered pairs in which the first component is less than the second component, can alternatively be written as O = { x e. ( V X. V ) | ( 1stx ) R ( 2ndx ) } or even as O = { x e. ( V X. V ) | <. ( 1stx ) , ( 2ndx ) >. e. R } , by which the relationship between ordered and unordered pair is immediately visible. (Contributed by AV, 18-Mar-2023)

Ref Expression
Hypothesis prproropf1o.o 
|- O = ( R i^i ( V X. V ) )
Assertion prproropf1olem0 
|- ( W e. O <-> ( W = <. ( 1st ` W ) , ( 2nd ` W ) >. /\ ( ( 1st ` W ) e. V /\ ( 2nd ` W ) e. V ) /\ ( 1st ` W ) R ( 2nd ` W ) ) )

Proof

Step Hyp Ref Expression
1 prproropf1o.o 
 |-  O = ( R i^i ( V X. V ) )
2 1 eleq2i 
 |-  ( W e. O <-> W e. ( R i^i ( V X. V ) ) )
3 elin 
 |-  ( W e. ( R i^i ( V X. V ) ) <-> ( W e. R /\ W e. ( V X. V ) ) )
4 ancom 
 |-  ( ( W e. R /\ ( W = <. ( 1st ` W ) , ( 2nd ` W ) >. /\ ( ( 1st ` W ) e. V /\ ( 2nd ` W ) e. V ) ) ) <-> ( ( W = <. ( 1st ` W ) , ( 2nd ` W ) >. /\ ( ( 1st ` W ) e. V /\ ( 2nd ` W ) e. V ) ) /\ W e. R ) )
5 eleq1 
 |-  ( W = <. ( 1st ` W ) , ( 2nd ` W ) >. -> ( W e. R <-> <. ( 1st ` W ) , ( 2nd ` W ) >. e. R ) )
6 df-br 
 |-  ( ( 1st ` W ) R ( 2nd ` W ) <-> <. ( 1st ` W ) , ( 2nd ` W ) >. e. R )
7 5 6 bitr4di 
 |-  ( W = <. ( 1st ` W ) , ( 2nd ` W ) >. -> ( W e. R <-> ( 1st ` W ) R ( 2nd ` W ) ) )
8 7 adantr 
 |-  ( ( W = <. ( 1st ` W ) , ( 2nd ` W ) >. /\ ( ( 1st ` W ) e. V /\ ( 2nd ` W ) e. V ) ) -> ( W e. R <-> ( 1st ` W ) R ( 2nd ` W ) ) )
9 8 pm5.32i 
 |-  ( ( ( W = <. ( 1st ` W ) , ( 2nd ` W ) >. /\ ( ( 1st ` W ) e. V /\ ( 2nd ` W ) e. V ) ) /\ W e. R ) <-> ( ( W = <. ( 1st ` W ) , ( 2nd ` W ) >. /\ ( ( 1st ` W ) e. V /\ ( 2nd ` W ) e. V ) ) /\ ( 1st ` W ) R ( 2nd ` W ) ) )
10 4 9 bitri 
 |-  ( ( W e. R /\ ( W = <. ( 1st ` W ) , ( 2nd ` W ) >. /\ ( ( 1st ` W ) e. V /\ ( 2nd ` W ) e. V ) ) ) <-> ( ( W = <. ( 1st ` W ) , ( 2nd ` W ) >. /\ ( ( 1st ` W ) e. V /\ ( 2nd ` W ) e. V ) ) /\ ( 1st ` W ) R ( 2nd ` W ) ) )
11 elxp6 
 |-  ( W e. ( V X. V ) <-> ( W = <. ( 1st ` W ) , ( 2nd ` W ) >. /\ ( ( 1st ` W ) e. V /\ ( 2nd ` W ) e. V ) ) )
12 11 anbi2i 
 |-  ( ( W e. R /\ W e. ( V X. V ) ) <-> ( W e. R /\ ( W = <. ( 1st ` W ) , ( 2nd ` W ) >. /\ ( ( 1st ` W ) e. V /\ ( 2nd ` W ) e. V ) ) ) )
13 df-3an 
 |-  ( ( W = <. ( 1st ` W ) , ( 2nd ` W ) >. /\ ( ( 1st ` W ) e. V /\ ( 2nd ` W ) e. V ) /\ ( 1st ` W ) R ( 2nd ` W ) ) <-> ( ( W = <. ( 1st ` W ) , ( 2nd ` W ) >. /\ ( ( 1st ` W ) e. V /\ ( 2nd ` W ) e. V ) ) /\ ( 1st ` W ) R ( 2nd ` W ) ) )
14 10 12 13 3bitr4i 
 |-  ( ( W e. R /\ W e. ( V X. V ) ) <-> ( W = <. ( 1st ` W ) , ( 2nd ` W ) >. /\ ( ( 1st ` W ) e. V /\ ( 2nd ` W ) e. V ) /\ ( 1st ` W ) R ( 2nd ` W ) ) )
15 2 3 14 3bitri 
 |-  ( W e. O <-> ( W = <. ( 1st ` W ) , ( 2nd ` W ) >. /\ ( ( 1st ` W ) e. V /\ ( 2nd ` W ) e. V ) /\ ( 1st ` W ) R ( 2nd ` W ) ) )