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

Theorem pcocn 19044
 Description: The concatenation of two paths is a path. (Contributed by Jeff Madsen, 19-Jun-2010.) (Proof shortened by Mario Carneiro, 7-Jun-2014.)
Hypotheses
Ref Expression
pcoval.2
pcoval.3
pcoval2.4
Assertion
Ref Expression
pcocn

Proof of Theorem pcocn
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 pcoval.2 . . 3
2 pcoval.3 . . 3
31, 2pcoval 19038 . 2
4 iitopon 18911 . . . 4 TopOn
54a1i 11 . . 3 TopOn
65cnmptid 17695 . . 3
7 0elunit 11017 . . . . 5
87a1i 11 . . . 4
95, 5, 8cnmptc 17696 . . 3
10 eqid 2438 . . . 4
11 eqid 2438 . . . 4 t t
12 eqid 2438 . . . 4 t t
13 dfii2 18914 . . . 4 t
14 0re 9093 . . . . 5
1514a1i 11 . . . 4
16 1re 9092 . . . . 5
1716a1i 11 . . . 4
1816rehalfcli 10218 . . . . . 6
19 halfgt0 10190 . . . . . . 7
2014, 18, 19ltleii 9198 . . . . . 6
21 halflt1 10191 . . . . . . 7
2218, 16, 21ltleii 9198 . . . . . 6
2314, 16elicc2i 10978 . . . . . 6
2418, 20, 22, 23mpbir3an 1137 . . . . 5
2524a1i 11 . . . 4
26 pcoval2.4 . . . . . 6
2726adantr 453 . . . . 5
28 simprl 734 . . . . . . . 8
2928oveq2d 6099 . . . . . . 7
30 2cn 10072 . . . . . . . 8
31 2ne0 10085 . . . . . . . 8
3230, 31recidi 9747 . . . . . . 7
3329, 32syl6eq 2486 . . . . . 6
3433fveq2d 5734 . . . . 5
3533oveq1d 6098 . . . . . . 7
36 1m1e0 10070 . . . . . . 7
3735, 36syl6eq 2486 . . . . . 6
3837fveq2d 5734 . . . . 5
3927, 34, 383eqtr4d 2480 . . . 4
40 retopon 18799 . . . . . . 7 TopOn
41 iccssre 10994 . . . . . . . 8
4214, 18, 41mp2an 655 . . . . . . 7
43 resttopon 17227 . . . . . . 7 TopOn t TopOn
4440, 42, 43mp2an 655 . . . . . 6 t TopOn
4544a1i 11 . . . . 5 t TopOn
4645, 5cnmpt1st 17702 . . . . . 6 t t
4711iihalf1cn 18959 . . . . . . 7 t
4847a1i 11 . . . . . 6 t
49 oveq2 6091 . . . . . 6
5045, 5, 46, 45, 48, 49cnmpt21 17705 . . . . 5 t
5145, 5, 50, 1cnmpt21f 17706 . . . 4 t
52 iccssre 10994 . . . . . . . 8
5318, 16, 52mp2an 655 . . . . . . 7
54 resttopon 17227 . . . . . . 7 TopOn t TopOn
5540, 53, 54mp2an 655 . . . . . 6 t TopOn
5655a1i 11 . . . . 5 t TopOn
5756, 5cnmpt1st 17702 . . . . . 6 t t
5812iihalf2cn 18961 . . . . . . 7 t
5958a1i 11 . . . . . 6 t
6049oveq1d 6098 . . . . . 6
6156, 5, 57, 56, 59, 60cnmpt21 17705 . . . . 5 t
6256, 5, 61, 2cnmpt21f 17706 . . . 4 t
6310, 11, 12, 13, 15, 17, 25, 5, 39, 51, 62cnmpt2pc 18955 . . 3
64 breq1 4217 . . . . 5
65 oveq2 6091 . . . . . 6
6665fveq2d 5734 . . . . 5
6765oveq1d 6098 . . . . . 6
6867fveq2d 5734 . . . . 5
6964, 66, 68ifbieq12d 3763 . . . 4