Metamath Proof Explorer

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 ⊢ B ∈ V ∧ F ∈ A ↑ 𝑝𝑚 C → F ↾ B ∈ A ↑ 𝑝𝑚 B

Proof

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