Theorem 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 Om1 Y )
	om1bas.j	|- ( ph -> J e. ( TopOn ` X ) )
	om1bas.y	|- ( ph -> Y e. X )
	om1bas.b	|- ( ph -> B = ( Base ` O ) )
Assertion	om1elbas	|- ( ph -> ( F e. B <-> ( F e. ( II Cn J ) /\ ( F ` 0 ) = Y /\ ( F ` 1 ) = Y ) ) )

Proof

Step	Hyp	Ref	Expression
1		om1bas.o	|- O = ( J Om1 Y )
2		om1bas.j	|- ( ph -> J e. ( TopOn ` X ) )
3		om1bas.y	|- ( ph -> Y e. X )
4		om1bas.b	|- ( ph -> B = ( Base ` O ) )
5	1 2 3 4	om1bas	|- ( ph -> B = { f e. ( II Cn J ) | ( ( f ` 0 ) = Y /\ ( f ` 1 ) = Y ) } )
6	5	eleq2d	|- ( ph -> ( F e. B <-> F e. { f e. ( II Cn J ) | ( ( f ` 0 ) = Y /\ ( f ` 1 ) = Y ) } ) )
7		fveq1	|- ( f = F -> ( f ` 0 ) = ( F ` 0 ) )
8	7	eqeq1d	|- ( f = F -> ( ( f ` 0 ) = Y <-> ( F ` 0 ) = Y ) )
9		fveq1	|- ( f = F -> ( f ` 1 ) = ( F ` 1 ) )
10	9	eqeq1d	|- ( f = F -> ( ( f ` 1 ) = Y <-> ( F ` 1 ) = Y ) )
11	8 10	anbi12d	|- ( f = F -> ( ( ( f ` 0 ) = Y /\ ( f ` 1 ) = Y ) <-> ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Y ) ) )
12	11	elrab	|- ( F e. { f e. ( II Cn J ) | ( ( f ` 0 ) = Y /\ ( f ` 1 ) = Y ) } <-> ( F e. ( II Cn J ) /\ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Y ) ) )
13		3anass	|- ( ( F e. ( II Cn J ) /\ ( F ` 0 ) = Y /\ ( F ` 1 ) = Y ) <-> ( F e. ( II Cn J ) /\ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Y ) ) )
14	12 13	bitr4i	|- ( F e. { f e. ( II Cn J ) | ( ( f ` 0 ) = Y /\ ( f ` 1 ) = Y ) } <-> ( F e. ( II Cn J ) /\ ( F ` 0 ) = Y /\ ( F ` 1 ) = Y ) )
15	6 14	bitrdi	|- ( ph -> ( F e. B <-> ( F e. ( II Cn J ) /\ ( F ` 0 ) = Y /\ ( F ` 1 ) = Y ) ) )