ishtpy

Description: Membership in the class of homotopies between two continuous functions. (Contributed by Mario Carneiro, 22-Feb-2015) (Revised by Mario Carneiro, 5-Sep-2015)

	Ref	Expression
Hypotheses	ishtpy.1	$⊢ φ \to J \in TopOn (X)$
	ishtpy.3	$⊢ φ \to F \in (J Cn K)$
	ishtpy.4	$⊢ φ \to G \in (J Cn K)$
Assertion	ishtpy	$⊢ φ \to (H \in (F (J Htpy K) G) \leftrightarrow (H \in ((J \times_{t} II) Cn K) \land \forall s \in X (s H 0 = F (s) \land s H 1 = G (s))))$

Proof

Step	Hyp	Ref	Expression
1		ishtpy.1	$⊢ φ \to J \in TopOn (X)$
2		ishtpy.3	$⊢ φ \to F \in (J Cn K)$
3		ishtpy.4	$⊢ φ \to G \in (J Cn K)$
4		df-htpy	$⊢ Htpy = (j \in Top, k \in Top ⟼ (f \in (j Cn k), g \in (j Cn k) ⟼ \{h \in ((j \times_{t} II) Cn k) \| \forall s \in ⋃ j (s h 0 = f (s) \land s h 1 = g (s))\}))$
5	4	a1i	$⊢ φ \to Htpy = (j \in Top, k \in Top ⟼ (f \in (j Cn k), g \in (j Cn k) ⟼ \{h \in ((j \times_{t} II) Cn k) \| \forall s \in ⋃ j (s h 0 = f (s) \land s h 1 = g (s))\}))$
6		simprl	$⊢ (φ \land (j = J \land k = K)) \to j = J$
7		simprr	$⊢ (φ \land (j = J \land k = K)) \to k = K$
8	6 7	oveq12d	$⊢ (φ \land (j = J \land k = K)) \to j Cn k = J Cn K$
9	6	oveq1d	$⊢ (φ \land (j = J \land k = K)) \to j \times_{t} II = J \times_{t} II$
10	9 7	oveq12d	$⊢ (φ \land (j = J \land k = K)) \to (j \times_{t} II) Cn k = (J \times_{t} II) Cn K$
11	6	unieqd	$⊢ (φ \land (j = J \land k = K)) \to ⋃ j = ⋃ J$
12		toponuni	$⊢ J \in TopOn (X) \to X = ⋃ J$
13	1 12	syl	$⊢ φ \to X = ⋃ J$
14	13	adantr	$⊢ (φ \land (j = J \land k = K)) \to X = ⋃ J$
15	11 14	eqtr4d	$⊢ (φ \land (j = J \land k = K)) \to ⋃ j = X$
16	15	raleqdv	$⊢ (φ \land (j = J \land k = K)) \to (\forall s \in ⋃ j (s h 0 = f (s) \land s h 1 = g (s)) \leftrightarrow \forall s \in X (s h 0 = f (s) \land s h 1 = g (s)))$
17	10 16	rabeqbidv	$⊢ (φ \land (j = J \land k = K)) \to \{h \in ((j \times_{t} II) Cn k) \| \forall s \in ⋃ j (s h 0 = f (s) \land s h 1 = g (s))\} = \{h \in ((J \times_{t} II) Cn K) \| \forall s \in X (s h 0 = f (s) \land s h 1 = g (s))\}$
18	8 8 17	mpoeq123dv	$⊢ (φ \land (j = J \land k = K)) \to (f \in (j Cn k), g \in (j Cn k) ⟼ \{h \in ((j \times_{t} II) Cn k) \| \forall s \in ⋃ j (s h 0 = f (s) \land s h 1 = g (s))\}) = (f \in (J Cn K), g \in (J Cn K) ⟼ \{h \in ((J \times_{t} II) Cn K) \| \forall s \in X (s h 0 = f (s) \land s h 1 = g (s))\})$
19		topontop	$⊢ J \in TopOn (X) \to J \in Top$
20	1 19	syl	$⊢ φ \to J \in Top$
21		cntop2	$⊢ F \in (J Cn K) \to K \in Top$
22	2 21	syl	$⊢ φ \to K \in Top$
23		ovex	$⊢ (J \times_{t} II) Cn K \in V$
24		ssrab2	$⊢ \{h \in ((J \times_{t} II) Cn K) \| \forall s \in X (s h 0 = f (s) \land s h 1 = g (s))\} \subseteq (J \times_{t} II) Cn K$
25	23 24	elpwi2	$⊢ \{h \in ((J \times_{t} II) Cn K) \| \forall s \in X (s h 0 = f (s) \land s h 1 = g (s))\} \in 𝒫 ((J \times_{t} II) Cn K)$
26	25	rgen2w	$⊢ \forall f \in (J Cn K) \forall g \in (J Cn K) \{h \in ((J \times_{t} II) Cn K) \| \forall s \in X (s h 0 = f (s) \land s h 1 = g (s))\} \in 𝒫 ((J \times_{t} II) Cn K)$
27		eqid	$⊢ (f \in (J Cn K), g \in (J Cn K) ⟼ \{h \in ((J \times_{t} II) Cn K) \| \forall s \in X (s h 0 = f (s) \land s h 1 = g (s))\}) = (f \in (J Cn K), g \in (J Cn K) ⟼ \{h \in ((J \times_{t} II) Cn K) \| \forall s \in X (s h 0 = f (s) \land s h 1 = g (s))\})$
28	27	fmpo	$⊢ \forall f \in (J Cn K) \forall g \in (J Cn K) \{h \in ((J \times_{t} II) Cn K) \| \forall s \in X (s h 0 = f (s) \land s h 1 = g (s))\} \in 𝒫 ((J \times_{t} II) Cn K) \leftrightarrow (f \in (J Cn K), g \in (J Cn K) ⟼ \{h \in ((J \times_{t} II) Cn K) \| \forall s \in X (s h 0 = f (s) \land s h 1 = g (s))\}) : (J Cn K) \times (J Cn K) ⟶ 𝒫 ((J \times_{t} II) Cn K)$
29	26 28	mpbi	$⊢ (f \in (J Cn K), g \in (J Cn K) ⟼ \{h \in ((J \times_{t} II) Cn K) \| \forall s \in X (s h 0 = f (s) \land s h 1 = g (s))\}) : (J Cn K) \times (J Cn K) ⟶ 𝒫 ((J \times_{t} II) Cn K)$
30		ovex	$⊢ J Cn K \in V$
31	30 30	xpex	$⊢ (J Cn K) \times (J Cn K) \in V$
32	23	pwex	$⊢ 𝒫 ((J \times_{t} II) Cn K) \in V$
33		fex2	$⊢ ((f \in (J Cn K), g \in (J Cn K) ⟼ \{h \in ((J \times_{t} II) Cn K) \| \forall s \in X (s h 0 = f (s) \land s h 1 = g (s))\}) : (J Cn K) \times (J Cn K) ⟶ 𝒫 ((J \times_{t} II) Cn K) \land (J Cn K) \times (J Cn K) \in V \land 𝒫 ((J \times_{t} II) Cn K) \in V) \to (f \in (J Cn K), g \in (J Cn K) ⟼ \{h \in ((J \times_{t} II) Cn K) \| \forall s \in X (s h 0 = f (s) \land s h 1 = g (s))\}) \in V$
34	29 31 32 33	mp3an	$⊢ (f \in (J Cn K), g \in (J Cn K) ⟼ \{h \in ((J \times_{t} II) Cn K) \| \forall s \in X (s h 0 = f (s) \land s h 1 = g (s))\}) \in V$
35	34	a1i	$⊢ φ \to (f \in (J Cn K), g \in (J Cn K) ⟼ \{h \in ((J \times_{t} II) Cn K) \| \forall s \in X (s h 0 = f (s) \land s h 1 = g (s))\}) \in V$
36	5 18 20 22 35	ovmpod	$⊢ φ \to J Htpy K = (f \in (J Cn K), g \in (J Cn K) ⟼ \{h \in ((J \times_{t} II) Cn K) \| \forall s \in X (s h 0 = f (s) \land s h 1 = g (s))\})$
37		fveq1	$⊢ f = F \to f (s) = F (s)$
38	37	eqeq2d	$⊢ f = F \to (s h 0 = f (s) \leftrightarrow s h 0 = F (s))$
39		fveq1	$⊢ g = G \to g (s) = G (s)$
40	39	eqeq2d	$⊢ g = G \to (s h 1 = g (s) \leftrightarrow s h 1 = G (s))$
41	38 40	bi2anan9	$⊢ (f = F \land g = G) \to ((s h 0 = f (s) \land s h 1 = g (s)) \leftrightarrow (s h 0 = F (s) \land s h 1 = G (s)))$
42	41	adantl	$⊢ (φ \land (f = F \land g = G)) \to ((s h 0 = f (s) \land s h 1 = g (s)) \leftrightarrow (s h 0 = F (s) \land s h 1 = G (s)))$
43	42	ralbidv	$⊢ (φ \land (f = F \land g = G)) \to (\forall s \in X (s h 0 = f (s) \land s h 1 = g (s)) \leftrightarrow \forall s \in X (s h 0 = F (s) \land s h 1 = G (s)))$
44	43	rabbidv	$⊢ (φ \land (f = F \land g = G)) \to \{h \in ((J \times_{t} II) Cn K) \| \forall s \in X (s h 0 = f (s) \land s h 1 = g (s))\} = \{h \in ((J \times_{t} II) Cn K) \| \forall s \in X (s h 0 = F (s) \land s h 1 = G (s))\}$
45	23	rabex	$⊢ \{h \in ((J \times_{t} II) Cn K) \| \forall s \in X (s h 0 = F (s) \land s h 1 = G (s))\} \in V$
46	45	a1i	$⊢ φ \to \{h \in ((J \times_{t} II) Cn K) \| \forall s \in X (s h 0 = F (s) \land s h 1 = G (s))\} \in V$
47	36 44 2 3 46	ovmpod	$⊢ φ \to F (J Htpy K) G = \{h \in ((J \times_{t} II) Cn K) \| \forall s \in X (s h 0 = F (s) \land s h 1 = G (s))\}$
48	47	eleq2d	$⊢ φ \to (H \in (F (J Htpy K) G) \leftrightarrow H \in \{h \in ((J \times_{t} II) Cn K) \| \forall s \in X (s h 0 = F (s) \land s h 1 = G (s))\})$
49		oveq	$⊢ h = H \to s h 0 = s H 0$
50	49	eqeq1d	$⊢ h = H \to (s h 0 = F (s) \leftrightarrow s H 0 = F (s))$
51		oveq	$⊢ h = H \to s h 1 = s H 1$
52	51	eqeq1d	$⊢ h = H \to (s h 1 = G (s) \leftrightarrow s H 1 = G (s))$
53	50 52	anbi12d	$⊢ h = H \to ((s h 0 = F (s) \land s h 1 = G (s)) \leftrightarrow (s H 0 = F (s) \land s H 1 = G (s)))$
54	53	ralbidv	$⊢ h = H \to (\forall s \in X (s h 0 = F (s) \land s h 1 = G (s)) \leftrightarrow \forall s \in X (s H 0 = F (s) \land s H 1 = G (s)))$
55	54	elrab	$⊢ H \in \{h \in ((J \times_{t} II) Cn K) \| \forall s \in X (s h 0 = F (s) \land s h 1 = G (s))\} \leftrightarrow (H \in ((J \times_{t} II) Cn K) \land \forall s \in X (s H 0 = F (s) \land s H 1 = G (s)))$
56	48 55	bitrdi	$⊢ φ \to (H \in (F (J Htpy K) G) \leftrightarrow (H \in ((J \times_{t} II) Cn K) \land \forall s \in X (s H 0 = F (s) \land s H 1 = G (s))))$

Metamath Proof Explorer

Theorem ishtpy

Proof