Theorem pmresg

Description: Elementhood of a restricted function in the set of partial functions. (Contributed by Mario Carneiro, 31-Dec-2013)

	Ref	Expression
Assertion	pmresg	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐹 ∈ ( 𝐴 ↑pm 𝐶 ) ) → ( 𝐹 ↾ 𝐵 ) ∈ ( 𝐴 ↑pm 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		n0i	⊢ ( 𝐹 ∈ ( 𝐴 ↑pm 𝐶 ) → ¬ ( 𝐴 ↑pm 𝐶 ) = ∅ )
2		fnpm	⊢ ↑pm Fn ( V × V )
3	2	fndmi	⊢ dom ↑pm = ( V × V )
4	3	ndmov	⊢ ( ¬ ( 𝐴 ∈ V ∧ 𝐶 ∈ V ) → ( 𝐴 ↑pm 𝐶 ) = ∅ )
5	1 4	nsyl2	⊢ ( 𝐹 ∈ ( 𝐴 ↑pm 𝐶 ) → ( 𝐴 ∈ V ∧ 𝐶 ∈ V ) )
6	5	simpld	⊢ ( 𝐹 ∈ ( 𝐴 ↑pm 𝐶 ) → 𝐴 ∈ V )
7	6	adantl	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐹 ∈ ( 𝐴 ↑pm 𝐶 ) ) → 𝐴 ∈ V )
8		simpl	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐹 ∈ ( 𝐴 ↑pm 𝐶 ) ) → 𝐵 ∈ 𝑉 )
9		elpmi	⊢ ( 𝐹 ∈ ( 𝐴 ↑pm 𝐶 ) → ( 𝐹 : dom 𝐹 ⟶ 𝐴 ∧ dom 𝐹 ⊆ 𝐶 ) )
10	9	simpld	⊢ ( 𝐹 ∈ ( 𝐴 ↑pm 𝐶 ) → 𝐹 : dom 𝐹 ⟶ 𝐴 )
11	10	adantl	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐹 ∈ ( 𝐴 ↑pm 𝐶 ) ) → 𝐹 : dom 𝐹 ⟶ 𝐴 )
12		inss1	⊢ ( dom 𝐹 ∩ 𝐵 ) ⊆ dom 𝐹
13		fssres	⊢ ( ( 𝐹 : dom 𝐹 ⟶ 𝐴 ∧ ( dom 𝐹 ∩ 𝐵 ) ⊆ dom 𝐹 ) → ( 𝐹 ↾ ( dom 𝐹 ∩ 𝐵 ) ) : ( dom 𝐹 ∩ 𝐵 ) ⟶ 𝐴 )
14	11 12 13	sylancl	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐹 ∈ ( 𝐴 ↑pm 𝐶 ) ) → ( 𝐹 ↾ ( dom 𝐹 ∩ 𝐵 ) ) : ( dom 𝐹 ∩ 𝐵 ) ⟶ 𝐴 )
15		ffun	⊢ ( 𝐹 : dom 𝐹 ⟶ 𝐴 → Fun 𝐹 )
16		resres	⊢ ( ( 𝐹 ↾ dom 𝐹 ) ↾ 𝐵 ) = ( 𝐹 ↾ ( dom 𝐹 ∩ 𝐵 ) )
17		funrel	⊢ ( Fun 𝐹 → Rel 𝐹 )
18		resdm	⊢ ( Rel 𝐹 → ( 𝐹 ↾ dom 𝐹 ) = 𝐹 )
19		reseq1	⊢ ( ( 𝐹 ↾ dom 𝐹 ) = 𝐹 → ( ( 𝐹 ↾ dom 𝐹 ) ↾ 𝐵 ) = ( 𝐹 ↾ 𝐵 ) )
20	17 18 19	3syl	⊢ ( Fun 𝐹 → ( ( 𝐹 ↾ dom 𝐹 ) ↾ 𝐵 ) = ( 𝐹 ↾ 𝐵 ) )
21	16 20	syl5eqr	⊢ ( Fun 𝐹 → ( 𝐹 ↾ ( dom 𝐹 ∩ 𝐵 ) ) = ( 𝐹 ↾ 𝐵 ) )
22	11 15 21	3syl	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐹 ∈ ( 𝐴 ↑pm 𝐶 ) ) → ( 𝐹 ↾ ( dom 𝐹 ∩ 𝐵 ) ) = ( 𝐹 ↾ 𝐵 ) )
23	22	feq1d	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐹 ∈ ( 𝐴 ↑pm 𝐶 ) ) → ( ( 𝐹 ↾ ( dom 𝐹 ∩ 𝐵 ) ) : ( dom 𝐹 ∩ 𝐵 ) ⟶ 𝐴 ↔ ( 𝐹 ↾ 𝐵 ) : ( dom 𝐹 ∩ 𝐵 ) ⟶ 𝐴 ) )
24	14 23	mpbid	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐹 ∈ ( 𝐴 ↑pm 𝐶 ) ) → ( 𝐹 ↾ 𝐵 ) : ( dom 𝐹 ∩ 𝐵 ) ⟶ 𝐴 )
25		inss2	⊢ ( dom 𝐹 ∩ 𝐵 ) ⊆ 𝐵
26		elpm2r	⊢ ( ( ( 𝐴 ∈ V ∧ 𝐵 ∈ 𝑉 ) ∧ ( ( 𝐹 ↾ 𝐵 ) : ( dom 𝐹 ∩ 𝐵 ) ⟶ 𝐴 ∧ ( dom 𝐹 ∩ 𝐵 ) ⊆ 𝐵 ) ) → ( 𝐹 ↾ 𝐵 ) ∈ ( 𝐴 ↑pm 𝐵 ) )
27	25 26	mpanr2	⊢ ( ( ( 𝐴 ∈ V ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐹 ↾ 𝐵 ) : ( dom 𝐹 ∩ 𝐵 ) ⟶ 𝐴 ) → ( 𝐹 ↾ 𝐵 ) ∈ ( 𝐴 ↑pm 𝐵 ) )
28	7 8 24 27	syl21anc	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐹 ∈ ( 𝐴 ↑pm 𝐶 ) ) → ( 𝐹 ↾ 𝐵 ) ∈ ( 𝐴 ↑pm 𝐵 ) )