Metamath Proof Explorer

Theorem ovmptss

Description: If all the values of the mapping are subsets of a class X , then so is any evaluation of the mapping. (Contributed by Mario Carneiro, 24-Dec-2016)

Ref Expression
Hypothesis ovmptss.1 
|- F = ( x e. A , y e. B |-> C )
Assertion ovmptss 
|- ( A. x e. A A. y e. B C C_ X -> ( E F G ) C_ X )

Proof

Step Hyp Ref Expression
1 ovmptss.1 
 |-  F = ( x e. A , y e. B |-> C )
2 mpomptsx 
 |-  ( x e. A , y e. B |-> C ) = ( z e. U_ x e. A ( { x } X. B ) |-> [_ ( 1st ` z ) / x ]_ [_ ( 2nd ` z ) / y ]_ C )
3 1 2 eqtri 
 |-  F = ( z e. U_ x e. A ( { x } X. B ) |-> [_ ( 1st ` z ) / x ]_ [_ ( 2nd ` z ) / y ]_ C )
4 3 fvmptss 
 |-  ( A. z e. U_ x e. A ( { x } X. B ) [_ ( 1st ` z ) / x ]_ [_ ( 2nd ` z ) / y ]_ C C_ X -> ( F ` <. E , G >. ) C_ X )
5 vex 
 |-  u e. _V
6 vex 
 |-  v e. _V
7 5 6 op1std 
 |-  ( z = <. u , v >. -> ( 1st ` z ) = u )
8 7 csbeq1d 
 |-  ( z = <. u , v >. -> [_ ( 1st ` z ) / x ]_ [_ ( 2nd ` z ) / y ]_ C = [_ u / x ]_ [_ ( 2nd ` z ) / y ]_ C )
9 5 6 op2ndd 
 |-  ( z = <. u , v >. -> ( 2nd ` z ) = v )
10 9 csbeq1d 
 |-  ( z = <. u , v >. -> [_ ( 2nd ` z ) / y ]_ C = [_ v / y ]_ C )
11 10 csbeq2dv 
 |-  ( z = <. u , v >. -> [_ u / x ]_ [_ ( 2nd ` z ) / y ]_ C = [_ u / x ]_ [_ v / y ]_ C )
12 8 11 eqtrd 
 |-  ( z = <. u , v >. -> [_ ( 1st ` z ) / x ]_ [_ ( 2nd ` z ) / y ]_ C = [_ u / x ]_ [_ v / y ]_ C )
13 12 sseq1d 
 |-  ( z = <. u , v >. -> ( [_ ( 1st ` z ) / x ]_ [_ ( 2nd ` z ) / y ]_ C C_ X <-> [_ u / x ]_ [_ v / y ]_ C C_ X ) )
14 13 raliunxp 
 |-  ( A. z e. U_ u e. A ( { u } X. [_ u / x ]_ B ) [_ ( 1st ` z ) / x ]_ [_ ( 2nd ` z ) / y ]_ C C_ X <-> A. u e. A A. v e. [_ u / x ]_ B [_ u / x ]_ [_ v / y ]_ C C_ X )
15 nfcv 
 |-  F/_ u ( { x } X. B )
16 nfcv 
 |-  F/_ x { u }
17 nfcsb1v 
 |-  F/_ x [_ u / x ]_ B
18 16 17 nfxp 
 |-  F/_ x ( { u } X. [_ u / x ]_ B )
19 sneq 
 |-  ( x = u -> { x } = { u } )
20 csbeq1a 
 |-  ( x = u -> B = [_ u / x ]_ B )
21 19 20 xpeq12d 
 |-  ( x = u -> ( { x } X. B ) = ( { u } X. [_ u / x ]_ B ) )
22 15 18 21 cbviun 
 |-  U_ x e. A ( { x } X. B ) = U_ u e. A ( { u } X. [_ u / x ]_ B )
23 22 raleqi 
 |-  ( A. z e. U_ x e. A ( { x } X. B ) [_ ( 1st ` z ) / x ]_ [_ ( 2nd ` z ) / y ]_ C C_ X <-> A. z e. U_ u e. A ( { u } X. [_ u / x ]_ B ) [_ ( 1st ` z ) / x ]_ [_ ( 2nd ` z ) / y ]_ C C_ X )
24 nfv 
 |-  F/ u A. y e. B C C_ X
25 nfcsb1v 
 |-  F/_ x [_ u / x ]_ [_ v / y ]_ C
26 nfcv 
 |-  F/_ x X
27 25 26 nfss 
 |-  F/ x [_ u / x ]_ [_ v / y ]_ C C_ X
28 17 27 nfralw 
 |-  F/ x A. v e. [_ u / x ]_ B [_ u / x ]_ [_ v / y ]_ C C_ X
29 nfv 
 |-  F/ v C C_ X
30 nfcsb1v 
 |-  F/_ y [_ v / y ]_ C
31 nfcv 
 |-  F/_ y X
32 30 31 nfss 
 |-  F/ y [_ v / y ]_ C C_ X
33 csbeq1a 
 |-  ( y = v -> C = [_ v / y ]_ C )
34 33 sseq1d 
 |-  ( y = v -> ( C C_ X <-> [_ v / y ]_ C C_ X ) )
35 29 32 34 cbvralw 
 |-  ( A. y e. B C C_ X <-> A. v e. B [_ v / y ]_ C C_ X )
36 csbeq1a 
 |-  ( x = u -> [_ v / y ]_ C = [_ u / x ]_ [_ v / y ]_ C )
37 36 sseq1d 
 |-  ( x = u -> ( [_ v / y ]_ C C_ X <-> [_ u / x ]_ [_ v / y ]_ C C_ X ) )
38 20 37 raleqbidv 
 |-  ( x = u -> ( A. v e. B [_ v / y ]_ C C_ X <-> A. v e. [_ u / x ]_ B [_ u / x ]_ [_ v / y ]_ C C_ X ) )
39 35 38 bitrid 
 |-  ( x = u -> ( A. y e. B C C_ X <-> A. v e. [_ u / x ]_ B [_ u / x ]_ [_ v / y ]_ C C_ X ) )
40 24 28 39 cbvralw 
 |-  ( A. x e. A A. y e. B C C_ X <-> A. u e. A A. v e. [_ u / x ]_ B [_ u / x ]_ [_ v / y ]_ C C_ X )
41 14 23 40 3bitr4ri 
 |-  ( A. x e. A A. y e. B C C_ X <-> A. z e. U_ x e. A ( { x } X. B ) [_ ( 1st ` z ) / x ]_ [_ ( 2nd ` z ) / y ]_ C C_ X )
42 df-ov 
 |-  ( E F G ) = ( F ` <. E , G >. )
43 42 sseq1i 
 |-  ( ( E F G ) C_ X <-> ( F ` <. E , G >. ) C_ X )
44 4 41 43 3imtr4i 
 |-  ( A. x e. A A. y e. B C C_ X -> ( E F G ) C_ X )