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