Metamath Proof Explorer

Theorem fsplit

Description: A function that can be used to feed a common value to both operands of an operation. Use as the second argument of a composition with the function of fpar in order to build compound functions such as ( x e. ( 0 [,) +oo ) |-> ( ( sqrtx ) + ( sinx ) ) ) . (Contributed by NM, 17-Sep-2007) Replace use of dfid2 with df-id . (Revised by BJ, 31-Dec-2023)

Ref Expression
Assertion fsplit 
|- `' ( 1st |` _I ) = ( x e. _V |-> <. x , x >. )

Proof

Step Hyp Ref Expression
1 vex 
 |-  x e. _V
2 vex 
 |-  y e. _V
3 1 2 brcnv 
 |-  ( x `' ( 1st |` _I ) y <-> y ( 1st |` _I ) x )
4 1 brresi 
 |-  ( y ( 1st |` _I ) x <-> ( y e. _I /\ y 1st x ) )
5 19.42v 
 |-  ( E. z ( ( 1st ` y ) = x /\ y = <. z , z >. ) <-> ( ( 1st ` y ) = x /\ E. z y = <. z , z >. ) )
6 vex 
 |-  z e. _V
7 6 6 op1std 
 |-  ( y = <. z , z >. -> ( 1st ` y ) = z )
8 7 eqeq1d 
 |-  ( y = <. z , z >. -> ( ( 1st ` y ) = x <-> z = x ) )
9 8 pm5.32ri 
 |-  ( ( ( 1st ` y ) = x /\ y = <. z , z >. ) <-> ( z = x /\ y = <. z , z >. ) )
10 9 exbii 
 |-  ( E. z ( ( 1st ` y ) = x /\ y = <. z , z >. ) <-> E. z ( z = x /\ y = <. z , z >. ) )
11 fo1st 
 |-  1st : _V -onto-> _V
12 fofn 
 |-  ( 1st : _V -onto-> _V -> 1st Fn _V )
13 11 12 ax-mp 
 |-  1st Fn _V
14 fnbrfvb 
 |-  ( ( 1st Fn _V /\ y e. _V ) -> ( ( 1st ` y ) = x <-> y 1st x ) )
15 13 2 14 mp2an 
 |-  ( ( 1st ` y ) = x <-> y 1st x )
16 df-id 
 |-  _I = { <. z , t >. | z = t }
17 16 eleq2i 
 |-  ( y e. _I <-> y e. { <. z , t >. | z = t } )
18 elopab 
 |-  ( y e. { <. z , t >. | z = t } <-> E. z E. t ( y = <. z , t >. /\ z = t ) )
19 ancom 
 |-  ( ( y = <. z , t >. /\ z = t ) <-> ( z = t /\ y = <. z , t >. ) )
20 equcom 
 |-  ( z = t <-> t = z )
21 20 anbi1i 
 |-  ( ( z = t /\ y = <. z , t >. ) <-> ( t = z /\ y = <. z , t >. ) )
22 opeq2 
 |-  ( t = z -> <. z , t >. = <. z , z >. )
23 22 eqeq2d 
 |-  ( t = z -> ( y = <. z , t >. <-> y = <. z , z >. ) )
24 23 pm5.32i 
 |-  ( ( t = z /\ y = <. z , t >. ) <-> ( t = z /\ y = <. z , z >. ) )
25 19 21 24 3bitri 
 |-  ( ( y = <. z , t >. /\ z = t ) <-> ( t = z /\ y = <. z , z >. ) )
26 25 exbii 
 |-  ( E. t ( y = <. z , t >. /\ z = t ) <-> E. t ( t = z /\ y = <. z , z >. ) )
27 biidd 
 |-  ( t = z -> ( y = <. z , z >. <-> y = <. z , z >. ) )
28 27 equsexvw 
 |-  ( E. t ( t = z /\ y = <. z , z >. ) <-> y = <. z , z >. )
29 26 28 bitri 
 |-  ( E. t ( y = <. z , t >. /\ z = t ) <-> y = <. z , z >. )
30 29 exbii 
 |-  ( E. z E. t ( y = <. z , t >. /\ z = t ) <-> E. z y = <. z , z >. )
31 17 18 30 3bitrri 
 |-  ( E. z y = <. z , z >. <-> y e. _I )
32 15 31 anbi12ci 
 |-  ( ( ( 1st ` y ) = x /\ E. z y = <. z , z >. ) <-> ( y e. _I /\ y 1st x ) )
33 5 10 32 3bitr3ri 
 |-  ( ( y e. _I /\ y 1st x ) <-> E. z ( z = x /\ y = <. z , z >. ) )
34 id 
 |-  ( z = x -> z = x )
35 34 34 opeq12d 
 |-  ( z = x -> <. z , z >. = <. x , x >. )
36 35 eqeq2d 
 |-  ( z = x -> ( y = <. z , z >. <-> y = <. x , x >. ) )
37 36 equsexvw 
 |-  ( E. z ( z = x /\ y = <. z , z >. ) <-> y = <. x , x >. )
38 33 37 bitri 
 |-  ( ( y e. _I /\ y 1st x ) <-> y = <. x , x >. )
39 3 4 38 3bitri 
 |-  ( x `' ( 1st |` _I ) y <-> y = <. x , x >. )
40 39 opabbii 
 |-  { <. x , y >. | x `' ( 1st |` _I ) y } = { <. x , y >. | y = <. x , x >. }
41 relcnv 
 |-  Rel `' ( 1st |` _I )
42 dfrel4v 
 |-  ( Rel `' ( 1st |` _I ) <-> `' ( 1st |` _I ) = { <. x , y >. | x `' ( 1st |` _I ) y } )
43 41 42 mpbi 
 |-  `' ( 1st |` _I ) = { <. x , y >. | x `' ( 1st |` _I ) y }
44 mptv 
 |-  ( x e. _V |-> <. x , x >. ) = { <. x , y >. | y = <. x , x >. }
45 40 43 44 3eqtr4i 
 |-  `' ( 1st |` _I ) = ( x e. _V |-> <. x , x >. )