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

Metamath Proof Explorer

Theorem oprabexd

Description: Existence of an operator abstraction. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by AV, 9-Aug-2024)

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

Proof

Step Hyp Ref Expression
1 oprabexd.1 
 |-  ( ph -> A e. V )
2 oprabexd.2 
 |-  ( ph -> B e. W )
3 oprabexd.3 
 |-  ( ( ph /\ ( x e. A /\ y e. B ) ) -> E* z ps )
4 oprabexd.4 
 |-  ( ph -> F = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ ps ) } )
5 3 ex 
 |-  ( ph -> ( ( x e. A /\ y e. B ) -> E* z ps ) )
6 moanimv 
 |-  ( E* z ( ( x e. A /\ y e. B ) /\ ps ) <-> ( ( x e. A /\ y e. B ) -> E* z ps ) )
7 5 6 sylibr 
 |-  ( ph -> E* z ( ( x e. A /\ y e. B ) /\ ps ) )
8 7 alrimivv 
 |-  ( ph -> A. x A. y E* z ( ( x e. A /\ y e. B ) /\ ps ) )
9 funoprabg 
 |-  ( A. x A. y E* z ( ( x e. A /\ y e. B ) /\ ps ) -> Fun { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ ps ) } )
10 8 9 syl 
 |-  ( ph -> Fun { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ ps ) } )
11 dmoprabss 
 |-  dom { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ ps ) } C_ ( A X. B )
12 1 2 xpexd 
 |-  ( ph -> ( A X. B ) e. _V )
13 ssexg 
 |-  ( ( dom { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ ps ) } C_ ( A X. B ) /\ ( A X. B ) e. _V ) -> dom { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ ps ) } e. _V )
14 11 12 13 sylancr 
 |-  ( ph -> dom { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ ps ) } e. _V )
15 funex 
 |-  ( ( Fun { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ ps ) } /\ dom { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ ps ) } e. _V ) -> { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ ps ) } e. _V )
16 10 14 15 syl2anc 
 |-  ( ph -> { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ ps ) } e. _V )
17 4 16 eqeltrd 
 |-  ( ph -> F e. _V )