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 )