om1val

Description: The definition of the loop space. (Contributed by Mario Carneiro, 10-Jul-2015)

	Ref	Expression
Hypotheses	om1val.o	$⊢ O = J Ω_{1} Y$
	om1val.b	$⊢ φ \to B = \{f \in (II Cn J) \| (f (0) = Y \land f (1) = Y)\}$
	om1val.p	$⊢ φ \to \underset{˙}{+} = *_{𝑝} (J)$
	om1val.k	$⊢ φ \to K = J^_{ko} II$
	om1val.j	$⊢ φ \to J \in TopOn (X)$
	om1val.y	$⊢ φ \to Y \in X$
Assertion	om1val	$⊢ φ \to O = \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨TopSet (ndx), K⟩\}$

Proof

Step	Hyp	Ref	Expression
1		om1val.o	$⊢ O = J Ω_{1} Y$
2		om1val.b	$⊢ φ \to B = \{f \in (II Cn J) \| (f (0) = Y \land f (1) = Y)\}$
3		om1val.p	$⊢ φ \to \underset{˙}{+} = *_{𝑝} (J)$
4		om1val.k	$⊢ φ \to K = J^_{ko} II$
5		om1val.j	$⊢ φ \to J \in TopOn (X)$
6		om1val.y	$⊢ φ \to Y \in X$
7		df-om1	$⊢ Ω_{1} = (j \in Top, y \in ⋃ j ⟼ \{⟨{Base}_{ndx}, \{f \in (II Cn j) \| (f (0) = y \land f (1) = y)\}⟩, ⟨+_{ndx}, *_{𝑝} (j)⟩, ⟨TopSet (ndx), j^_{ko} II⟩\})$
8	7	a1i	$⊢ φ \to Ω_{1} = (j \in Top, y \in ⋃ j ⟼ \{⟨{Base}_{ndx}, \{f \in (II Cn j) \| (f (0) = y \land f (1) = y)\}⟩, ⟨+_{ndx}, *_{𝑝} (j)⟩, ⟨TopSet (ndx), j^_{ko} II⟩\})$
9		simprl	$⊢ (φ \land (j = J \land y = Y)) \to j = J$
10	9	oveq2d	$⊢ (φ \land (j = J \land y = Y)) \to II Cn j = II Cn J$
11		simprr	$⊢ (φ \land (j = J \land y = Y)) \to y = Y$
12	11	eqeq2d	$⊢ (φ \land (j = J \land y = Y)) \to (f (0) = y \leftrightarrow f (0) = Y)$
13	11	eqeq2d	$⊢ (φ \land (j = J \land y = Y)) \to (f (1) = y \leftrightarrow f (1) = Y)$
14	12 13	anbi12d	$⊢ (φ \land (j = J \land y = Y)) \to ((f (0) = y \land f (1) = y) \leftrightarrow (f (0) = Y \land f (1) = Y))$
15	10 14	rabeqbidv	$⊢ (φ \land (j = J \land y = Y)) \to \{f \in (II Cn j) \| (f (0) = y \land f (1) = y)\} = \{f \in (II Cn J) \| (f (0) = Y \land f (1) = Y)\}$
16	2	adantr	$⊢ (φ \land (j = J \land y = Y)) \to B = \{f \in (II Cn J) \| (f (0) = Y \land f (1) = Y)\}$
17	15 16	eqtr4d	$⊢ (φ \land (j = J \land y = Y)) \to \{f \in (II Cn j) \| (f (0) = y \land f (1) = y)\} = B$
18	17	opeq2d	$⊢ (φ \land (j = J \land y = Y)) \to ⟨{Base}_{ndx}, \{f \in (II Cn j) \| (f (0) = y \land f (1) = y)\}⟩ = ⟨{Base}_{ndx}, B⟩$
19	9	fveq2d	$⊢ (φ \land (j = J \land y = Y)) \to _{𝑝} (j) = _{𝑝} (J)$
20	3	adantr	$⊢ (φ \land (j = J \land y = Y)) \to \underset{˙}{+} = *_{𝑝} (J)$
21	19 20	eqtr4d	$⊢ (φ \land (j = J \land y = Y)) \to *_{𝑝} (j) = \underset{˙}{+}$
22	21	opeq2d	$⊢ (φ \land (j = J \land y = Y)) \to ⟨+_{ndx}, *_{𝑝} (j)⟩ = ⟨+_{ndx}, \underset{˙}{+}⟩$
23	9	oveq1d	$⊢ (φ \land (j = J \land y = Y)) \to j^_{ko} II = J^_{ko} II$
24	4	adantr	$⊢ (φ \land (j = J \land y = Y)) \to K = J^_{ko} II$
25	23 24	eqtr4d	$⊢ (φ \land (j = J \land y = Y)) \to j^_{ko} II = K$
26	25	opeq2d	$⊢ (φ \land (j = J \land y = Y)) \to ⟨TopSet (ndx), j^_{ko} II⟩ = ⟨TopSet (ndx), K⟩$
27	18 22 26	tpeq123d	$⊢ (φ \land (j = J \land y = Y)) \to \{⟨{Base}_{ndx}, \{f \in (II Cn j) \| (f (0) = y \land f (1) = y)\}⟩, ⟨+_{ndx}, *_{𝑝} (j)⟩, ⟨TopSet (ndx), j^_{ko} II⟩\} = \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨TopSet (ndx), K⟩\}$
28		unieq	$⊢ j = J \to ⋃ j = ⋃ J$
29	28	adantl	$⊢ (φ \land j = J) \to ⋃ j = ⋃ J$
30		toponuni	$⊢ J \in TopOn (X) \to X = ⋃ J$
31	5 30	syl	$⊢ φ \to X = ⋃ J$
32	31	adantr	$⊢ (φ \land j = J) \to X = ⋃ J$
33	29 32	eqtr4d	$⊢ (φ \land j = J) \to ⋃ j = X$
34		topontop	$⊢ J \in TopOn (X) \to J \in Top$
35	5 34	syl	$⊢ φ \to J \in Top$
36		tpex	$⊢ \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨TopSet (ndx), K⟩\} \in V$
37	36	a1i	$⊢ φ \to \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨TopSet (ndx), K⟩\} \in V$
38	8 27 33 35 6 37	ovmpodx	$⊢ φ \to J Ω_{1} Y = \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨TopSet (ndx), K⟩\}$
39	1 38	eqtrid	$⊢ φ \to O = \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨TopSet (ndx), K⟩\}$

Metamath Proof Explorer

Theorem om1val

Proof