isphtpy

Description: Membership in the class of path homotopies between two continuous functions. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 23-Feb-2015)

	Ref	Expression
Hypotheses	isphtpy.2	$⊢ φ \to F \in (II Cn J)$
	isphtpy.3	$⊢ φ \to G \in (II Cn J)$
Assertion	isphtpy	$⊢ φ \to (H \in (F PHtpy (J) G) \leftrightarrow (H \in (F (II Htpy J) G) \land \forall s \in [0, 1] (0 H s = F (0) \land 1 H s = F (1))))$

Proof

Step	Hyp	Ref	Expression
1		isphtpy.2	$⊢ φ \to F \in (II Cn J)$
2		isphtpy.3	$⊢ φ \to G \in (II Cn J)$
3		cntop2	$⊢ F \in (II Cn J) \to J \in Top$
4		oveq2	$⊢ j = J \to II Cn j = II Cn J$
5		oveq2	$⊢ j = J \to II Htpy j = II Htpy J$
6	5	oveqd	$⊢ j = J \to f (II Htpy j) g = f (II Htpy J) g$
7	6	rabeqdv	$⊢ j = J \to \{h \in (f (II Htpy j) g) \| \forall s \in [0, 1] (0 h s = f (0) \land 1 h s = f (1))\} = \{h \in (f (II Htpy J) g) \| \forall s \in [0, 1] (0 h s = f (0) \land 1 h s = f (1))\}$
8	4 4 7	mpoeq123dv	$⊢ j = J \to (f \in (II Cn j), g \in (II Cn j) ⟼ \{h \in (f (II Htpy j) g) \| \forall s \in [0, 1] (0 h s = f (0) \land 1 h s = f (1))\}) = (f \in (II Cn J), g \in (II Cn J) ⟼ \{h \in (f (II Htpy J) g) \| \forall s \in [0, 1] (0 h s = f (0) \land 1 h s = f (1))\})$
9		df-phtpy	$⊢ PHtpy = (j \in Top ⟼ (f \in (II Cn j), g \in (II Cn j) ⟼ \{h \in (f (II Htpy j) g) \| \forall s \in [0, 1] (0 h s = f (0) \land 1 h s = f (1))\}))$
10		ovex	$⊢ II Cn J \in V$
11	10 10	mpoex	$⊢ (f \in (II Cn J), g \in (II Cn J) ⟼ \{h \in (f (II Htpy J) g) \| \forall s \in [0, 1] (0 h s = f (0) \land 1 h s = f (1))\}) \in V$
12	8 9 11	fvmpt	$⊢ J \in Top \to PHtpy (J) = (f \in (II Cn J), g \in (II Cn J) ⟼ \{h \in (f (II Htpy J) g) \| \forall s \in [0, 1] (0 h s = f (0) \land 1 h s = f (1))\})$
13	1 3 12	3syl	$⊢ φ \to PHtpy (J) = (f \in (II Cn J), g \in (II Cn J) ⟼ \{h \in (f (II Htpy J) g) \| \forall s \in [0, 1] (0 h s = f (0) \land 1 h s = f (1))\})$
14		oveq12	$⊢ (f = F \land g = G) \to f (II Htpy J) g = F (II Htpy J) G$
15		simpl	$⊢ (f = F \land g = G) \to f = F$
16	15	fveq1d	$⊢ (f = F \land g = G) \to f (0) = F (0)$
17	16	eqeq2d	$⊢ (f = F \land g = G) \to (0 h s = f (0) \leftrightarrow 0 h s = F (0))$
18	15	fveq1d	$⊢ (f = F \land g = G) \to f (1) = F (1)$
19	18	eqeq2d	$⊢ (f = F \land g = G) \to (1 h s = f (1) \leftrightarrow 1 h s = F (1))$
20	17 19	anbi12d	$⊢ (f = F \land g = G) \to ((0 h s = f (0) \land 1 h s = f (1)) \leftrightarrow (0 h s = F (0) \land 1 h s = F (1)))$
21	20	ralbidv	$⊢ (f = F \land g = G) \to (\forall s \in [0, 1] (0 h s = f (0) \land 1 h s = f (1)) \leftrightarrow \forall s \in [0, 1] (0 h s = F (0) \land 1 h s = F (1)))$
22	14 21	rabeqbidv	$⊢ (f = F \land g = G) \to \{h \in (f (II Htpy J) g) \| \forall s \in [0, 1] (0 h s = f (0) \land 1 h s = f (1))\} = \{h \in (F (II Htpy J) G) \| \forall s \in [0, 1] (0 h s = F (0) \land 1 h s = F (1))\}$
23	22	adantl	$⊢ (φ \land (f = F \land g = G)) \to \{h \in (f (II Htpy J) g) \| \forall s \in [0, 1] (0 h s = f (0) \land 1 h s = f (1))\} = \{h \in (F (II Htpy J) G) \| \forall s \in [0, 1] (0 h s = F (0) \land 1 h s = F (1))\}$
24		ovex	$⊢ F (II Htpy J) G \in V$
25	24	rabex	$⊢ \{h \in (F (II Htpy J) G) \| \forall s \in [0, 1] (0 h s = F (0) \land 1 h s = F (1))\} \in V$
26	25	a1i	$⊢ φ \to \{h \in (F (II Htpy J) G) \| \forall s \in [0, 1] (0 h s = F (0) \land 1 h s = F (1))\} \in V$
27	13 23 1 2 26	ovmpod	$⊢ φ \to F PHtpy (J) G = \{h \in (F (II Htpy J) G) \| \forall s \in [0, 1] (0 h s = F (0) \land 1 h s = F (1))\}$
28	27	eleq2d	$⊢ φ \to (H \in (F PHtpy (J) G) \leftrightarrow H \in \{h \in (F (II Htpy J) G) \| \forall s \in [0, 1] (0 h s = F (0) \land 1 h s = F (1))\})$
29		oveq	$⊢ h = H \to 0 h s = 0 H s$
30	29	eqeq1d	$⊢ h = H \to (0 h s = F (0) \leftrightarrow 0 H s = F (0))$
31		oveq	$⊢ h = H \to 1 h s = 1 H s$
32	31	eqeq1d	$⊢ h = H \to (1 h s = F (1) \leftrightarrow 1 H s = F (1))$
33	30 32	anbi12d	$⊢ h = H \to ((0 h s = F (0) \land 1 h s = F (1)) \leftrightarrow (0 H s = F (0) \land 1 H s = F (1)))$
34	33	ralbidv	$⊢ h = H \to (\forall s \in [0, 1] (0 h s = F (0) \land 1 h s = F (1)) \leftrightarrow \forall s \in [0, 1] (0 H s = F (0) \land 1 H s = F (1)))$
35	34	elrab	$⊢ H \in \{h \in (F (II Htpy J) G) \| \forall s \in [0, 1] (0 h s = F (0) \land 1 h s = F (1))\} \leftrightarrow (H \in (F (II Htpy J) G) \land \forall s \in [0, 1] (0 H s = F (0) \land 1 H s = F (1)))$
36	28 35	bitrdi	$⊢ φ \to (H \in (F PHtpy (J) G) \leftrightarrow (H \in (F (II Htpy J) G) \land \forall s \in [0, 1] (0 H s = F (0) \land 1 H s = F (1))))$

Metamath Proof Explorer

Theorem isphtpy

Proof