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

Metamath Proof Explorer

Theorem funssres

Description: The restriction of a function to the domain of a subclass equals the subclass. (Contributed by NM, 15-Aug-1994)

Ref Expression
Assertion funssres ( ( Fun 𝐹 ∧ 𝐺 ⊆ 𝐹 ) → ( 𝐹 ↾ dom 𝐺 ) = 𝐺 )

Proof

Step Hyp Ref Expression
1 vex ⊢ 𝑦 ∈ V
2 1 opelresi ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐹 ↾ dom 𝐺 ) ↔ ( 𝑥 ∈ dom 𝐺 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) )
3 vex ⊢ 𝑥 ∈ V
4 3 1 opeldm ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 → 𝑥 ∈ dom 𝐺 )
5 4 a1i ⊢ ( 𝐺 ⊆ 𝐹 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 → 𝑥 ∈ dom 𝐺 ) )
6 ssel ⊢ ( 𝐺 ⊆ 𝐹 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) )
7 5 6 jcad ⊢ ( 𝐺 ⊆ 𝐹 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 → ( 𝑥 ∈ dom 𝐺 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) ) )
8 7 adantl ⊢ ( ( Fun 𝐹 ∧ 𝐺 ⊆ 𝐹 ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 → ( 𝑥 ∈ dom 𝐺 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) ) )
9 funeu2 ⊢ ( ( Fun 𝐹 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) → ∃! 𝑦 ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 )
10 3 eldm2 ⊢ ( 𝑥 ∈ dom 𝐺 ↔ ∃ 𝑦 ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 )
11 6 ancrd ⊢ ( 𝐺 ⊆ 𝐹 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ) ) )
12 11 eximdv ⊢ ( 𝐺 ⊆ 𝐹 → ( ∃ 𝑦 ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 → ∃ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ) ) )
13 10 12 biimtrid ⊢ ( 𝐺 ⊆ 𝐹 → ( 𝑥 ∈ dom 𝐺 → ∃ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ) ) )
14 13 imp ⊢ ( ( 𝐺 ⊆ 𝐹 ∧ 𝑥 ∈ dom 𝐺 ) → ∃ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ) )
15 eupick ⊢ ( ( ∃! 𝑦 ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ∃ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ) )
16 9 14 15 syl2an ⊢ ( ( ( Fun 𝐹 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) ∧ ( 𝐺 ⊆ 𝐹 ∧ 𝑥 ∈ dom 𝐺 ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ) )
17 16 exp43 ⊢ ( Fun 𝐹 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 → ( 𝐺 ⊆ 𝐹 → ( 𝑥 ∈ dom 𝐺 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ) ) ) ) )
18 17 com23 ⊢ ( Fun 𝐹 → ( 𝐺 ⊆ 𝐹 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 → ( 𝑥 ∈ dom 𝐺 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ) ) ) ) )
19 18 imp ⊢ ( ( Fun 𝐹 ∧ 𝐺 ⊆ 𝐹 ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 → ( 𝑥 ∈ dom 𝐺 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ) ) ) )
20 19 com34 ⊢ ( ( Fun 𝐹 ∧ 𝐺 ⊆ 𝐹 ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 → ( 𝑥 ∈ dom 𝐺 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ) ) ) )
21 20 pm2.43d ⊢ ( ( Fun 𝐹 ∧ 𝐺 ⊆ 𝐹 ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 → ( 𝑥 ∈ dom 𝐺 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ) ) )
22 21 impcomd ⊢ ( ( Fun 𝐹 ∧ 𝐺 ⊆ 𝐹 ) → ( ( 𝑥 ∈ dom 𝐺 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ) )
23 8 22 impbid ⊢ ( ( Fun 𝐹 ∧ 𝐺 ⊆ 𝐹 ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ↔ ( 𝑥 ∈ dom 𝐺 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) ) )
24 2 23 bitr4id ⊢ ( ( Fun 𝐹 ∧ 𝐺 ⊆ 𝐹 ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐹 ↾ dom 𝐺 ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ) )
25 24 alrimivv ⊢ ( ( Fun 𝐹 ∧ 𝐺 ⊆ 𝐹 ) → ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐹 ↾ dom 𝐺 ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ) )
26 relres ⊢ Rel ( 𝐹 ↾ dom 𝐺 )
27 funrel ⊢ ( Fun 𝐹 → Rel 𝐹 )
28 relss ⊢ ( 𝐺 ⊆ 𝐹 → ( Rel 𝐹 → Rel 𝐺 ) )
29 27 28 mpan9 ⊢ ( ( Fun 𝐹 ∧ 𝐺 ⊆ 𝐹 ) → Rel 𝐺 )
30 eqrel ⊢ ( ( Rel ( 𝐹 ↾ dom 𝐺 ) ∧ Rel 𝐺 ) → ( ( 𝐹 ↾ dom 𝐺 ) = 𝐺 ↔ ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐹 ↾ dom 𝐺 ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ) ) )
31 26 29 30 sylancr ⊢ ( ( Fun 𝐹 ∧ 𝐺 ⊆ 𝐹 ) → ( ( 𝐹 ↾ dom 𝐺 ) = 𝐺 ↔ ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐹 ↾ dom 𝐺 ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ) ) )
32 25 31 mpbird ⊢ ( ( Fun 𝐹 ∧ 𝐺 ⊆ 𝐹 ) → ( 𝐹 ↾ dom 𝐺 ) = 𝐺 )