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 𝐺 ) = 𝐺 )