This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem oprabex

Description: Existence of an operation class abstraction. (Contributed by NM, 19-Oct-2004)

Ref Expression
Hypotheses oprabex.1 
|- A e. _V
oprabex.2 
|- B e. _V
oprabex.3 
|- ( ( x e. A /\ y e. B ) -> E* z ph )
oprabex.4 
|- F = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ ph ) }
Assertion oprabex 
|- F e. _V

Proof

Step Hyp Ref Expression
1 oprabex.1 
 |-  A e. _V
2 oprabex.2 
 |-  B e. _V
3 oprabex.3 
 |-  ( ( x e. A /\ y e. B ) -> E* z ph )
4 oprabex.4 
 |-  F = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ ph ) }
5 moanimv 
 |-  ( E* z ( ( x e. A /\ y e. B ) /\ ph ) <-> ( ( x e. A /\ y e. B ) -> E* z ph ) )
6 3 5 mpbir 
 |-  E* z ( ( x e. A /\ y e. B ) /\ ph )
7 6 funoprab 
 |-  Fun { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ ph ) }
8 1 2 xpex 
 |-  ( A X. B ) e. _V
9 dmoprabss 
 |-  dom { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ ph ) } C_ ( A X. B )
10 8 9 ssexi 
 |-  dom { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ ph ) } e. _V
11 funex 
 |-  ( ( Fun { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ ph ) } /\ dom { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ ph ) } e. _V ) -> { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ ph ) } e. _V )
12 7 10 11 mp2an 
 |-  { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ ph ) } e. _V
13 4 12 eqeltri 
 |-  F e. _V