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	$$⊢{\simeq }_{\mathrm{ph}}=\left(x\in \mathrm{Top}⟼\left\{⟨f,g⟩|\left(\left\{f,g\right\}\subseteq \mathrm{II}\mathrm{Cn}x\wedge f\mathrm{PHtpy}\left(x\right)g\ne \varnothing \right)\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cphtpc	$$class{\simeq }_{\mathrm{ph}}$$
1		vx	$$setvarx$$
2		ctop	$$class\mathrm{Top}$$
3		vf	$$setvarf$$
4		vg	$$setvarg$$
5	3	cv	$$setvarf$$
6	4	cv	$$setvarg$$
7	5 6	cpr	$$class\left\{f,g\right\}$$
8		cii	$$class\mathrm{II}$$
9		ccn	$$class\mathrm{Cn}$$
10	1	cv	$$setvarx$$
11	8 10 9	co	$$class\left(\mathrm{II}\mathrm{Cn}x\right)$$
12	7 11	wss	$$wff\left\{f,g\right\}\subseteq \mathrm{II}\mathrm{Cn}x$$
13		cphtpy	$$class\mathrm{PHtpy}$$
14	10 13	cfv	$$class\mathrm{PHtpy}\left(x\right)$$
15	5 6 14	co	$$class\left(f\mathrm{PHtpy}\left(x\right)g\right)$$
16		c0	$$class\varnothing$$
17	15 16	wne	$$wfff\mathrm{PHtpy}\left(x\right)g\ne \varnothing$$
18	12 17	wa	$$wff\left(\left\{f,g\right\}\subseteq \mathrm{II}\mathrm{Cn}x\wedge f\mathrm{PHtpy}\left(x\right)g\ne \varnothing \right)$$
19	18 3 4	copab	$$class\left\{⟨f,g⟩|\left(\left\{f,g\right\}\subseteq \mathrm{II}\mathrm{Cn}x\wedge f\mathrm{PHtpy}\left(x\right)g\ne \varnothing \right)\right\}$$
20	1 2 19	cmpt	$$class\left(x\in \mathrm{Top}⟼\left\{⟨f,g⟩|\left(\left\{f,g\right\}\subseteq \mathrm{II}\mathrm{Cn}x\wedge f\mathrm{PHtpy}\left(x\right)g\ne \varnothing \right)\right\}\right)$$
21	0 20	wceq	$$wff{\simeq }_{\mathrm{ph}}=\left(x\in \mathrm{Top}⟼\left\{⟨f,g⟩|\left(\left\{f,g\right\}\subseteq \mathrm{II}\mathrm{Cn}x\wedge f\mathrm{PHtpy}\left(x\right)g\ne \varnothing \right)\right\}\right)$$