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		vex	⊢ 𝑦 ∈ V
3	1 2	opeldm	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 → 𝑥 ∈ dom 𝐺 )
4	3	a1i	⊢ ( 𝐺 ⊆ 𝐹 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 → 𝑥 ∈ dom 𝐺 ) )
5		ssel	⊢ ( 𝐺 ⊆ 𝐹 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) )
6	4 5	jcad	⊢ ( 𝐺 ⊆ 𝐹 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 → ( 𝑥 ∈ dom 𝐺 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) ) )
7	6	adantl	⊢ ( ( Fun 𝐹 ∧ 𝐺 ⊆ 𝐹 ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 → ( 𝑥 ∈ dom 𝐺 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) ) )
8		funeu2	⊢ ( ( Fun 𝐹 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) → ∃! 𝑦 ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 )
9	1	eldm2	⊢ ( 𝑥 ∈ dom 𝐺 ↔ ∃ 𝑦 ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 )
10	5	ancrd	⊢ ( 𝐺 ⊆ 𝐹 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ) ) )
11	10	eximdv	⊢ ( 𝐺 ⊆ 𝐹 → ( ∃ 𝑦 ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 → ∃ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ) ) )
12	9 11	syl5bi	⊢ ( 𝐺 ⊆ 𝐹 → ( 𝑥 ∈ dom 𝐺 → ∃ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ) ) )
13	12	imp	⊢ ( ( 𝐺 ⊆ 𝐹 ∧ 𝑥 ∈ dom 𝐺 ) → ∃ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ) )
14		eupick	⊢ ( ( ∃! 𝑦 ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ∃ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ) )
15	8 13 14	syl2an	⊢ ( ( ( Fun 𝐹 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) ∧ ( 𝐺 ⊆ 𝐹 ∧ 𝑥 ∈ dom 𝐺 ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ) )
16	15	exp43	⊢ ( Fun 𝐹 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 → ( 𝐺 ⊆ 𝐹 → ( 𝑥 ∈ dom 𝐺 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ) ) ) ) )
17	16	com23	⊢ ( Fun 𝐹 → ( 𝐺 ⊆ 𝐹 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 → ( 𝑥 ∈ dom 𝐺 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ) ) ) ) )
18	17	imp	⊢ ( ( Fun 𝐹 ∧ 𝐺 ⊆ 𝐹 ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 → ( 𝑥 ∈ dom 𝐺 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ) ) ) )
19	18	com34	⊢ ( ( Fun 𝐹 ∧ 𝐺 ⊆ 𝐹 ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 → ( 𝑥 ∈ dom 𝐺 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ) ) ) )
20	19	pm2.43d	⊢ ( ( Fun 𝐹 ∧ 𝐺 ⊆ 𝐹 ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 → ( 𝑥 ∈ dom 𝐺 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ) ) )
21	20	impcomd	⊢ ( ( Fun 𝐹 ∧ 𝐺 ⊆ 𝐹 ) → ( ( 𝑥 ∈ dom 𝐺 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ) )
22	7 21	impbid	⊢ ( ( Fun 𝐹 ∧ 𝐺 ⊆ 𝐹 ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ↔ ( 𝑥 ∈ dom 𝐺 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) ) )
23	2	opelresi	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐹 ↾ dom 𝐺 ) ↔ ( 𝑥 ∈ dom 𝐺 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) )
24	22 23	syl6rbbr	⊢ ( ( 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 𝐺 ) = 𝐺 )