Metamath Proof Explorer


Theorem fnres

Description: An equivalence for functionality of a restriction. Compare dffun8 . (Contributed by Mario Carneiro, 20-May-2015) (Proof shortened by Peter Mazsa, 2-Oct-2022)

Ref Expression
Assertion fnres
|- ( ( F |` A ) Fn A <-> A. x e. A E! y x F y )

Proof

Step Hyp Ref Expression
1 ancom
 |-  ( ( A. x e. A E* y x F y /\ A. x e. A E. y x F y ) <-> ( A. x e. A E. y x F y /\ A. x e. A E* y x F y ) )
2 vex
 |-  y e. _V
3 2 brresi
 |-  ( x ( F |` A ) y <-> ( x e. A /\ x F y ) )
4 3 mobii
 |-  ( E* y x ( F |` A ) y <-> E* y ( x e. A /\ x F y ) )
5 moanimv
 |-  ( E* y ( x e. A /\ x F y ) <-> ( x e. A -> E* y x F y ) )
6 4 5 bitri
 |-  ( E* y x ( F |` A ) y <-> ( x e. A -> E* y x F y ) )
7 6 albii
 |-  ( A. x E* y x ( F |` A ) y <-> A. x ( x e. A -> E* y x F y ) )
8 relres
 |-  Rel ( F |` A )
9 dffun6
 |-  ( Fun ( F |` A ) <-> ( Rel ( F |` A ) /\ A. x E* y x ( F |` A ) y ) )
10 8 9 mpbiran
 |-  ( Fun ( F |` A ) <-> A. x E* y x ( F |` A ) y )
11 df-ral
 |-  ( A. x e. A E* y x F y <-> A. x ( x e. A -> E* y x F y ) )
12 7 10 11 3bitr4i
 |-  ( Fun ( F |` A ) <-> A. x e. A E* y x F y )
13 dmres
 |-  dom ( F |` A ) = ( A i^i dom F )
14 inss1
 |-  ( A i^i dom F ) C_ A
15 13 14 eqsstri
 |-  dom ( F |` A ) C_ A
16 eqss
 |-  ( dom ( F |` A ) = A <-> ( dom ( F |` A ) C_ A /\ A C_ dom ( F |` A ) ) )
17 15 16 mpbiran
 |-  ( dom ( F |` A ) = A <-> A C_ dom ( F |` A ) )
18 dfss3
 |-  ( A C_ dom ( F |` A ) <-> A. x e. A x e. dom ( F |` A ) )
19 13 elin2
 |-  ( x e. dom ( F |` A ) <-> ( x e. A /\ x e. dom F ) )
20 19 baib
 |-  ( x e. A -> ( x e. dom ( F |` A ) <-> x e. dom F ) )
21 vex
 |-  x e. _V
22 21 eldm
 |-  ( x e. dom F <-> E. y x F y )
23 20 22 bitrdi
 |-  ( x e. A -> ( x e. dom ( F |` A ) <-> E. y x F y ) )
24 23 ralbiia
 |-  ( A. x e. A x e. dom ( F |` A ) <-> A. x e. A E. y x F y )
25 18 24 bitri
 |-  ( A C_ dom ( F |` A ) <-> A. x e. A E. y x F y )
26 17 25 bitri
 |-  ( dom ( F |` A ) = A <-> A. x e. A E. y x F y )
27 12 26 anbi12i
 |-  ( ( Fun ( F |` A ) /\ dom ( F |` A ) = A ) <-> ( A. x e. A E* y x F y /\ A. x e. A E. y x F y ) )
28 r19.26
 |-  ( A. x e. A ( E. y x F y /\ E* y x F y ) <-> ( A. x e. A E. y x F y /\ A. x e. A E* y x F y ) )
29 1 27 28 3bitr4i
 |-  ( ( Fun ( F |` A ) /\ dom ( F |` A ) = A ) <-> A. x e. A ( E. y x F y /\ E* y x F y ) )
30 df-fn
 |-  ( ( F |` A ) Fn A <-> ( Fun ( F |` A ) /\ dom ( F |` A ) = A ) )
31 df-eu
 |-  ( E! y x F y <-> ( E. y x F y /\ E* y x F y ) )
32 31 ralbii
 |-  ( A. x e. A E! y x F y <-> A. x e. A ( E. y x F y /\ E* y x F y ) )
33 29 30 32 3bitr4i
 |-  ( ( F |` A ) Fn A <-> A. x e. A E! y x F y )