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 ( ≃ph ‘ 𝐽 ) Er ( II Cn 𝐽 )

Proof

Step Hyp Ref Expression
1 phtpcrel ⊢ Rel ( ≃ph ‘ 𝐽 )
2 isphtpc ⊢ ( 𝑥 ( ≃ph ‘ 𝐽 ) 𝑦 ↔ ( 𝑥 ∈ ( II Cn 𝐽 ) ∧ 𝑦 ∈ ( II Cn 𝐽 ) ∧ ( 𝑥 ( PHtpy ‘ 𝐽 ) 𝑦 ) ≠ ∅ ) )
3 2 simp2bi ⊢ ( 𝑥 ( ≃ph ‘ 𝐽 ) 𝑦 → 𝑦 ∈ ( II Cn 𝐽 ) )
4 2 simp1bi ⊢ ( 𝑥 ( ≃ph ‘ 𝐽 ) 𝑦 → 𝑥 ∈ ( II Cn 𝐽 ) )
5 2 simp3bi ⊢ ( 𝑥 ( ≃ph ‘ 𝐽 ) 𝑦 → ( 𝑥 ( PHtpy ‘ 𝐽 ) 𝑦 ) ≠ ∅ )
6 n0 ⊢ ( ( 𝑥 ( PHtpy ‘ 𝐽 ) 𝑦 ) ≠ ∅ ↔ ∃ 𝑓 𝑓 ∈ ( 𝑥 ( PHtpy ‘ 𝐽 ) 𝑦 ) )
7 5 6 sylib ⊢ ( 𝑥 ( ≃ph ‘ 𝐽 ) 𝑦 → ∃ 𝑓 𝑓 ∈ ( 𝑥 ( PHtpy ‘ 𝐽 ) 𝑦 ) )
8 4 adantr ⊢ ( ( 𝑥 ( ≃ph ‘ 𝐽 ) 𝑦 ∧ 𝑓 ∈ ( 𝑥 ( PHtpy ‘ 𝐽 ) 𝑦 ) ) → 𝑥 ∈ ( II Cn 𝐽 ) )
9 3 adantr ⊢ ( ( 𝑥 ( ≃ph ‘ 𝐽 ) 𝑦 ∧ 𝑓 ∈ ( 𝑥 ( PHtpy ‘ 𝐽 ) 𝑦 ) ) → 𝑦 ∈ ( II Cn 𝐽 ) )
10 eqid ⊢ ( 𝑢 ∈ ( 0 [,] 1 ) , 𝑣 ∈ ( 0 [,] 1 ) ↦ ( 𝑢 𝑓 ( 1 − 𝑣 ) ) ) = ( 𝑢 ∈ ( 0 [,] 1 ) , 𝑣 ∈ ( 0 [,] 1 ) ↦ ( 𝑢 𝑓 ( 1 − 𝑣 ) ) )
11 simpr ⊢ ( ( 𝑥 ( ≃ph ‘ 𝐽 ) 𝑦 ∧ 𝑓 ∈ ( 𝑥 ( PHtpy ‘ 𝐽 ) 𝑦 ) ) → 𝑓 ∈ ( 𝑥 ( PHtpy ‘ 𝐽 ) 𝑦 ) )
12 8 9 10 11 phtpycom ⊢ ( ( 𝑥 ( ≃ph ‘ 𝐽 ) 𝑦 ∧ 𝑓 ∈ ( 𝑥 ( PHtpy ‘ 𝐽 ) 𝑦 ) ) → ( 𝑢 ∈ ( 0 [,] 1 ) , 𝑣 ∈ ( 0 [,] 1 ) ↦ ( 𝑢 𝑓 ( 1 − 𝑣 ) ) ) ∈ ( 𝑦 ( PHtpy ‘ 𝐽 ) 𝑥 ) )
13 12 ne0d ⊢ ( ( 𝑥 ( ≃ph ‘ 𝐽 ) 𝑦 ∧ 𝑓 ∈ ( 𝑥 ( PHtpy ‘ 𝐽 ) 𝑦 ) ) → ( 𝑦 ( PHtpy ‘ 𝐽 ) 𝑥 ) ≠ ∅ )
14 7 13 exlimddv ⊢ ( 𝑥 ( ≃ph ‘ 𝐽 ) 𝑦 → ( 𝑦 ( PHtpy ‘ 𝐽 ) 𝑥 ) ≠ ∅ )
15 isphtpc ⊢ ( 𝑦 ( ≃ph ‘ 𝐽 ) 𝑥 ↔ ( 𝑦 ∈ ( II Cn 𝐽 ) ∧ 𝑥 ∈ ( II Cn 𝐽 ) ∧ ( 𝑦 ( PHtpy ‘ 𝐽 ) 𝑥 ) ≠ ∅ ) )
16 3 4 14 15 syl3anbrc ⊢ ( 𝑥 ( ≃ph ‘ 𝐽 ) 𝑦 → 𝑦 ( ≃ph ‘ 𝐽 ) 𝑥 )
17 4 adantr ⊢ ( ( 𝑥 ( ≃ph ‘ 𝐽 ) 𝑦 ∧ 𝑦 ( ≃ph ‘ 𝐽 ) 𝑧 ) → 𝑥 ∈ ( II Cn 𝐽 ) )
18 simpr ⊢ ( ( 𝑥 ( ≃ph ‘ 𝐽 ) 𝑦 ∧ 𝑦 ( ≃ph ‘ 𝐽 ) 𝑧 ) → 𝑦 ( ≃ph ‘ 𝐽 ) 𝑧 )
19 isphtpc ⊢ ( 𝑦 ( ≃ph ‘ 𝐽 ) 𝑧 ↔ ( 𝑦 ∈ ( II Cn 𝐽 ) ∧ 𝑧 ∈ ( II Cn 𝐽 ) ∧ ( 𝑦 ( PHtpy ‘ 𝐽 ) 𝑧 ) ≠ ∅ ) )
20 18 19 sylib ⊢ ( ( 𝑥 ( ≃ph ‘ 𝐽 ) 𝑦 ∧ 𝑦 ( ≃ph ‘ 𝐽 ) 𝑧 ) → ( 𝑦 ∈ ( II Cn 𝐽 ) ∧ 𝑧 ∈ ( II Cn 𝐽 ) ∧ ( 𝑦 ( PHtpy ‘ 𝐽 ) 𝑧 ) ≠ ∅ ) )
21 20 simp2d ⊢ ( ( 𝑥 ( ≃ph ‘ 𝐽 ) 𝑦 ∧ 𝑦 ( ≃ph ‘ 𝐽 ) 𝑧 ) → 𝑧 ∈ ( II Cn 𝐽 ) )
22 5 adantr ⊢ ( ( 𝑥 ( ≃ph ‘ 𝐽 ) 𝑦 ∧ 𝑦 ( ≃ph ‘ 𝐽 ) 𝑧 ) → ( 𝑥 ( PHtpy ‘ 𝐽 ) 𝑦 ) ≠ ∅ )
23 22 6 sylib ⊢ ( ( 𝑥 ( ≃ph ‘ 𝐽 ) 𝑦 ∧ 𝑦 ( ≃ph ‘ 𝐽 ) 𝑧 ) → ∃ 𝑓 𝑓 ∈ ( 𝑥 ( PHtpy ‘ 𝐽 ) 𝑦 ) )
24 20 simp3d ⊢ ( ( 𝑥 ( ≃ph ‘ 𝐽 ) 𝑦 ∧ 𝑦 ( ≃ph ‘ 𝐽 ) 𝑧 ) → ( 𝑦 ( PHtpy ‘ 𝐽 ) 𝑧 ) ≠ ∅ )
25 n0 ⊢ ( ( 𝑦 ( PHtpy ‘ 𝐽 ) 𝑧 ) ≠ ∅ ↔ ∃ 𝑔 𝑔 ∈ ( 𝑦 ( PHtpy ‘ 𝐽 ) 𝑧 ) )
26 24 25 sylib ⊢ ( ( 𝑥 ( ≃ph ‘ 𝐽 ) 𝑦 ∧ 𝑦 ( ≃ph ‘ 𝐽 ) 𝑧 ) → ∃ 𝑔 𝑔 ∈ ( 𝑦 ( PHtpy ‘ 𝐽 ) 𝑧 ) )
27 exdistrv ⊢ ( ∃ 𝑓 ∃ 𝑔 ( 𝑓 ∈ ( 𝑥 ( PHtpy ‘ 𝐽 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( PHtpy ‘ 𝐽 ) 𝑧 ) ) ↔ ( ∃ 𝑓 𝑓 ∈ ( 𝑥 ( PHtpy ‘ 𝐽 ) 𝑦 ) ∧ ∃ 𝑔 𝑔 ∈ ( 𝑦 ( PHtpy ‘ 𝐽 ) 𝑧 ) ) )
28 23 26 27 sylanbrc ⊢ ( ( 𝑥 ( ≃ph ‘ 𝐽 ) 𝑦 ∧ 𝑦 ( ≃ph ‘ 𝐽 ) 𝑧 ) → ∃ 𝑓 ∃ 𝑔 ( 𝑓 ∈ ( 𝑥 ( PHtpy ‘ 𝐽 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( PHtpy ‘ 𝐽 ) 𝑧 ) ) )
29 eqid ⊢ ( 𝑢 ∈ ( 0 [,] 1 ) , 𝑣 ∈ ( 0 [,] 1 ) ↦ if ( 𝑣 ≤ ( 1 / 2 ) , ( 𝑢 𝑓 ( 2 · 𝑣 ) ) , ( 𝑢 𝑔 ( ( 2 · 𝑣 ) − 1 ) ) ) ) = ( 𝑢 ∈ ( 0 [,] 1 ) , 𝑣 ∈ ( 0 [,] 1 ) ↦ if ( 𝑣 ≤ ( 1 / 2 ) , ( 𝑢 𝑓 ( 2 · 𝑣 ) ) , ( 𝑢 𝑔 ( ( 2 · 𝑣 ) − 1 ) ) ) )
30 17 adantr ⊢ ( ( ( 𝑥 ( ≃ph ‘ 𝐽 ) 𝑦 ∧ 𝑦 ( ≃ph ‘ 𝐽 ) 𝑧 ) ∧ ( 𝑓 ∈ ( 𝑥 ( PHtpy ‘ 𝐽 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( PHtpy ‘ 𝐽 ) 𝑧 ) ) ) → 𝑥 ∈ ( II Cn 𝐽 ) )
31 20 simp1d ⊢ ( ( 𝑥 ( ≃ph ‘ 𝐽 ) 𝑦 ∧ 𝑦 ( ≃ph ‘ 𝐽 ) 𝑧 ) → 𝑦 ∈ ( II Cn 𝐽 ) )
32 31 adantr ⊢ ( ( ( 𝑥 ( ≃ph ‘ 𝐽 ) 𝑦 ∧ 𝑦 ( ≃ph ‘ 𝐽 ) 𝑧 ) ∧ ( 𝑓 ∈ ( 𝑥 ( PHtpy ‘ 𝐽 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( PHtpy ‘ 𝐽 ) 𝑧 ) ) ) → 𝑦 ∈ ( II Cn 𝐽 ) )
33 21 adantr ⊢ ( ( ( 𝑥 ( ≃ph ‘ 𝐽 ) 𝑦 ∧ 𝑦 ( ≃ph ‘ 𝐽 ) 𝑧 ) ∧ ( 𝑓 ∈ ( 𝑥 ( PHtpy ‘ 𝐽 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( PHtpy ‘ 𝐽 ) 𝑧 ) ) ) → 𝑧 ∈ ( II Cn 𝐽 ) )
34 simprl ⊢ ( ( ( 𝑥 ( ≃ph ‘ 𝐽 ) 𝑦 ∧ 𝑦 ( ≃ph ‘ 𝐽 ) 𝑧 ) ∧ ( 𝑓 ∈ ( 𝑥 ( PHtpy ‘ 𝐽 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( PHtpy ‘ 𝐽 ) 𝑧 ) ) ) → 𝑓 ∈ ( 𝑥 ( PHtpy ‘ 𝐽 ) 𝑦 ) )
35 simprr ⊢ ( ( ( 𝑥 ( ≃ph ‘ 𝐽 ) 𝑦 ∧ 𝑦 ( ≃ph ‘ 𝐽 ) 𝑧 ) ∧ ( 𝑓 ∈ ( 𝑥 ( PHtpy ‘ 𝐽 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( PHtpy ‘ 𝐽 ) 𝑧 ) ) ) → 𝑔 ∈ ( 𝑦 ( PHtpy ‘ 𝐽 ) 𝑧 ) )
36 29 30 32 33 34 35 phtpycc ⊢ ( ( ( 𝑥 ( ≃ph ‘ 𝐽 ) 𝑦 ∧ 𝑦 ( ≃ph ‘ 𝐽 ) 𝑧 ) ∧ ( 𝑓 ∈ ( 𝑥 ( PHtpy ‘ 𝐽 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( PHtpy ‘ 𝐽 ) 𝑧 ) ) ) → ( 𝑢 ∈ ( 0 [,] 1 ) , 𝑣 ∈ ( 0 [,] 1 ) ↦ if ( 𝑣 ≤ ( 1 / 2 ) , ( 𝑢 𝑓 ( 2 · 𝑣 ) ) , ( 𝑢 𝑔 ( ( 2 · 𝑣 ) − 1 ) ) ) ) ∈ ( 𝑥 ( PHtpy ‘ 𝐽 ) 𝑧 ) )
37 36 ne0d ⊢ ( ( ( 𝑥 ( ≃ph ‘ 𝐽 ) 𝑦 ∧ 𝑦 ( ≃ph ‘ 𝐽 ) 𝑧 ) ∧ ( 𝑓 ∈ ( 𝑥 ( PHtpy ‘ 𝐽 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( PHtpy ‘ 𝐽 ) 𝑧 ) ) ) → ( 𝑥 ( PHtpy ‘ 𝐽 ) 𝑧 ) ≠ ∅ )
38 37 ex ⊢ ( ( 𝑥 ( ≃ph ‘ 𝐽 ) 𝑦 ∧ 𝑦 ( ≃ph ‘ 𝐽 ) 𝑧 ) → ( ( 𝑓 ∈ ( 𝑥 ( PHtpy ‘ 𝐽 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( PHtpy ‘ 𝐽 ) 𝑧 ) ) → ( 𝑥 ( PHtpy ‘ 𝐽 ) 𝑧 ) ≠ ∅ ) )
39 38 exlimdvv ⊢ ( ( 𝑥 ( ≃ph ‘ 𝐽 ) 𝑦 ∧ 𝑦 ( ≃ph ‘ 𝐽 ) 𝑧 ) → ( ∃ 𝑓 ∃ 𝑔 ( 𝑓 ∈ ( 𝑥 ( PHtpy ‘ 𝐽 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( PHtpy ‘ 𝐽 ) 𝑧 ) ) → ( 𝑥 ( PHtpy ‘ 𝐽 ) 𝑧 ) ≠ ∅ ) )
40 28 39 mpd ⊢ ( ( 𝑥 ( ≃ph ‘ 𝐽 ) 𝑦 ∧ 𝑦 ( ≃ph ‘ 𝐽 ) 𝑧 ) → ( 𝑥 ( PHtpy ‘ 𝐽 ) 𝑧 ) ≠ ∅ )
41 isphtpc ⊢ ( 𝑥 ( ≃ph ‘ 𝐽 ) 𝑧 ↔ ( 𝑥 ∈ ( II Cn 𝐽 ) ∧ 𝑧 ∈ ( II Cn 𝐽 ) ∧ ( 𝑥 ( PHtpy ‘ 𝐽 ) 𝑧 ) ≠ ∅ ) )
42 17 21 40 41 syl3anbrc ⊢ ( ( 𝑥 ( ≃ph ‘ 𝐽 ) 𝑦 ∧ 𝑦 ( ≃ph ‘ 𝐽 ) 𝑧 ) → 𝑥 ( ≃ph ‘ 𝐽 ) 𝑧 )
43 eqid ⊢ ( 𝑦 ∈ ( 0 [,] 1 ) , 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 ‘ 𝑦 ) ) = ( 𝑦 ∈ ( 0 [,] 1 ) , 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 ‘ 𝑦 ) )
44 id ⊢ ( 𝑥 ∈ ( II Cn 𝐽 ) → 𝑥 ∈ ( II Cn 𝐽 ) )
45 43 44 phtpyid ⊢ ( 𝑥 ∈ ( II Cn 𝐽 ) → ( 𝑦 ∈ ( 0 [,] 1 ) , 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 ‘ 𝑦 ) ) ∈ ( 𝑥 ( PHtpy ‘ 𝐽 ) 𝑥 ) )
46 45 ne0d ⊢ ( 𝑥 ∈ ( II Cn 𝐽 ) → ( 𝑥 ( PHtpy ‘ 𝐽 ) 𝑥 ) ≠ ∅ )
47 46 ancli ⊢ ( 𝑥 ∈ ( II Cn 𝐽 ) → ( 𝑥 ∈ ( II Cn 𝐽 ) ∧ ( 𝑥 ( PHtpy ‘ 𝐽 ) 𝑥 ) ≠ ∅ ) )
48 47 pm4.71ri ⊢ ( 𝑥 ∈ ( II Cn 𝐽 ) ↔ ( ( 𝑥 ∈ ( II Cn 𝐽 ) ∧ ( 𝑥 ( PHtpy ‘ 𝐽 ) 𝑥 ) ≠ ∅ ) ∧ 𝑥 ∈ ( II Cn 𝐽 ) ) )
49 df-3an ⊢ ( ( 𝑥 ∈ ( II Cn 𝐽 ) ∧ ( 𝑥 ( PHtpy ‘ 𝐽 ) 𝑥 ) ≠ ∅ ∧ 𝑥 ∈ ( II Cn 𝐽 ) ) ↔ ( ( 𝑥 ∈ ( II Cn 𝐽 ) ∧ ( 𝑥 ( PHtpy ‘ 𝐽 ) 𝑥 ) ≠ ∅ ) ∧ 𝑥 ∈ ( II Cn 𝐽 ) ) )
50 3ancomb ⊢ ( ( 𝑥 ∈ ( II Cn 𝐽 ) ∧ ( 𝑥 ( PHtpy ‘ 𝐽 ) 𝑥 ) ≠ ∅ ∧ 𝑥 ∈ ( II Cn 𝐽 ) ) ↔ ( 𝑥 ∈ ( II Cn 𝐽 ) ∧ 𝑥 ∈ ( II Cn 𝐽 ) ∧ ( 𝑥 ( PHtpy ‘ 𝐽 ) 𝑥 ) ≠ ∅ ) )
51 48 49 50 3bitr2i ⊢ ( 𝑥 ∈ ( II Cn 𝐽 ) ↔ ( 𝑥 ∈ ( II Cn 𝐽 ) ∧ 𝑥 ∈ ( II Cn 𝐽 ) ∧ ( 𝑥 ( PHtpy ‘ 𝐽 ) 𝑥 ) ≠ ∅ ) )
52 isphtpc ⊢ ( 𝑥 ( ≃ph ‘ 𝐽 ) 𝑥 ↔ ( 𝑥 ∈ ( II Cn 𝐽 ) ∧ 𝑥 ∈ ( II Cn 𝐽 ) ∧ ( 𝑥 ( PHtpy ‘ 𝐽 ) 𝑥 ) ≠ ∅ ) )
53 51 52 bitr4i ⊢ ( 𝑥 ∈ ( II Cn 𝐽 ) ↔ 𝑥 ( ≃ph ‘ 𝐽 ) 𝑥 )
54 1 16 42 53 iseri ⊢ ( ≃ph ‘ 𝐽 ) Er ( II Cn 𝐽 )