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 𝐽 )