Metamath Proof Explorer

Theorem om1bas

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

		Ref	Expression
	Hypotheses	om1bas.o	$⊢ O = J Ω_{1} Y$
		om1bas.j	$⊢ φ \to J \in TopOn (X)$
		om1bas.y	$⊢ φ \to Y \in X$
		om1bas.b	$⊢ φ \to B = {Base}_{O}$
	Assertion	om1bas	$⊢ φ \to B = \{f \in (II Cn J) \| (f (0) = Y \land f (1) = Y)\}$

Proof

Step	Hyp	Ref	Expression
1		om1bas.o	$⊢ O = J Ω_{1} Y$
2		om1bas.j	$⊢ φ \to J \in TopOn (X)$
3		om1bas.y	$⊢ φ \to Y \in X$
4		om1bas.b	$⊢ φ \to B = {Base}_{O}$
5		eqidd	$⊢ φ \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)\}$
6		eqidd	$⊢ φ \to _{𝑝} (J) = _{𝑝} (J)$
7		eqidd	$⊢ φ \to J^_{ko} II = J^_{ko} II$
8	1 5 6 7 2 3	om1val	$⊢ φ \to O = \{⟨{Base}_{ndx}, \{f \in (II Cn J) \| (f (0) = Y \land f (1) = Y)\}⟩, ⟨+_{ndx}, *_{𝑝} (J)⟩, ⟨TopSet (ndx), J^_{ko} II⟩\}$
9	8	fveq2d	$⊢ φ \to {Base}_{O} = {Base}_{\{⟨{Base}_{ndx}, \{f \in (II Cn J) \| (f (0) = Y \land f (1) = Y)\}⟩, ⟨+_{ndx}, *_{𝑝} (J)⟩, ⟨TopSet (ndx), J^_{ko} II⟩\}}$
10	4 9	eqtrd	$⊢ φ \to B = {Base}_{\{⟨{Base}_{ndx}, \{f \in (II Cn J) \| (f (0) = Y \land f (1) = Y)\}⟩, ⟨+_{ndx}, *_{𝑝} (J)⟩, ⟨TopSet (ndx), J^_{ko} II⟩\}}$
11		ovex	$⊢ II Cn J \in V$
12	11	rabex	$⊢ \{f \in (II Cn J) \| (f (0) = Y \land f (1) = Y)\} \in V$
13		eqid	$⊢ \{⟨{Base}_{ndx}, \{f \in (II Cn J) \| (f (0) = Y \land f (1) = Y)\}⟩, ⟨+_{ndx}, _{𝑝} (J)⟩, ⟨TopSet (ndx), J^_{ko} II⟩\} = \{⟨{Base}_{ndx}, \{f \in (II Cn J) \| (f (0) = Y \land f (1) = Y)\}⟩, ⟨+_{ndx}, _{𝑝} (J)⟩, ⟨TopSet (ndx), J^_{ko} II⟩\}$
14	13	topgrpbas	$⊢ \{f \in (II Cn J) \| (f (0) = Y \land f (1) = Y)\} \in V \to \{f \in (II Cn J) \| (f (0) = Y \land f (1) = Y)\} = {Base}_{\{⟨{Base}_{ndx}, \{f \in (II Cn J) \| (f (0) = Y \land f (1) = Y)\}⟩, ⟨+_{ndx}, *_{𝑝} (J)⟩, ⟨TopSet (ndx), J^_{ko} II⟩\}}$
15	12 14	ax-mp	$⊢ \{f \in (II Cn J) \| (f (0) = Y \land f (1) = Y)\} = {Base}_{\{⟨{Base}_{ndx}, \{f \in (II Cn J) \| (f (0) = Y \land f (1) = Y)\}⟩, ⟨+_{ndx}, *_{𝑝} (J)⟩, ⟨TopSet (ndx), J^_{ko} II⟩\}}$
16	10 15	eqtr4di	$⊢ φ \to B = \{f \in (II Cn J) \| (f (0) = Y \land f (1) = Y)\}$