Definition df-phtpc

Description: Define the function which takes a topology and returns the path homotopy relation on that topology. Definition of Hatcher p. 25. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 7-Jun-2014)

	Ref	Expression
Assertion	df-phtpc	⊢ ≃ph = ( 𝑥 ∈ Top ↦ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ ( II Cn 𝑥 ) ∧ ( 𝑓 ( PHtpy ‘ 𝑥 ) 𝑔 ) ≠ ∅ ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cphtpc	⊢ ≃ph
1		vx	⊢ 𝑥
2		ctop	⊢ Top
3		vf	⊢ 𝑓
4		vg	⊢ 𝑔
5	3	cv	⊢ 𝑓
6	4	cv	⊢ 𝑔
7	5 6	cpr	⊢ { 𝑓 , 𝑔 }
8		cii	⊢ II
9		ccn	⊢ Cn
10	1	cv	⊢ 𝑥
11	8 10 9	co	⊢ ( II Cn 𝑥 )
12	7 11	wss	⊢ { 𝑓 , 𝑔 } ⊆ ( II Cn 𝑥 )
13		cphtpy	⊢ PHtpy
14	10 13	cfv	⊢ ( PHtpy ‘ 𝑥 )
15	5 6 14	co	⊢ ( 𝑓 ( PHtpy ‘ 𝑥 ) 𝑔 )
16		c0	⊢ ∅
17	15 16	wne	⊢ ( 𝑓 ( PHtpy ‘ 𝑥 ) 𝑔 ) ≠ ∅
18	12 17	wa	⊢ ( { 𝑓 , 𝑔 } ⊆ ( II Cn 𝑥 ) ∧ ( 𝑓 ( PHtpy ‘ 𝑥 ) 𝑔 ) ≠ ∅ )
19	18 3 4	copab	⊢ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ ( II Cn 𝑥 ) ∧ ( 𝑓 ( PHtpy ‘ 𝑥 ) 𝑔 ) ≠ ∅ ) }
20	1 2 19	cmpt	⊢ ( 𝑥 ∈ Top ↦ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ ( II Cn 𝑥 ) ∧ ( 𝑓 ( PHtpy ‘ 𝑥 ) 𝑔 ) ≠ ∅ ) } )
21	0 20	wceq	⊢ ≃ph = ( 𝑥 ∈ Top ↦ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ ( II Cn 𝑥 ) ∧ ( 𝑓 ( PHtpy ‘ 𝑥 ) 𝑔 ) ≠ ∅ ) } )