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 syl6ibr
 |-  ( ( 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 } )