Metamath Proof Explorer

Theorem tposideq

Description: Two ways of expressing the swap function. (Contributed by Zhi Wang, 6-Oct-2025)

Ref Expression
Assertion tposideq 
|- ( Rel R -> ( tpos _I |` R ) = ( x e. R |-> U. `' { x } ) )

Proof

Step Hyp Ref Expression
1 tposres 
 |-  ( Rel R -> ( tpos _I |` R ) = tpos ( _I |` `' R ) )
2 relcnv 
 |-  Rel `' R
3 fnresi 
 |-  ( _I |` `' R ) Fn `' R
4 tposfn2 
 |-  ( Rel `' R -> ( ( _I |` `' R ) Fn `' R -> tpos ( _I |` `' R ) Fn `' `' R ) )
5 2 3 4 mp2 
 |-  tpos ( _I |` `' R ) Fn `' `' R
6 dfrel2 
 |-  ( Rel R <-> `' `' R = R )
7 6 biimpi 
 |-  ( Rel R -> `' `' R = R )
8 7 fneq2d 
 |-  ( Rel R -> ( tpos ( _I |` `' R ) Fn `' `' R <-> tpos ( _I |` `' R ) Fn R ) )
9 5 8 mpbii 
 |-  ( Rel R -> tpos ( _I |` `' R ) Fn R )
10 vsnex 
 |-  { x } e. _V
11 10 cnvex 
 |-  `' { x } e. _V
12 11 uniex 
 |-  U. `' { x } e. _V
13 eqid 
 |-  ( x e. R |-> U. `' { x } ) = ( x e. R |-> U. `' { x } )
14 12 13 fnmpti 
 |-  ( x e. R |-> U. `' { x } ) Fn R
15 14 a1i 
 |-  ( Rel R -> ( x e. R |-> U. `' { x } ) Fn R )
16 1st2nd 
 |-  ( ( Rel R /\ y e. R ) -> y = <. ( 1st ` y ) , ( 2nd ` y ) >. )
17 1st2ndb 
 |-  ( y e. ( _V X. _V ) <-> y = <. ( 1st ` y ) , ( 2nd ` y ) >. )
18 17 biimpri 
 |-  ( y = <. ( 1st ` y ) , ( 2nd ` y ) >. -> y e. ( _V X. _V ) )
19 2nd1st 
 |-  ( y e. ( _V X. _V ) -> U. `' { y } = <. ( 2nd ` y ) , ( 1st ` y ) >. )
20 16 18 19 3syl 
 |-  ( ( Rel R /\ y e. R ) -> U. `' { y } = <. ( 2nd ` y ) , ( 1st ` y ) >. )
21 sneq 
 |-  ( x = y -> { x } = { y } )
22 21 cnveqd 
 |-  ( x = y -> `' { x } = `' { y } )
23 22 unieqd 
 |-  ( x = y -> U. `' { x } = U. `' { y } )
24 23 13 12 fvmpt3i 
 |-  ( y e. R -> ( ( x e. R |-> U. `' { x } ) ` y ) = U. `' { y } )
25 24 adantl 
 |-  ( ( Rel R /\ y e. R ) -> ( ( x e. R |-> U. `' { x } ) ` y ) = U. `' { y } )
26 16 fveq2d 
 |-  ( ( Rel R /\ y e. R ) -> ( tpos ( _I |` `' R ) ` y ) = ( tpos ( _I |` `' R ) ` <. ( 1st ` y ) , ( 2nd ` y ) >. ) )
27 ovtpos 
 |-  ( ( 1st ` y ) tpos ( _I |` `' R ) ( 2nd ` y ) ) = ( ( 2nd ` y ) ( _I |` `' R ) ( 1st ` y ) )
28 df-ov 
 |-  ( ( 1st ` y ) tpos ( _I |` `' R ) ( 2nd ` y ) ) = ( tpos ( _I |` `' R ) ` <. ( 1st ` y ) , ( 2nd ` y ) >. )
29 df-ov 
 |-  ( ( 2nd ` y ) ( _I |` `' R ) ( 1st ` y ) ) = ( ( _I |` `' R ) ` <. ( 2nd ` y ) , ( 1st ` y ) >. )
30 27 28 29 3eqtr3i 
 |-  ( tpos ( _I |` `' R ) ` <. ( 1st ` y ) , ( 2nd ` y ) >. ) = ( ( _I |` `' R ) ` <. ( 2nd ` y ) , ( 1st ` y ) >. )
31 30 a1i 
 |-  ( ( Rel R /\ y e. R ) -> ( tpos ( _I |` `' R ) ` <. ( 1st ` y ) , ( 2nd ` y ) >. ) = ( ( _I |` `' R ) ` <. ( 2nd ` y ) , ( 1st ` y ) >. ) )
32 simpr 
 |-  ( ( Rel R /\ y e. R ) -> y e. R )
33 16 32 eqeltrrd 
 |-  ( ( Rel R /\ y e. R ) -> <. ( 1st ` y ) , ( 2nd ` y ) >. e. R )
34 fvex 
 |-  ( 2nd ` y ) e. _V
35 fvex 
 |-  ( 1st ` y ) e. _V
36 34 35 opelcnv 
 |-  ( <. ( 2nd ` y ) , ( 1st ` y ) >. e. `' R <-> <. ( 1st ` y ) , ( 2nd ` y ) >. e. R )
37 36 biimpri 
 |-  ( <. ( 1st ` y ) , ( 2nd ` y ) >. e. R -> <. ( 2nd ` y ) , ( 1st ` y ) >. e. `' R )
38 fvresi 
 |-  ( <. ( 2nd ` y ) , ( 1st ` y ) >. e. `' R -> ( ( _I |` `' R ) ` <. ( 2nd ` y ) , ( 1st ` y ) >. ) = <. ( 2nd ` y ) , ( 1st ` y ) >. )
39 33 37 38 3syl 
 |-  ( ( Rel R /\ y e. R ) -> ( ( _I |` `' R ) ` <. ( 2nd ` y ) , ( 1st ` y ) >. ) = <. ( 2nd ` y ) , ( 1st ` y ) >. )
40 26 31 39 3eqtrd 
 |-  ( ( Rel R /\ y e. R ) -> ( tpos ( _I |` `' R ) ` y ) = <. ( 2nd ` y ) , ( 1st ` y ) >. )
41 20 25 40 3eqtr4rd 
 |-  ( ( Rel R /\ y e. R ) -> ( tpos ( _I |` `' R ) ` y ) = ( ( x e. R |-> U. `' { x } ) ` y ) )
42 9 15 41 eqfnfvd 
 |-  ( Rel R -> tpos ( _I |` `' R ) = ( x e. R |-> U. `' { x } ) )
43 1 42 eqtrd 
 |-  ( Rel R -> ( tpos _I |` R ) = ( x e. R |-> U. `' { x } ) )