Metamath Proof Explorer

Theorem mptfnf

Description: The maps-to notation defines a function with domain. (Contributed by Scott Fenton, 21-Mar-2011) (Revised by Thierry Arnoux, 10-May-2017)

Ref Expression
Hypothesis mptfnf.0 
|- F/_ x A
Assertion mptfnf 
|- ( A. x e. A B e. _V <-> ( x e. A |-> B ) Fn A )

Proof

Step Hyp Ref Expression
1 mptfnf.0 
 |-  F/_ x A
2 eueq 
 |-  ( B e. _V <-> E! y y = B )
3 2 ralbii 
 |-  ( A. x e. A B e. _V <-> A. x e. A E! y y = B )
4 r19.26 
 |-  ( A. x e. A ( E. y y = B /\ E* y y = B ) <-> ( A. x e. A E. y y = B /\ A. x e. A E* y y = B ) )
5 df-eu 
 |-  ( E! y y = B <-> ( E. y y = B /\ E* y y = B ) )
6 5 ralbii 
 |-  ( A. x e. A E! y y = B <-> A. x e. A ( E. y y = B /\ E* y y = B ) )
7 df-mpt 
 |-  ( x e. A |-> B ) = { <. x , y >. | ( x e. A /\ y = B ) }
8 7 fneq1i 
 |-  ( ( x e. A |-> B ) Fn A <-> { <. x , y >. | ( x e. A /\ y = B ) } Fn A )
9 df-fn 
 |-  ( { <. x , y >. | ( x e. A /\ y = B ) } Fn A <-> ( Fun { <. x , y >. | ( x e. A /\ y = B ) } /\ dom { <. x , y >. | ( x e. A /\ y = B ) } = A ) )
10 8 9 bitri 
 |-  ( ( x e. A |-> B ) Fn A <-> ( Fun { <. x , y >. | ( x e. A /\ y = B ) } /\ dom { <. x , y >. | ( x e. A /\ y = B ) } = A ) )
11 moanimv 
 |-  ( E* y ( x e. A /\ y = B ) <-> ( x e. A -> E* y y = B ) )
12 11 albii 
 |-  ( A. x E* y ( x e. A /\ y = B ) <-> A. x ( x e. A -> E* y y = B ) )
13 funopab 
 |-  ( Fun { <. x , y >. | ( x e. A /\ y = B ) } <-> A. x E* y ( x e. A /\ y = B ) )
14 df-ral 
 |-  ( A. x e. A E* y y = B <-> A. x ( x e. A -> E* y y = B ) )
15 12 13 14 3bitr4ri 
 |-  ( A. x e. A E* y y = B <-> Fun { <. x , y >. | ( x e. A /\ y = B ) } )
16 eqcom 
 |-  ( { x | ( x e. A /\ E. y y = B ) } = A <-> A = { x | ( x e. A /\ E. y y = B ) } )
17 dmopab 
 |-  dom { <. x , y >. | ( x e. A /\ y = B ) } = { x | E. y ( x e. A /\ y = B ) }
18 19.42v 
 |-  ( E. y ( x e. A /\ y = B ) <-> ( x e. A /\ E. y y = B ) )
19 18 abbii 
 |-  { x | E. y ( x e. A /\ y = B ) } = { x | ( x e. A /\ E. y y = B ) }
20 17 19 eqtri 
 |-  dom { <. x , y >. | ( x e. A /\ y = B ) } = { x | ( x e. A /\ E. y y = B ) }
21 20 eqeq1i 
 |-  ( dom { <. x , y >. | ( x e. A /\ y = B ) } = A <-> { x | ( x e. A /\ E. y y = B ) } = A )
22 pm4.71 
 |-  ( ( x e. A -> E. y y = B ) <-> ( x e. A <-> ( x e. A /\ E. y y = B ) ) )
23 22 albii 
 |-  ( A. x ( x e. A -> E. y y = B ) <-> A. x ( x e. A <-> ( x e. A /\ E. y y = B ) ) )
24 df-ral 
 |-  ( A. x e. A E. y y = B <-> A. x ( x e. A -> E. y y = B ) )
25 1 abeq2f 
 |-  ( A = { x | ( x e. A /\ E. y y = B ) } <-> A. x ( x e. A <-> ( x e. A /\ E. y y = B ) ) )
26 23 24 25 3bitr4i 
 |-  ( A. x e. A E. y y = B <-> A = { x | ( x e. A /\ E. y y = B ) } )
27 16 21 26 3bitr4ri 
 |-  ( A. x e. A E. y y = B <-> dom { <. x , y >. | ( x e. A /\ y = B ) } = A )
28 15 27 anbi12i 
 |-  ( ( A. x e. A E* y y = B /\ A. x e. A E. y y = B ) <-> ( Fun { <. x , y >. | ( x e. A /\ y = B ) } /\ dom { <. x , y >. | ( x e. A /\ y = B ) } = A ) )
29 ancom 
 |-  ( ( A. x e. A E* y y = B /\ A. x e. A E. y y = B ) <-> ( A. x e. A E. y y = B /\ A. x e. A E* y y = B ) )
30 10 28 29 3bitr2i 
 |-  ( ( x e. A |-> B ) Fn A <-> ( A. x e. A E. y y = B /\ A. x e. A E* y y = B ) )
31 4 6 30 3bitr4ri 
 |-  ( ( x e. A |-> B ) Fn A <-> A. x e. A E! y y = B )
32 3 31 bitr4i 
 |-  ( A. x e. A B e. _V <-> ( x e. A |-> B ) Fn A )