Metamath Proof Explorer

Theorem prproropf1o

Description: There is a bijection between the set of proper pairs and the set of ordered ordered pairs, i.e., ordered pairs in which the first component is less than the second component. (Contributed by AV, 15-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 prproropf1o 
|- ( R Or V -> F : P -1-1-onto-> 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 prproropf1o.f 
 |-  F = ( p e. P |-> <. inf ( p , V , R ) , sup ( p , V , R ) >. )
4 1 2 prproropf1olem2 
 |-  ( ( R Or V /\ w e. P ) -> <. inf ( w , V , R ) , sup ( w , V , R ) >. e. O )
5 infeq1 
 |-  ( p = w -> inf ( p , V , R ) = inf ( w , V , R ) )
6 supeq1 
 |-  ( p = w -> sup ( p , V , R ) = sup ( w , V , R ) )
7 5 6 opeq12d 
 |-  ( p = w -> <. inf ( p , V , R ) , sup ( p , V , R ) >. = <. inf ( w , V , R ) , sup ( w , V , R ) >. )
8 7 cbvmptv 
 |-  ( p e. P |-> <. inf ( p , V , R ) , sup ( p , V , R ) >. ) = ( w e. P |-> <. inf ( w , V , R ) , sup ( w , V , R ) >. )
9 3 8 eqtri 
 |-  F = ( w e. P |-> <. inf ( w , V , R ) , sup ( w , V , R ) >. )
10 4 9 fmptd 
 |-  ( R Or V -> F : P --> O )
11 3ancomb 
 |-  ( ( R Or V /\ w e. P /\ z e. P ) <-> ( R Or V /\ z e. P /\ w e. P ) )
12 3anass 
 |-  ( ( R Or V /\ z e. P /\ w e. P ) <-> ( R Or V /\ ( z e. P /\ w e. P ) ) )
13 11 12 bitri 
 |-  ( ( R Or V /\ w e. P /\ z e. P ) <-> ( R Or V /\ ( z e. P /\ w e. P ) ) )
14 1 2 3 prproropf1olem4 
 |-  ( ( R Or V /\ w e. P /\ z e. P ) -> ( ( F ` z ) = ( F ` w ) -> z = w ) )
15 13 14 sylbir 
 |-  ( ( R Or V /\ ( z e. P /\ w e. P ) ) -> ( ( F ` z ) = ( F ` w ) -> z = w ) )
16 15 ralrimivva 
 |-  ( R Or V -> A. z e. P A. w e. P ( ( F ` z ) = ( F ` w ) -> z = w ) )
17 dff13 
 |-  ( F : P -1-1-> O <-> ( F : P --> O /\ A. z e. P A. w e. P ( ( F ` z ) = ( F ` w ) -> z = w ) ) )
18 10 16 17 sylanbrc 
 |-  ( R Or V -> F : P -1-1-> O )
19 1 2 prproropf1olem1 
 |-  ( ( R Or V /\ w e. O ) -> { ( 1st ` w ) , ( 2nd ` w ) } e. P )
20 fveq2 
 |-  ( z = { ( 1st ` w ) , ( 2nd ` w ) } -> ( F ` z ) = ( F ` { ( 1st ` w ) , ( 2nd ` w ) } ) )
21 20 eqeq2d 
 |-  ( z = { ( 1st ` w ) , ( 2nd ` w ) } -> ( w = ( F ` z ) <-> w = ( F ` { ( 1st ` w ) , ( 2nd ` w ) } ) ) )
22 21 adantl 
 |-  ( ( ( R Or V /\ w e. O ) /\ z = { ( 1st ` w ) , ( 2nd ` w ) } ) -> ( w = ( F ` z ) <-> w = ( F ` { ( 1st ` w ) , ( 2nd ` w ) } ) ) )
23 1 2 3 prproropf1olem3 
 |-  ( ( R Or V /\ w e. O ) -> ( F ` { ( 1st ` w ) , ( 2nd ` w ) } ) = <. ( 1st ` w ) , ( 2nd ` w ) >. )
24 1 prproropf1olem0 
 |-  ( w e. O <-> ( w = <. ( 1st ` w ) , ( 2nd ` w ) >. /\ ( ( 1st ` w ) e. V /\ ( 2nd ` w ) e. V ) /\ ( 1st ` w ) R ( 2nd ` w ) ) )
25 24 simp1bi 
 |-  ( w e. O -> w = <. ( 1st ` w ) , ( 2nd ` w ) >. )
26 25 eqcomd 
 |-  ( w e. O -> <. ( 1st ` w ) , ( 2nd ` w ) >. = w )
27 26 adantl 
 |-  ( ( R Or V /\ w e. O ) -> <. ( 1st ` w ) , ( 2nd ` w ) >. = w )
28 23 27 eqtr2d 
 |-  ( ( R Or V /\ w e. O ) -> w = ( F ` { ( 1st ` w ) , ( 2nd ` w ) } ) )
29 19 22 28 rspcedvd 
 |-  ( ( R Or V /\ w e. O ) -> E. z e. P w = ( F ` z ) )
30 29 ralrimiva 
 |-  ( R Or V -> A. w e. O E. z e. P w = ( F ` z ) )
31 dffo3 
 |-  ( F : P -onto-> O <-> ( F : P --> O /\ A. w e. O E. z e. P w = ( F ` z ) ) )
32 10 30 31 sylanbrc 
 |-  ( R Or V -> F : P -onto-> O )
33 df-f1o 
 |-  ( F : P -1-1-onto-> O <-> ( F : P -1-1-> O /\ F : P -onto-> O ) )
34 18 32 33 sylanbrc 
 |-  ( R Or V -> F : P -1-1-onto-> O )