Metamath Proof Explorer

Theorem oprabex3

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

Ref Expression
Hypotheses oprabex3.1 
|- H e. _V
oprabex3.2 
|- F = { <. <. x , y >. , z >. | ( ( x e. ( H X. H ) /\ y e. ( H X. H ) ) /\ E. w E. v E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = R ) ) }
Assertion oprabex3 
|- F e. _V

Proof

Step Hyp Ref Expression
1 oprabex3.1 
 |-  H e. _V
2 oprabex3.2 
 |-  F = { <. <. x , y >. , z >. | ( ( x e. ( H X. H ) /\ y e. ( H X. H ) ) /\ E. w E. v E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = R ) ) }
3 1 1 xpex 
 |-  ( H X. H ) e. _V
4 moeq 
 |-  E* z z = R
5 4 mosubop 
 |-  E* z E. u E. f ( y = <. u , f >. /\ z = R )
6 5 mosubop 
 |-  E* z E. w E. v ( x = <. w , v >. /\ E. u E. f ( y = <. u , f >. /\ z = R ) )
7 anass 
 |-  ( ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = R ) <-> ( x = <. w , v >. /\ ( y = <. u , f >. /\ z = R ) ) )
8 7 2exbii 
 |-  ( E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = R ) <-> E. u E. f ( x = <. w , v >. /\ ( y = <. u , f >. /\ z = R ) ) )
9 19.42vv 
 |-  ( E. u E. f ( x = <. w , v >. /\ ( y = <. u , f >. /\ z = R ) ) <-> ( x = <. w , v >. /\ E. u E. f ( y = <. u , f >. /\ z = R ) ) )
10 8 9 bitri 
 |-  ( E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = R ) <-> ( x = <. w , v >. /\ E. u E. f ( y = <. u , f >. /\ z = R ) ) )
11 10 2exbii 
 |-  ( E. w E. v E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = R ) <-> E. w E. v ( x = <. w , v >. /\ E. u E. f ( y = <. u , f >. /\ z = R ) ) )
12 11 mobii 
 |-  ( E* z E. w E. v E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = R ) <-> E* z E. w E. v ( x = <. w , v >. /\ E. u E. f ( y = <. u , f >. /\ z = R ) ) )
13 6 12 mpbir 
 |-  E* z E. w E. v E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = R )
14 13 a1i 
 |-  ( ( x e. ( H X. H ) /\ y e. ( H X. H ) ) -> E* z E. w E. v E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = R ) )
15 3 3 14 2 oprabex 
 |-  F e. _V