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

Theorem off 6320
 Description: The function operation produces a function. (Contributed by Mario Carneiro, 20-Jul-2014.)
Hypotheses
Ref Expression
off.1
off.2
off.3
off.4
off.5
off.6
Assertion
Ref Expression
off
Distinct variable groups:   ,   ,,   ,,   ,,   ,,   ,,   ,,
Allowed substitution hints:   (,)   (,)   (,)   ()   (,)   (,)

Proof of Theorem off
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 off.2 . . . . 5
2 off.6 . . . . . . 7
3 inss1 3561 . . . . . . 7
42, 3eqsstr3i 3379 . . . . . 6
54sseli 3344 . . . . 5
6 ffvelrn 5868 . . . . 5
71, 5, 6syl2an 464 . . . 4
8 off.3 . . . . 5
9 inss2 3562 . . . . . . 7
102, 9eqsstr3i 3379 . . . . . 6
1110sseli 3344 . . . . 5
12 ffvelrn 5868 . . . . 5
138, 11, 12syl2an 464 . . . 4
14 off.1 . . . . . 6
1514ralrimivva 2798 . . . . 5
1615adantr 452 . . . 4
17 oveq1 6088 . . . . . 6
1817eleq1d 2502 . . . . 5
19 oveq2 6089 . . . . . 6
2019eleq1d 2502 . . . . 5
2118, 20rspc2va 3059 . . . 4
227, 13, 16, 21syl21anc 1183 . . 3
23 eqid 2436 . . 3
2422, 23fmptd 5893 . 2
25 ffn 5591 . . . . 5
261, 25syl 16 . . . 4
27 ffn 5591 . . . . 5
288, 27syl 16 . . . 4
29 off.4 . . . 4
30 off.5 . . . 4
31 eqidd 2437 . . . 4
32 eqidd 2437 . . . 4
3326, 28, 29, 30, 2, 31, 32offval 6312 . . 3
3433feq1d 5580 . 2
3524, 34mpbird 224 1