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 syl5bi ( 𝐺𝐹 → ( 𝑥 ∈ 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 𝐺 ) = 𝐺 )