isphtpc

Description: The relation "is path homotopic to". (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 5-Sep-2015)

		Ref	Expression
	Assertion	isphtpc	$⊢ F ≃_{ph} (J) G \leftrightarrow (F \in (II Cn J) \land G \in (II Cn J) \land F PHtpy (J) G \neq \emptyset)$

Proof

Step	Hyp	Ref	Expression
1		df-br	$⊢ F ≃_{ph} (J) G \leftrightarrow ⟨F, G⟩ \in ≃_{ph} (J)$
2		df-phtpc	$⊢ ≃_{ph} = (j \in Top ⟼ \{⟨f, g⟩ \| (\{f, g\} \subseteq II Cn j \land f PHtpy (j) g \neq \emptyset)\})$
3	2	mptrcl	$⊢ ⟨F, G⟩ \in ≃_{ph} (J) \to J \in Top$
4	1 3	sylbi	$⊢ F ≃_{ph} (J) G \to J \in Top$
5		cntop2	$⊢ F \in (II Cn J) \to J \in Top$
6	5	3ad2ant1	$⊢ (F \in (II Cn J) \land G \in (II Cn J) \land F PHtpy (J) G \neq \emptyset) \to J \in Top$
7		oveq2	$⊢ j = J \to II Cn j = II Cn J$
8	7	sseq2d	$⊢ j = J \to (\{f, g\} \subseteq II Cn j \leftrightarrow \{f, g\} \subseteq II Cn J)$
9		vex	$⊢ f \in V$
10		vex	$⊢ g \in V$
11	9 10	prss	$⊢ (f \in (II Cn J) \land g \in (II Cn J)) \leftrightarrow \{f, g\} \subseteq II Cn J$
12	8 11	bitr4di	$⊢ j = J \to (\{f, g\} \subseteq II Cn j \leftrightarrow (f \in (II Cn J) \land g \in (II Cn J)))$
13		fveq2	$⊢ j = J \to PHtpy (j) = PHtpy (J)$
14	13	oveqd	$⊢ j = J \to f PHtpy (j) g = f PHtpy (J) g$
15	14	neeq1d	$⊢ j = J \to (f PHtpy (j) g \neq \emptyset \leftrightarrow f PHtpy (J) g \neq \emptyset)$
16	12 15	anbi12d	$⊢ j = J \to ((\{f, g\} \subseteq II Cn j \land f PHtpy (j) g \neq \emptyset) \leftrightarrow ((f \in (II Cn J) \land g \in (II Cn J)) \land f PHtpy (J) g \neq \emptyset))$
17	16	opabbidv	$⊢ j = J \to \{⟨f, g⟩ \| (\{f, g\} \subseteq II Cn j \land f PHtpy (j) g \neq \emptyset)\} = \{⟨f, g⟩ \| ((f \in (II Cn J) \land g \in (II Cn J)) \land f PHtpy (J) g \neq \emptyset)\}$
18		ovex	$⊢ II Cn J \in V$
19	18 18	xpex	$⊢ (II Cn J) \times (II Cn J) \in V$
20		opabssxp	$⊢ \{⟨f, g⟩ \| ((f \in (II Cn J) \land g \in (II Cn J)) \land f PHtpy (J) g \neq \emptyset)\} \subseteq (II Cn J) \times (II Cn J)$
21	19 20	ssexi	$⊢ \{⟨f, g⟩ \| ((f \in (II Cn J) \land g \in (II Cn J)) \land f PHtpy (J) g \neq \emptyset)\} \in V$
22	17 2 21	fvmpt	$⊢ J \in Top \to ≃_{ph} (J) = \{⟨f, g⟩ \| ((f \in (II Cn J) \land g \in (II Cn J)) \land f PHtpy (J) g \neq \emptyset)\}$
23	22	breqd	$⊢ J \in Top \to (F ≃_{ph} (J) G \leftrightarrow F \{⟨f, g⟩ \| ((f \in (II Cn J) \land g \in (II Cn J)) \land f PHtpy (J) g \neq \emptyset)\} G)$
24		oveq12	$⊢ (f = F \land g = G) \to f PHtpy (J) g = F PHtpy (J) G$
25	24	neeq1d	$⊢ (f = F \land g = G) \to (f PHtpy (J) g \neq \emptyset \leftrightarrow F PHtpy (J) G \neq \emptyset)$
26		eqid	$⊢ \{⟨f, g⟩ \| ((f \in (II Cn J) \land g \in (II Cn J)) \land f PHtpy (J) g \neq \emptyset)\} = \{⟨f, g⟩ \| ((f \in (II Cn J) \land g \in (II Cn J)) \land f PHtpy (J) g \neq \emptyset)\}$
27	25 26	brab2a	$⊢ F \{⟨f, g⟩ \| ((f \in (II Cn J) \land g \in (II Cn J)) \land f PHtpy (J) g \neq \emptyset)\} G \leftrightarrow ((F \in (II Cn J) \land G \in (II Cn J)) \land F PHtpy (J) G \neq \emptyset)$
28		df-3an	$⊢ (F \in (II Cn J) \land G \in (II Cn J) \land F PHtpy (J) G \neq \emptyset) \leftrightarrow ((F \in (II Cn J) \land G \in (II Cn J)) \land F PHtpy (J) G \neq \emptyset)$
29	27 28	bitr4i	$⊢ F \{⟨f, g⟩ \| ((f \in (II Cn J) \land g \in (II Cn J)) \land f PHtpy (J) g \neq \emptyset)\} G \leftrightarrow (F \in (II Cn J) \land G \in (II Cn J) \land F PHtpy (J) G \neq \emptyset)$
30	23 29	bitrdi	$⊢ J \in Top \to (F ≃_{ph} (J) G \leftrightarrow (F \in (II Cn J) \land G \in (II Cn J) \land F PHtpy (J) G \neq \emptyset))$
31	4 6 30	pm5.21nii	$⊢ F ≃_{ph} (J) G \leftrightarrow (F \in (II Cn J) \land G \in (II Cn J) \land F PHtpy (J) G \neq \emptyset)$

Metamath Proof Explorer

Theorem isphtpc

Proof