Metamath Proof Explorer

Theorem fmpox

Description: Functionality, domain and codomain of a class given by the maps-to notation, where B ( x ) is not constant but depends on x . (Contributed by NM, 29-Dec-2014)

Ref Expression
Hypothesis fmpox.1 
|- F = ( x e. A , y e. B |-> C )
Assertion fmpox 
|- ( A. x e. A A. y e. B C e. D <-> F : U_ x e. A ( { x } X. B ) --> D )

Proof

Step Hyp Ref Expression
1 fmpox.1 
 |-  F = ( x e. A , y e. B |-> C )
2 vex 
 |-  z e. _V
3 vex 
 |-  w e. _V
4 2 3 op1std 
 |-  ( v = <. z , w >. -> ( 1st ` v ) = z )
5 4 csbeq1d 
 |-  ( v = <. z , w >. -> [_ ( 1st ` v ) / x ]_ [_ ( 2nd ` v ) / y ]_ C = [_ z / x ]_ [_ ( 2nd ` v ) / y ]_ C )
6 2 3 op2ndd 
 |-  ( v = <. z , w >. -> ( 2nd ` v ) = w )
7 6 csbeq1d 
 |-  ( v = <. z , w >. -> [_ ( 2nd ` v ) / y ]_ C = [_ w / y ]_ C )
8 7 csbeq2dv 
 |-  ( v = <. z , w >. -> [_ z / x ]_ [_ ( 2nd ` v ) / y ]_ C = [_ z / x ]_ [_ w / y ]_ C )
9 5 8 eqtrd 
 |-  ( v = <. z , w >. -> [_ ( 1st ` v ) / x ]_ [_ ( 2nd ` v ) / y ]_ C = [_ z / x ]_ [_ w / y ]_ C )
10 9 eleq1d 
 |-  ( v = <. z , w >. -> ( [_ ( 1st ` v ) / x ]_ [_ ( 2nd ` v ) / y ]_ C e. D <-> [_ z / x ]_ [_ w / y ]_ C e. D ) )
11 10 raliunxp 
 |-  ( A. v e. U_ z e. A ( { z } X. [_ z / x ]_ B ) [_ ( 1st ` v ) / x ]_ [_ ( 2nd ` v ) / y ]_ C e. D <-> A. z e. A A. w e. [_ z / x ]_ B [_ z / x ]_ [_ w / y ]_ C e. D )
12 nfv 
 |-  F/ z ( ( x e. A /\ y e. B ) /\ v = C )
13 nfv 
 |-  F/ w ( ( x e. A /\ y e. B ) /\ v = C )
14 nfv 
 |-  F/ x z e. A
15 nfcsb1v 
 |-  F/_ x [_ z / x ]_ B
16 15 nfcri 
 |-  F/ x w e. [_ z / x ]_ B
17 14 16 nfan 
 |-  F/ x ( z e. A /\ w e. [_ z / x ]_ B )
18 nfcsb1v 
 |-  F/_ x [_ z / x ]_ [_ w / y ]_ C
19 18 nfeq2 
 |-  F/ x v = [_ z / x ]_ [_ w / y ]_ C
20 17 19 nfan 
 |-  F/ x ( ( z e. A /\ w e. [_ z / x ]_ B ) /\ v = [_ z / x ]_ [_ w / y ]_ C )
21 nfv 
 |-  F/ y ( z e. A /\ w e. [_ z / x ]_ B )
22 nfcv 
 |-  F/_ y z
23 nfcsb1v 
 |-  F/_ y [_ w / y ]_ C
24 22 23 nfcsbw 
 |-  F/_ y [_ z / x ]_ [_ w / y ]_ C
25 24 nfeq2 
 |-  F/ y v = [_ z / x ]_ [_ w / y ]_ C
26 21 25 nfan 
 |-  F/ y ( ( z e. A /\ w e. [_ z / x ]_ B ) /\ v = [_ z / x ]_ [_ w / y ]_ C )
27 eleq1w 
 |-  ( x = z -> ( x e. A <-> z e. A ) )
28 27 adantr 
 |-  ( ( x = z /\ y = w ) -> ( x e. A <-> z e. A ) )
29 eleq1w 
 |-  ( y = w -> ( y e. B <-> w e. B ) )
30 csbeq1a 
 |-  ( x = z -> B = [_ z / x ]_ B )
31 30 eleq2d 
 |-  ( x = z -> ( w e. B <-> w e. [_ z / x ]_ B ) )
32 29 31 sylan9bbr 
 |-  ( ( x = z /\ y = w ) -> ( y e. B <-> w e. [_ z / x ]_ B ) )
33 28 32 anbi12d 
 |-  ( ( x = z /\ y = w ) -> ( ( x e. A /\ y e. B ) <-> ( z e. A /\ w e. [_ z / x ]_ B ) ) )
34 csbeq1a 
 |-  ( y = w -> C = [_ w / y ]_ C )
35 csbeq1a 
 |-  ( x = z -> [_ w / y ]_ C = [_ z / x ]_ [_ w / y ]_ C )
36 34 35 sylan9eqr 
 |-  ( ( x = z /\ y = w ) -> C = [_ z / x ]_ [_ w / y ]_ C )
37 36 eqeq2d 
 |-  ( ( x = z /\ y = w ) -> ( v = C <-> v = [_ z / x ]_ [_ w / y ]_ C ) )
38 33 37 anbi12d 
 |-  ( ( x = z /\ y = w ) -> ( ( ( x e. A /\ y e. B ) /\ v = C ) <-> ( ( z e. A /\ w e. [_ z / x ]_ B ) /\ v = [_ z / x ]_ [_ w / y ]_ C ) ) )
39 12 13 20 26 38 cbvoprab12 
 |-  { <. <. x , y >. , v >. | ( ( x e. A /\ y e. B ) /\ v = C ) } = { <. <. z , w >. , v >. | ( ( z e. A /\ w e. [_ z / x ]_ B ) /\ v = [_ z / x ]_ [_ w / y ]_ C ) }
40 df-mpo 
 |-  ( x e. A , y e. B |-> C ) = { <. <. x , y >. , v >. | ( ( x e. A /\ y e. B ) /\ v = C ) }
41 df-mpo 
 |-  ( z e. A , w e. [_ z / x ]_ B |-> [_ z / x ]_ [_ w / y ]_ C ) = { <. <. z , w >. , v >. | ( ( z e. A /\ w e. [_ z / x ]_ B ) /\ v = [_ z / x ]_ [_ w / y ]_ C ) }
42 39 40 41 3eqtr4i 
 |-  ( x e. A , y e. B |-> C ) = ( z e. A , w e. [_ z / x ]_ B |-> [_ z / x ]_ [_ w / y ]_ C )
43 9 mpomptx 
 |-  ( v e. U_ z e. A ( { z } X. [_ z / x ]_ B ) |-> [_ ( 1st ` v ) / x ]_ [_ ( 2nd ` v ) / y ]_ C ) = ( z e. A , w e. [_ z / x ]_ B |-> [_ z / x ]_ [_ w / y ]_ C )
44 42 1 43 3eqtr4i 
 |-  F = ( v e. U_ z e. A ( { z } X. [_ z / x ]_ B ) |-> [_ ( 1st ` v ) / x ]_ [_ ( 2nd ` v ) / y ]_ C )
45 44 fmpt 
 |-  ( A. v e. U_ z e. A ( { z } X. [_ z / x ]_ B ) [_ ( 1st ` v ) / x ]_ [_ ( 2nd ` v ) / y ]_ C e. D <-> F : U_ z e. A ( { z } X. [_ z / x ]_ B ) --> D )
46 11 45 bitr3i 
 |-  ( A. z e. A A. w e. [_ z / x ]_ B [_ z / x ]_ [_ w / y ]_ C e. D <-> F : U_ z e. A ( { z } X. [_ z / x ]_ B ) --> D )
47 nfv 
 |-  F/ z A. y e. B C e. D
48 18 nfel1 
 |-  F/ x [_ z / x ]_ [_ w / y ]_ C e. D
49 15 48 nfralw 
 |-  F/ x A. w e. [_ z / x ]_ B [_ z / x ]_ [_ w / y ]_ C e. D
50 nfv 
 |-  F/ w C e. D
51 23 nfel1 
 |-  F/ y [_ w / y ]_ C e. D
52 34 eleq1d 
 |-  ( y = w -> ( C e. D <-> [_ w / y ]_ C e. D ) )
53 50 51 52 cbvralw 
 |-  ( A. y e. B C e. D <-> A. w e. B [_ w / y ]_ C e. D )
54 35 eleq1d 
 |-  ( x = z -> ( [_ w / y ]_ C e. D <-> [_ z / x ]_ [_ w / y ]_ C e. D ) )
55 30 54 raleqbidv 
 |-  ( x = z -> ( A. w e. B [_ w / y ]_ C e. D <-> A. w e. [_ z / x ]_ B [_ z / x ]_ [_ w / y ]_ C e. D ) )
56 53 55 syl5bb 
 |-  ( x = z -> ( A. y e. B C e. D <-> A. w e. [_ z / x ]_ B [_ z / x ]_ [_ w / y ]_ C e. D ) )
57 47 49 56 cbvralw 
 |-  ( A. x e. A A. y e. B C e. D <-> A. z e. A A. w e. [_ z / x ]_ B [_ z / x ]_ [_ w / y ]_ C e. D )
58 nfcv 
 |-  F/_ z ( { x } X. B )
59 nfcv 
 |-  F/_ x { z }
60 59 15 nfxp 
 |-  F/_ x ( { z } X. [_ z / x ]_ B )
61 sneq 
 |-  ( x = z -> { x } = { z } )
62 61 30 xpeq12d 
 |-  ( x = z -> ( { x } X. B ) = ( { z } X. [_ z / x ]_ B ) )
63 58 60 62 cbviun 
 |-  U_ x e. A ( { x } X. B ) = U_ z e. A ( { z } X. [_ z / x ]_ B )
64 63 feq2i 
 |-  ( F : U_ x e. A ( { x } X. B ) --> D <-> F : U_ z e. A ( { z } X. [_ z / x ]_ B ) --> D )
65 46 57 64 3bitr4i 
 |-  ( A. x e. A A. y e. B C e. D <-> F : U_ x e. A ( { x } X. B ) --> D )