Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  offval2 Structured version   Unicode version

Theorem offval2 6322
 Description: The function operation expressed as a mapping. (Contributed by Mario Carneiro, 20-Jul-2014.)
Hypotheses
Ref Expression
offval2.1
offval2.2
offval2.3
offval2.4
offval2.5
Assertion
Ref Expression
offval2
Distinct variable groups:   ,   ,   ,
Allowed substitution hints:   ()   ()   ()   ()   ()   ()   ()

Proof of Theorem offval2
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 offval2.2 . . . . . 6
21ralrimiva 2789 . . . . 5
3 eqid 2436 . . . . . 6
43fnmpt 5571 . . . . 5
52, 4syl 16 . . . 4
6 offval2.4 . . . . 5
76fneq1d 5536 . . . 4
85, 7mpbird 224 . . 3
9 offval2.3 . . . . . 6
109ralrimiva 2789 . . . . 5
11 eqid 2436 . . . . . 6
1211fnmpt 5571 . . . . 5
1310, 12syl 16 . . . 4
14 offval2.5 . . . . 5
1514fneq1d 5536 . . . 4
1613, 15mpbird 224 . . 3
17 offval2.1 . . 3
18 inidm 3550 . . 3
196adantr 452 . . . 4
2019fveq1d 5730 . . 3
2114adantr 452 . . . 4
2221fveq1d 5730 . . 3
238, 16, 17, 17, 18, 20, 22offval 6312 . 2
24 nffvmpt1 5736 . . . . 5
25 nfcv 2572 . . . . 5
26 nffvmpt1 5736 . . . . 5
2724, 25, 26nfov 6104 . . . 4
28 nfcv 2572 . . . 4
29 fveq2 5728 . . . . 5
30 fveq2 5728 . . . . 5
3129, 30oveq12d 6099 . . . 4
3227, 28, 31cbvmpt 4299 . . 3
33 simpr 448 . . . . . 6
343fvmpt2 5812 . . . . . 6
3533, 1, 34syl2anc 643 . . . . 5
3611fvmpt2 5812 . . . . . 6
3733, 9, 36syl2anc 643 . . . . 5
3835, 37oveq12d 6099 . . . 4
3938mpteq2dva 4295 . . 3
4032, 39syl5eq 2480 . 2
4123, 40eqtrd 2468 1