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

Theorem pcocn 18531
 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 18525 . 2
4 iitopon 18399 . . . 4 TopOn
54a1i 10 . . 3 TopOn
65cnmptid 17371 . . 3
7 0elunit 10770 . . . . 5
87a1i 10 . . . 4
95, 5, 8cnmptc 17372 . . 3
10 eqid 2296 . . . 4
11 eqid 2296 . . . 4 t t
12 eqid 2296 . . . 4 t t
13 dfii2 18402 . . . 4 t
14 0re 8854 . . . . 5
1514a1i 10 . . . 4
16 1re 8853 . . . . 5
1716a1i 10 . . . 4
18 rehalfcl 9954 . . . . . . 7
1916, 18ax-mp 8 . . . . . 6
20 halfgt0 9948 . . . . . . 7
2114, 19, 20ltleii 8957 . . . . . 6
22 halflt1 9949 . . . . . . 7
2319, 16, 22ltleii 8957 . . . . . 6
2414, 16elicc2i 10732 . . . . . 6
2519, 21, 23, 24mpbir3an 1134 . . . . 5
2625a1i 10 . . . 4
27 pcoval2.4 . . . . . 6
2827adantr 451 . . . . 5
29 simprl 732 . . . . . . . 8
3029oveq2d 5890 . . . . . . 7
31 2cn 9832 . . . . . . . 8
32 2ne0 9845 . . . . . . . 8
3331, 32recidi 9507 . . . . . . 7
3430, 33syl6eq 2344 . . . . . 6
3534fveq2d 5545 . . . . 5
3634oveq1d 5889 . . . . . . 7
37 1m1e0 9830 . . . . . . 7
3836, 37syl6eq 2344 . . . . . 6
3938fveq2d 5545 . . . . 5
4028, 35, 393eqtr4d 2338 . . . 4
41 retopon 18288 . . . . . . 7 TopOn
42 iccssre 10747 . . . . . . . 8
4314, 19, 42mp2an 653 . . . . . . 7
44 resttopon 16908 . . . . . . 7 TopOn t TopOn
4541, 43, 44mp2an 653 . . . . . 6 t TopOn
4645a1i 10 . . . . 5 t TopOn
4746, 5cnmpt1st 17378 . . . . . 6 t t
4811iihalf1cn 18446 . . . . . . 7 t
4948a1i 10 . . . . . 6 t
50 oveq2 5882 . . . . . 6
5146, 5, 47, 46, 49, 50cnmpt21 17381 . . . . 5 t
5246, 5, 51, 1cnmpt21f 17382 . . . 4 t
53 iccssre 10747 . . . . . . . 8
5419, 16, 53mp2an 653 . . . . . . 7
55 resttopon 16908 . . . . . . 7 TopOn t TopOn
5641, 54, 55mp2an 653 . . . . . 6 t TopOn
5756a1i 10 . . . . 5 t TopOn
5857, 5cnmpt1st 17378 . . . . . 6 t t
5912iihalf2cn 18448 . . . . . . 7 t
6059a1i 10 . . . . . 6 t
6150oveq1d 5889 . . . . . 6
6257, 5, 58, 57, 60, 61cnmpt21 17381 . . . . 5 t
6357, 5, 62, 2cnmpt21f 17382 . . . 4 t
6410, 11, 12, 13, 15, 17, 26, 5, 40, 52, 63cnmpt2pc 18442 . . 3
65 breq1 4042 . . . . 5
66 oveq2 5882 . . . . . 6
6766fveq2d 5545 . . . . 5
6866oveq1d 5889 . . . . . 6
6968fveq2d 5545 . . . . 5
7065, 67, 69ifbieq12d 3600 . . . 4