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

Theorem pcocn 22060
 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 22054 . 2
4 iitopon 21923 . . . 4 TopOn
54a1i 11 . . 3 TopOn
65cnmptid 20688 . . 3
7 0elunit 11757 . . . . 5
87a1i 11 . . . 4
95, 5, 8cnmptc 20689 . . 3
10 eqid 2453 . . . 4
11 eqid 2453 . . . 4 t t
12 eqid 2453 . . . 4 t t
13 dfii2 21926 . . . 4 t
14 0re 9648 . . . . 5
1514a1i 11 . . . 4
16 1re 9647 . . . . 5
1716a1i 11 . . . 4
18 halfre 10835 . . . . . 6
19 halfgt0 10837 . . . . . . 7
2014, 18, 19ltleii 9762 . . . . . 6
21 halflt1 10838 . . . . . . 7
2218, 16, 21ltleii 9762 . . . . . 6
2314, 16elicc2i 11707 . . . . . 6
2418, 20, 22, 23mpbir3an 1191 . . . . 5
2524a1i 11 . . . 4
26 pcoval2.4 . . . . . 6
2726adantr 467 . . . . 5
28 simprl 765 . . . . . . . 8
2928oveq2d 6311 . . . . . . 7
30 2cn 10687 . . . . . . . 8
31 2ne0 10709 . . . . . . . 8
3230, 31recidi 10345 . . . . . . 7
3329, 32syl6eq 2503 . . . . . 6
3433fveq2d 5874 . . . . 5
3533oveq1d 6310 . . . . . . 7
36 1m1e0 10685 . . . . . . 7
3735, 36syl6eq 2503 . . . . . 6
3837fveq2d 5874 . . . . 5
3927, 34, 383eqtr4d 2497 . . . 4
40 retopon 21796 . . . . . . 7 TopOn
41 iccssre 11723 . . . . . . . 8
4214, 18, 41mp2an 679 . . . . . . 7
43 resttopon 20189 . . . . . . 7 TopOn t TopOn
4440, 42, 43mp2an 679 . . . . . 6 t TopOn
4544a1i 11 . . . . 5 t TopOn
4645, 5cnmpt1st 20695 . . . . . 6 t t
4711iihalf1cn 21972 . . . . . . 7 t
4847a1i 11 . . . . . 6 t
49 oveq2 6303 . . . . . 6
5045, 5, 46, 45, 48, 49cnmpt21 20698 . . . . 5 t
5145, 5, 50, 1cnmpt21f 20699 . . . 4 t
52 iccssre 11723 . . . . . . . 8
5318, 16, 52mp2an 679 . . . . . . 7
54 resttopon 20189 . . . . . . 7 TopOn t TopOn
5540, 53, 54mp2an 679 . . . . . 6 t TopOn
5655a1i 11 . . . . 5 t TopOn
5756, 5cnmpt1st 20695 . . . . . 6 t t
5812iihalf2cn 21974 . . . . . . 7 t
5958a1i 11 . . . . . 6 t
6049oveq1d 6310 . . . . . 6
6156, 5, 57, 56, 59, 60cnmpt21 20698 . . . . 5 t
6256, 5, 61, 2cnmpt21f 20699 . . . 4 t
6310, 11, 12, 13, 15, 17, 25, 5, 39, 51, 62cnmpt2pc 21968 . . 3
64 breq1 4408 . . . . 5
65 oveq2 6303 . . . . . 6
6665fveq2d 5874 . . . . 5
6765oveq1d 6310 . . . . . 6
6867fveq2d 5874 . . . . 5
6964, 66, 68ifbieq12d 3910 . . . 4