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 )