# Metamath Proof Explorer

## Theorem phtpcer

Description: Path homotopy is an equivalence relation. Proposition 1.2 of Hatcher p. 26. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 6-Jul-2015) (Proof shortened by AV, 1-May-2021)

Ref Expression
Assertion phtpcer ${⊢}{\simeq }_{\mathrm{ph}}\left({J}\right)\mathrm{Er}\left(\mathrm{II}\mathrm{Cn}{J}\right)$

### Proof

Step Hyp Ref Expression
1 phtpcrel ${⊢}\mathrm{Rel}{\simeq }_{\mathrm{ph}}\left({J}\right)$
2 isphtpc ${⊢}{x}{\simeq }_{\mathrm{ph}}\left({J}\right){y}↔\left({x}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)\wedge {y}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)\wedge {x}\mathrm{PHtpy}\left({J}\right){y}\ne \varnothing \right)$
3 2 simp2bi ${⊢}{x}{\simeq }_{\mathrm{ph}}\left({J}\right){y}\to {y}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)$
4 2 simp1bi ${⊢}{x}{\simeq }_{\mathrm{ph}}\left({J}\right){y}\to {x}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)$
5 2 simp3bi ${⊢}{x}{\simeq }_{\mathrm{ph}}\left({J}\right){y}\to {x}\mathrm{PHtpy}\left({J}\right){y}\ne \varnothing$
6 n0 ${⊢}{x}\mathrm{PHtpy}\left({J}\right){y}\ne \varnothing ↔\exists {f}\phantom{\rule{.4em}{0ex}}{f}\in \left({x}\mathrm{PHtpy}\left({J}\right){y}\right)$
7 5 6 sylib ${⊢}{x}{\simeq }_{\mathrm{ph}}\left({J}\right){y}\to \exists {f}\phantom{\rule{.4em}{0ex}}{f}\in \left({x}\mathrm{PHtpy}\left({J}\right){y}\right)$
8 4 adantr ${⊢}\left({x}{\simeq }_{\mathrm{ph}}\left({J}\right){y}\wedge {f}\in \left({x}\mathrm{PHtpy}\left({J}\right){y}\right)\right)\to {x}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)$
9 3 adantr ${⊢}\left({x}{\simeq }_{\mathrm{ph}}\left({J}\right){y}\wedge {f}\in \left({x}\mathrm{PHtpy}\left({J}\right){y}\right)\right)\to {y}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)$
10 eqid ${⊢}\left({u}\in \left[0,1\right],{v}\in \left[0,1\right]⟼{u}{f}\left(1-{v}\right)\right)=\left({u}\in \left[0,1\right],{v}\in \left[0,1\right]⟼{u}{f}\left(1-{v}\right)\right)$
11 simpr ${⊢}\left({x}{\simeq }_{\mathrm{ph}}\left({J}\right){y}\wedge {f}\in \left({x}\mathrm{PHtpy}\left({J}\right){y}\right)\right)\to {f}\in \left({x}\mathrm{PHtpy}\left({J}\right){y}\right)$
12 8 9 10 11 phtpycom ${⊢}\left({x}{\simeq }_{\mathrm{ph}}\left({J}\right){y}\wedge {f}\in \left({x}\mathrm{PHtpy}\left({J}\right){y}\right)\right)\to \left({u}\in \left[0,1\right],{v}\in \left[0,1\right]⟼{u}{f}\left(1-{v}\right)\right)\in \left({y}\mathrm{PHtpy}\left({J}\right){x}\right)$
13 12 ne0d ${⊢}\left({x}{\simeq }_{\mathrm{ph}}\left({J}\right){y}\wedge {f}\in \left({x}\mathrm{PHtpy}\left({J}\right){y}\right)\right)\to {y}\mathrm{PHtpy}\left({J}\right){x}\ne \varnothing$
14 7 13 exlimddv ${⊢}{x}{\simeq }_{\mathrm{ph}}\left({J}\right){y}\to {y}\mathrm{PHtpy}\left({J}\right){x}\ne \varnothing$
15 isphtpc ${⊢}{y}{\simeq }_{\mathrm{ph}}\left({J}\right){x}↔\left({y}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)\wedge {x}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)\wedge {y}\mathrm{PHtpy}\left({J}\right){x}\ne \varnothing \right)$
16 3 4 14 15 syl3anbrc ${⊢}{x}{\simeq }_{\mathrm{ph}}\left({J}\right){y}\to {y}{\simeq }_{\mathrm{ph}}\left({J}\right){x}$
17 4 adantr ${⊢}\left({x}{\simeq }_{\mathrm{ph}}\left({J}\right){y}\wedge {y}{\simeq }_{\mathrm{ph}}\left({J}\right){z}\right)\to {x}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)$
18 simpr ${⊢}\left({x}{\simeq }_{\mathrm{ph}}\left({J}\right){y}\wedge {y}{\simeq }_{\mathrm{ph}}\left({J}\right){z}\right)\to {y}{\simeq }_{\mathrm{ph}}\left({J}\right){z}$
19 isphtpc ${⊢}{y}{\simeq }_{\mathrm{ph}}\left({J}\right){z}↔\left({y}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)\wedge {z}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)\wedge {y}\mathrm{PHtpy}\left({J}\right){z}\ne \varnothing \right)$
20 18 19 sylib ${⊢}\left({x}{\simeq }_{\mathrm{ph}}\left({J}\right){y}\wedge {y}{\simeq }_{\mathrm{ph}}\left({J}\right){z}\right)\to \left({y}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)\wedge {z}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)\wedge {y}\mathrm{PHtpy}\left({J}\right){z}\ne \varnothing \right)$
21 20 simp2d ${⊢}\left({x}{\simeq }_{\mathrm{ph}}\left({J}\right){y}\wedge {y}{\simeq }_{\mathrm{ph}}\left({J}\right){z}\right)\to {z}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)$
22 5 adantr ${⊢}\left({x}{\simeq }_{\mathrm{ph}}\left({J}\right){y}\wedge {y}{\simeq }_{\mathrm{ph}}\left({J}\right){z}\right)\to {x}\mathrm{PHtpy}\left({J}\right){y}\ne \varnothing$
23 22 6 sylib ${⊢}\left({x}{\simeq }_{\mathrm{ph}}\left({J}\right){y}\wedge {y}{\simeq }_{\mathrm{ph}}\left({J}\right){z}\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}{f}\in \left({x}\mathrm{PHtpy}\left({J}\right){y}\right)$
24 20 simp3d ${⊢}\left({x}{\simeq }_{\mathrm{ph}}\left({J}\right){y}\wedge {y}{\simeq }_{\mathrm{ph}}\left({J}\right){z}\right)\to {y}\mathrm{PHtpy}\left({J}\right){z}\ne \varnothing$
25 n0 ${⊢}{y}\mathrm{PHtpy}\left({J}\right){z}\ne \varnothing ↔\exists {g}\phantom{\rule{.4em}{0ex}}{g}\in \left({y}\mathrm{PHtpy}\left({J}\right){z}\right)$
26 24 25 sylib ${⊢}\left({x}{\simeq }_{\mathrm{ph}}\left({J}\right){y}\wedge {y}{\simeq }_{\mathrm{ph}}\left({J}\right){z}\right)\to \exists {g}\phantom{\rule{.4em}{0ex}}{g}\in \left({y}\mathrm{PHtpy}\left({J}\right){z}\right)$
27 exdistrv ${⊢}\exists {f}\phantom{\rule{.4em}{0ex}}\exists {g}\phantom{\rule{.4em}{0ex}}\left({f}\in \left({x}\mathrm{PHtpy}\left({J}\right){y}\right)\wedge {g}\in \left({y}\mathrm{PHtpy}\left({J}\right){z}\right)\right)↔\left(\exists {f}\phantom{\rule{.4em}{0ex}}{f}\in \left({x}\mathrm{PHtpy}\left({J}\right){y}\right)\wedge \exists {g}\phantom{\rule{.4em}{0ex}}{g}\in \left({y}\mathrm{PHtpy}\left({J}\right){z}\right)\right)$
28 23 26 27 sylanbrc ${⊢}\left({x}{\simeq }_{\mathrm{ph}}\left({J}\right){y}\wedge {y}{\simeq }_{\mathrm{ph}}\left({J}\right){z}\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}\exists {g}\phantom{\rule{.4em}{0ex}}\left({f}\in \left({x}\mathrm{PHtpy}\left({J}\right){y}\right)\wedge {g}\in \left({y}\mathrm{PHtpy}\left({J}\right){z}\right)\right)$
29 eqid ${⊢}\left({u}\in \left[0,1\right],{v}\in \left[0,1\right]⟼if\left({v}\le \frac{1}{2},{u}{f}2{v},{u}{g}\left(2{v}-1\right)\right)\right)=\left({u}\in \left[0,1\right],{v}\in \left[0,1\right]⟼if\left({v}\le \frac{1}{2},{u}{f}2{v},{u}{g}\left(2{v}-1\right)\right)\right)$
30 17 adantr ${⊢}\left(\left({x}{\simeq }_{\mathrm{ph}}\left({J}\right){y}\wedge {y}{\simeq }_{\mathrm{ph}}\left({J}\right){z}\right)\wedge \left({f}\in \left({x}\mathrm{PHtpy}\left({J}\right){y}\right)\wedge {g}\in \left({y}\mathrm{PHtpy}\left({J}\right){z}\right)\right)\right)\to {x}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)$
31 20 simp1d ${⊢}\left({x}{\simeq }_{\mathrm{ph}}\left({J}\right){y}\wedge {y}{\simeq }_{\mathrm{ph}}\left({J}\right){z}\right)\to {y}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)$
32 31 adantr ${⊢}\left(\left({x}{\simeq }_{\mathrm{ph}}\left({J}\right){y}\wedge {y}{\simeq }_{\mathrm{ph}}\left({J}\right){z}\right)\wedge \left({f}\in \left({x}\mathrm{PHtpy}\left({J}\right){y}\right)\wedge {g}\in \left({y}\mathrm{PHtpy}\left({J}\right){z}\right)\right)\right)\to {y}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)$
33 21 adantr ${⊢}\left(\left({x}{\simeq }_{\mathrm{ph}}\left({J}\right){y}\wedge {y}{\simeq }_{\mathrm{ph}}\left({J}\right){z}\right)\wedge \left({f}\in \left({x}\mathrm{PHtpy}\left({J}\right){y}\right)\wedge {g}\in \left({y}\mathrm{PHtpy}\left({J}\right){z}\right)\right)\right)\to {z}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)$
34 simprl ${⊢}\left(\left({x}{\simeq }_{\mathrm{ph}}\left({J}\right){y}\wedge {y}{\simeq }_{\mathrm{ph}}\left({J}\right){z}\right)\wedge \left({f}\in \left({x}\mathrm{PHtpy}\left({J}\right){y}\right)\wedge {g}\in \left({y}\mathrm{PHtpy}\left({J}\right){z}\right)\right)\right)\to {f}\in \left({x}\mathrm{PHtpy}\left({J}\right){y}\right)$
35 simprr ${⊢}\left(\left({x}{\simeq }_{\mathrm{ph}}\left({J}\right){y}\wedge {y}{\simeq }_{\mathrm{ph}}\left({J}\right){z}\right)\wedge \left({f}\in \left({x}\mathrm{PHtpy}\left({J}\right){y}\right)\wedge {g}\in \left({y}\mathrm{PHtpy}\left({J}\right){z}\right)\right)\right)\to {g}\in \left({y}\mathrm{PHtpy}\left({J}\right){z}\right)$
36 29 30 32 33 34 35 phtpycc ${⊢}\left(\left({x}{\simeq }_{\mathrm{ph}}\left({J}\right){y}\wedge {y}{\simeq }_{\mathrm{ph}}\left({J}\right){z}\right)\wedge \left({f}\in \left({x}\mathrm{PHtpy}\left({J}\right){y}\right)\wedge {g}\in \left({y}\mathrm{PHtpy}\left({J}\right){z}\right)\right)\right)\to \left({u}\in \left[0,1\right],{v}\in \left[0,1\right]⟼if\left({v}\le \frac{1}{2},{u}{f}2{v},{u}{g}\left(2{v}-1\right)\right)\right)\in \left({x}\mathrm{PHtpy}\left({J}\right){z}\right)$
37 36 ne0d ${⊢}\left(\left({x}{\simeq }_{\mathrm{ph}}\left({J}\right){y}\wedge {y}{\simeq }_{\mathrm{ph}}\left({J}\right){z}\right)\wedge \left({f}\in \left({x}\mathrm{PHtpy}\left({J}\right){y}\right)\wedge {g}\in \left({y}\mathrm{PHtpy}\left({J}\right){z}\right)\right)\right)\to {x}\mathrm{PHtpy}\left({J}\right){z}\ne \varnothing$
38 37 ex ${⊢}\left({x}{\simeq }_{\mathrm{ph}}\left({J}\right){y}\wedge {y}{\simeq }_{\mathrm{ph}}\left({J}\right){z}\right)\to \left(\left({f}\in \left({x}\mathrm{PHtpy}\left({J}\right){y}\right)\wedge {g}\in \left({y}\mathrm{PHtpy}\left({J}\right){z}\right)\right)\to {x}\mathrm{PHtpy}\left({J}\right){z}\ne \varnothing \right)$
39 38 exlimdvv ${⊢}\left({x}{\simeq }_{\mathrm{ph}}\left({J}\right){y}\wedge {y}{\simeq }_{\mathrm{ph}}\left({J}\right){z}\right)\to \left(\exists {f}\phantom{\rule{.4em}{0ex}}\exists {g}\phantom{\rule{.4em}{0ex}}\left({f}\in \left({x}\mathrm{PHtpy}\left({J}\right){y}\right)\wedge {g}\in \left({y}\mathrm{PHtpy}\left({J}\right){z}\right)\right)\to {x}\mathrm{PHtpy}\left({J}\right){z}\ne \varnothing \right)$
40 28 39 mpd ${⊢}\left({x}{\simeq }_{\mathrm{ph}}\left({J}\right){y}\wedge {y}{\simeq }_{\mathrm{ph}}\left({J}\right){z}\right)\to {x}\mathrm{PHtpy}\left({J}\right){z}\ne \varnothing$
41 isphtpc ${⊢}{x}{\simeq }_{\mathrm{ph}}\left({J}\right){z}↔\left({x}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)\wedge {z}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)\wedge {x}\mathrm{PHtpy}\left({J}\right){z}\ne \varnothing \right)$
42 17 21 40 41 syl3anbrc ${⊢}\left({x}{\simeq }_{\mathrm{ph}}\left({J}\right){y}\wedge {y}{\simeq }_{\mathrm{ph}}\left({J}\right){z}\right)\to {x}{\simeq }_{\mathrm{ph}}\left({J}\right){z}$
43 eqid ${⊢}\left({y}\in \left[0,1\right],{z}\in \left[0,1\right]⟼{x}\left({y}\right)\right)=\left({y}\in \left[0,1\right],{z}\in \left[0,1\right]⟼{x}\left({y}\right)\right)$
44 id ${⊢}{x}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)\to {x}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)$
45 43 44 phtpyid ${⊢}{x}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)\to \left({y}\in \left[0,1\right],{z}\in \left[0,1\right]⟼{x}\left({y}\right)\right)\in \left({x}\mathrm{PHtpy}\left({J}\right){x}\right)$
46 45 ne0d ${⊢}{x}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)\to {x}\mathrm{PHtpy}\left({J}\right){x}\ne \varnothing$
47 46 ancli ${⊢}{x}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)\to \left({x}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)\wedge {x}\mathrm{PHtpy}\left({J}\right){x}\ne \varnothing \right)$
48 47 pm4.71ri ${⊢}{x}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)↔\left(\left({x}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)\wedge {x}\mathrm{PHtpy}\left({J}\right){x}\ne \varnothing \right)\wedge {x}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)\right)$
49 df-3an ${⊢}\left({x}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)\wedge {x}\mathrm{PHtpy}\left({J}\right){x}\ne \varnothing \wedge {x}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)\right)↔\left(\left({x}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)\wedge {x}\mathrm{PHtpy}\left({J}\right){x}\ne \varnothing \right)\wedge {x}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)\right)$
50 3ancomb ${⊢}\left({x}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)\wedge {x}\mathrm{PHtpy}\left({J}\right){x}\ne \varnothing \wedge {x}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)\right)↔\left({x}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)\wedge {x}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)\wedge {x}\mathrm{PHtpy}\left({J}\right){x}\ne \varnothing \right)$
51 48 49 50 3bitr2i ${⊢}{x}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)↔\left({x}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)\wedge {x}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)\wedge {x}\mathrm{PHtpy}\left({J}\right){x}\ne \varnothing \right)$
52 isphtpc ${⊢}{x}{\simeq }_{\mathrm{ph}}\left({J}\right){x}↔\left({x}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)\wedge {x}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)\wedge {x}\mathrm{PHtpy}\left({J}\right){x}\ne \varnothing \right)$
53 51 52 bitr4i ${⊢}{x}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)↔{x}{\simeq }_{\mathrm{ph}}\left({J}\right){x}$
54 1 16 42 53 iseri ${⊢}{\simeq }_{\mathrm{ph}}\left({J}\right)\mathrm{Er}\left(\mathrm{II}\mathrm{Cn}{J}\right)$