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	⊢ ( ( 𝐹 ↾ 𝐴 ) Fn 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 𝑥 𝐹 𝑦 )

Proof

Step	Hyp	Ref	Expression
1		ancom	⊢ ( ( ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 𝑥 𝐹 𝑦 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 𝑥 𝐹 𝑦 ) ↔ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 𝑥 𝐹 𝑦 ∧ ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 𝑥 𝐹 𝑦 ) )
2		vex	⊢ 𝑦 ∈ V
3	2	brresi	⊢ ( 𝑥 ( 𝐹 ↾ 𝐴 ) 𝑦 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝐹 𝑦 ) )
4	3	mobii	⊢ ( ∃* 𝑦 𝑥 ( 𝐹 ↾ 𝐴 ) 𝑦 ↔ ∃* 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝐹 𝑦 ) )
5		moanimv	⊢ ( ∃* 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝐹 𝑦 ) ↔ ( 𝑥 ∈ 𝐴 → ∃* 𝑦 𝑥 𝐹 𝑦 ) )
6	4 5	bitri	⊢ ( ∃* 𝑦 𝑥 ( 𝐹 ↾ 𝐴 ) 𝑦 ↔ ( 𝑥 ∈ 𝐴 → ∃* 𝑦 𝑥 𝐹 𝑦 ) )
7	6	albii	⊢ ( ∀ 𝑥 ∃* 𝑦 𝑥 ( 𝐹 ↾ 𝐴 ) 𝑦 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∃* 𝑦 𝑥 𝐹 𝑦 ) )
8		relres	⊢ Rel ( 𝐹 ↾ 𝐴 )
9		dffun6	⊢ ( Fun ( 𝐹 ↾ 𝐴 ) ↔ ( Rel ( 𝐹 ↾ 𝐴 ) ∧ ∀ 𝑥 ∃* 𝑦 𝑥 ( 𝐹 ↾ 𝐴 ) 𝑦 ) )
10	8 9	mpbiran	⊢ ( Fun ( 𝐹 ↾ 𝐴 ) ↔ ∀ 𝑥 ∃* 𝑦 𝑥 ( 𝐹 ↾ 𝐴 ) 𝑦 )
11		df-ral	⊢ ( ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 𝑥 𝐹 𝑦 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∃* 𝑦 𝑥 𝐹 𝑦 ) )
12	7 10 11	3bitr4i	⊢ ( Fun ( 𝐹 ↾ 𝐴 ) ↔ ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 𝑥 𝐹 𝑦 )
13		dmres	⊢ dom ( 𝐹 ↾ 𝐴 ) = ( 𝐴 ∩ dom 𝐹 )
14		inss1	⊢ ( 𝐴 ∩ dom 𝐹 ) ⊆ 𝐴
15	13 14	eqsstri	⊢ dom ( 𝐹 ↾ 𝐴 ) ⊆ 𝐴
16		eqss	⊢ ( dom ( 𝐹 ↾ 𝐴 ) = 𝐴 ↔ ( dom ( 𝐹 ↾ 𝐴 ) ⊆ 𝐴 ∧ 𝐴 ⊆ dom ( 𝐹 ↾ 𝐴 ) ) )
17	15 16	mpbiran	⊢ ( dom ( 𝐹 ↾ 𝐴 ) = 𝐴 ↔ 𝐴 ⊆ dom ( 𝐹 ↾ 𝐴 ) )
18		dfss3	⊢ ( 𝐴 ⊆ dom ( 𝐹 ↾ 𝐴 ) ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ dom ( 𝐹 ↾ 𝐴 ) )
19	13	elin2	⊢ ( 𝑥 ∈ dom ( 𝐹 ↾ 𝐴 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ dom 𝐹 ) )
20	19	baib	⊢ ( 𝑥 ∈ 𝐴 → ( 𝑥 ∈ dom ( 𝐹 ↾ 𝐴 ) ↔ 𝑥 ∈ dom 𝐹 ) )
21		vex	⊢ 𝑥 ∈ V
22	21	eldm	⊢ ( 𝑥 ∈ dom 𝐹 ↔ ∃ 𝑦 𝑥 𝐹 𝑦 )
23	20 22	bitrdi	⊢ ( 𝑥 ∈ 𝐴 → ( 𝑥 ∈ dom ( 𝐹 ↾ 𝐴 ) ↔ ∃ 𝑦 𝑥 𝐹 𝑦 ) )
24	23	ralbiia	⊢ ( ∀ 𝑥 ∈ 𝐴 𝑥 ∈ dom ( 𝐹 ↾ 𝐴 ) ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 𝑥 𝐹 𝑦 )
25	18 24	bitri	⊢ ( 𝐴 ⊆ dom ( 𝐹 ↾ 𝐴 ) ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 𝑥 𝐹 𝑦 )
26	17 25	bitri	⊢ ( dom ( 𝐹 ↾ 𝐴 ) = 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 𝑥 𝐹 𝑦 )
27	12 26	anbi12i	⊢ ( ( Fun ( 𝐹 ↾ 𝐴 ) ∧ dom ( 𝐹 ↾ 𝐴 ) = 𝐴 ) ↔ ( ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 𝑥 𝐹 𝑦 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 𝑥 𝐹 𝑦 ) )
28		r19.26	⊢ ( ∀ 𝑥 ∈ 𝐴 ( ∃ 𝑦 𝑥 𝐹 𝑦 ∧ ∃* 𝑦 𝑥 𝐹 𝑦 ) ↔ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 𝑥 𝐹 𝑦 ∧ ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 𝑥 𝐹 𝑦 ) )
29	1 27 28	3bitr4i	⊢ ( ( Fun ( 𝐹 ↾ 𝐴 ) ∧ dom ( 𝐹 ↾ 𝐴 ) = 𝐴 ) ↔ ∀ 𝑥 ∈ 𝐴 ( ∃ 𝑦 𝑥 𝐹 𝑦 ∧ ∃* 𝑦 𝑥 𝐹 𝑦 ) )
30		df-fn	⊢ ( ( 𝐹 ↾ 𝐴 ) Fn 𝐴 ↔ ( Fun ( 𝐹 ↾ 𝐴 ) ∧ dom ( 𝐹 ↾ 𝐴 ) = 𝐴 ) )
31		df-eu	⊢ ( ∃! 𝑦 𝑥 𝐹 𝑦 ↔ ( ∃ 𝑦 𝑥 𝐹 𝑦 ∧ ∃* 𝑦 𝑥 𝐹 𝑦 ) )
32	31	ralbii	⊢ ( ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 𝑥 𝐹 𝑦 ↔ ∀ 𝑥 ∈ 𝐴 ( ∃ 𝑦 𝑥 𝐹 𝑦 ∧ ∃* 𝑦 𝑥 𝐹 𝑦 ) )
33	29 30 32	3bitr4i	⊢ ( ( 𝐹 ↾ 𝐴 ) Fn 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 𝑥 𝐹 𝑦 )