Metamath Proof Explorer


Theorem ovolfcl

Description: Closure for the interval endpoint function. (Contributed by Mario Carneiro, 16-Mar-2014)

Ref Expression
Assertion ovolfcl F:2N1stFN2ndFN1stFN2ndFN

Proof

Step Hyp Ref Expression
1 ffvelrn F:2NFN2
2 1 elin2d F:2NFN2
3 1st2nd2 FN2FN=1stFN2ndFN
4 2 3 syl F:2NFN=1stFN2ndFN
5 4 1 eqeltrrd F:2N1stFN2ndFN2
6 ancom 1stFN2ndFN1stFN2ndFN1stFN2ndFN1stFN2ndFN
7 elin 1stFN2ndFN21stFN2ndFN1stFN2ndFN2
8 df-br 1stFN2ndFN1stFN2ndFN
9 8 bicomi 1stFN2ndFN1stFN2ndFN
10 opelxp 1stFN2ndFN21stFN2ndFN
11 9 10 anbi12i 1stFN2ndFN1stFN2ndFN21stFN2ndFN1stFN2ndFN
12 7 11 bitri 1stFN2ndFN21stFN2ndFN1stFN2ndFN
13 df-3an 1stFN2ndFN1stFN2ndFN1stFN2ndFN1stFN2ndFN
14 6 12 13 3bitr4i 1stFN2ndFN21stFN2ndFN1stFN2ndFN
15 5 14 sylib F:2N1stFN2ndFN1stFN2ndFN