Metamath Proof Explorer

Theorem fnoprabg

Description: Functionality and domain of an operation class abstraction. (Contributed by NM, 28-Aug-2007)

Ref Expression
Assertion fnoprabg 
|- ( A. x A. y ( ph -> E! z ps ) -> { <. <. x , y >. , z >. | ( ph /\ ps ) } Fn { <. x , y >. | ph } )

Proof

Step Hyp Ref Expression
1 eumo 
 |-  ( E! z ps -> E* z ps )
2 1 imim2i 
 |-  ( ( ph -> E! z ps ) -> ( ph -> E* z ps ) )
3 moanimv 
 |-  ( E* z ( ph /\ ps ) <-> ( ph -> E* z ps ) )
4 2 3 sylibr 
 |-  ( ( ph -> E! z ps ) -> E* z ( ph /\ ps ) )
5 4 2alimi 
 |-  ( A. x A. y ( ph -> E! z ps ) -> A. x A. y E* z ( ph /\ ps ) )
6 funoprabg 
 |-  ( A. x A. y E* z ( ph /\ ps ) -> Fun { <. <. x , y >. , z >. | ( ph /\ ps ) } )
7 5 6 syl 
 |-  ( A. x A. y ( ph -> E! z ps ) -> Fun { <. <. x , y >. , z >. | ( ph /\ ps ) } )
8 dmoprab 
 |-  dom { <. <. x , y >. , z >. | ( ph /\ ps ) } = { <. x , y >. | E. z ( ph /\ ps ) }
9 nfa1 
 |-  F/ x A. x A. y ( ph -> E! z ps )
10 nfa2 
 |-  F/ y A. x A. y ( ph -> E! z ps )
11 simpl 
 |-  ( ( ph /\ ps ) -> ph )
12 11 exlimiv 
 |-  ( E. z ( ph /\ ps ) -> ph )
13 euex 
 |-  ( E! z ps -> E. z ps )
14 13 imim2i 
 |-  ( ( ph -> E! z ps ) -> ( ph -> E. z ps ) )
15 14 ancld 
 |-  ( ( ph -> E! z ps ) -> ( ph -> ( ph /\ E. z ps ) ) )
16 19.42v 
 |-  ( E. z ( ph /\ ps ) <-> ( ph /\ E. z ps ) )
17 15 16 imbitrrdi 
 |-  ( ( ph -> E! z ps ) -> ( ph -> E. z ( ph /\ ps ) ) )
18 12 17 impbid2 
 |-  ( ( ph -> E! z ps ) -> ( E. z ( ph /\ ps ) <-> ph ) )
19 18 sps 
 |-  ( A. y ( ph -> E! z ps ) -> ( E. z ( ph /\ ps ) <-> ph ) )
20 19 sps 
 |-  ( A. x A. y ( ph -> E! z ps ) -> ( E. z ( ph /\ ps ) <-> ph ) )
21 9 10 20 opabbid 
 |-  ( A. x A. y ( ph -> E! z ps ) -> { <. x , y >. | E. z ( ph /\ ps ) } = { <. x , y >. | ph } )
22 8 21 eqtrid 
 |-  ( A. x A. y ( ph -> E! z ps ) -> dom { <. <. x , y >. , z >. | ( ph /\ ps ) } = { <. x , y >. | ph } )
23 df-fn 
 |-  ( { <. <. x , y >. , z >. | ( ph /\ ps ) } Fn { <. x , y >. | ph } <-> ( Fun { <. <. x , y >. , z >. | ( ph /\ ps ) } /\ dom { <. <. x , y >. , z >. | ( ph /\ ps ) } = { <. x , y >. | ph } ) )
24 7 22 23 sylanbrc 
 |-  ( A. x A. y ( ph -> E! z ps ) -> { <. <. x , y >. , z >. | ( ph /\ ps ) } Fn { <. x , y >. | ph } )