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 ( ( 𝐵 ∈ 𝑉 ∧ 𝐹 ∈ ( 𝐴 ↑pm 𝐶 ) ) → ( 𝐹 ↾ 𝐵 ) ∈ ( 𝐴 ↑pm 𝐵 ) )

Proof

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