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