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