om1elbas

Description: Elementhood in 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	om1elbas	$⊢ φ \to (F \in B \leftrightarrow (F \in (II Cn J) \land F (0) = Y \land F (1) = Y))$

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	1 2 3 4	om1bas	$⊢ φ \to B = \{f \in (II Cn J) \| (f (0) = Y \land f (1) = Y)\}$
6	5	eleq2d	$⊢ φ \to (F \in B \leftrightarrow F \in \{f \in (II Cn J) \| (f (0) = Y \land f (1) = Y)\})$
7		fveq1	$⊢ f = F \to f (0) = F (0)$
8	7	eqeq1d	$⊢ f = F \to (f (0) = Y \leftrightarrow F (0) = Y)$
9		fveq1	$⊢ f = F \to f (1) = F (1)$
10	9	eqeq1d	$⊢ f = F \to (f (1) = Y \leftrightarrow F (1) = Y)$
11	8 10	anbi12d	$⊢ f = F \to ((f (0) = Y \land f (1) = Y) \leftrightarrow (F (0) = Y \land F (1) = Y))$
12	11	elrab	$⊢ F \in \{f \in (II Cn J) \| (f (0) = Y \land f (1) = Y)\} \leftrightarrow (F \in (II Cn J) \land (F (0) = Y \land F (1) = Y))$
13		3anass	$⊢ (F \in (II Cn J) \land F (0) = Y \land F (1) = Y) \leftrightarrow (F \in (II Cn J) \land (F (0) = Y \land F (1) = Y))$
14	12 13	bitr4i	$⊢ F \in \{f \in (II Cn J) \| (f (0) = Y \land f (1) = Y)\} \leftrightarrow (F \in (II Cn J) \land F (0) = Y \land F (1) = Y)$
15	6 14	bitrdi	$⊢ φ \to (F \in B \leftrightarrow (F \in (II Cn J) \land F (0) = Y \land F (1) = Y))$

Metamath Proof Explorer