This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )