This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 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 eqtr3id ⊢ ( 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 𝐵 ) )