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 𝐵 ) )