Metamath Proof Explorer

Theorem mpoexxg

Description: Existence of an operation class abstraction (version for dependent domains). (Contributed by Mario Carneiro, 30-Dec-2016)

Ref Expression
Hypothesis mpoexg.1 
|- F = ( x e. A , y e. B |-> C )
Assertion mpoexxg 
|- ( ( A e. R /\ A. x e. A B e. S ) -> F e. _V )

Proof

Step Hyp Ref Expression
1 mpoexg.1 
 |-  F = ( x e. A , y e. B |-> C )
2 1 mpofun 
 |-  Fun F
3 1 dmmpossx 
 |-  dom F C_ U_ x e. A ( { x } X. B )
4 snex 
 |-  { x } e. _V
5 xpexg 
 |-  ( ( { x } e. _V /\ B e. S ) -> ( { x } X. B ) e. _V )
6 4 5 mpan 
 |-  ( B e. S -> ( { x } X. B ) e. _V )
7 6 ralimi 
 |-  ( A. x e. A B e. S -> A. x e. A ( { x } X. B ) e. _V )
8 iunexg 
 |-  ( ( A e. R /\ A. x e. A ( { x } X. B ) e. _V ) -> U_ x e. A ( { x } X. B ) e. _V )
9 7 8 sylan2 
 |-  ( ( A e. R /\ A. x e. A B e. S ) -> U_ x e. A ( { x } X. B ) e. _V )
10 ssexg 
 |-  ( ( dom F C_ U_ x e. A ( { x } X. B ) /\ U_ x e. A ( { x } X. B ) e. _V ) -> dom F e. _V )
11 3 9 10 sylancr 
 |-  ( ( A e. R /\ A. x e. A B e. S ) -> dom F e. _V )
12 funex 
 |-  ( ( Fun F /\ dom F e. _V ) -> F e. _V )
13 2 11 12 sylancr 
 |-  ( ( A e. R /\ A. x e. A B e. S ) -> F e. _V )