Theorem pi1eluni

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

	Ref	Expression
Hypotheses	pi1val.g	|- G = ( J pi1 Y )
	pi1val.1	|- ( ph -> J e. ( TopOn ` X ) )
	pi1val.2	|- ( ph -> Y e. X )
	pi1bas2.b	|- ( ph -> B = ( Base ` G ) )
Assertion	pi1eluni	|- ( ph -> ( F e. U. B <-> ( F e. ( II Cn J ) /\ ( F ` 0 ) = Y /\ ( F ` 1 ) = Y ) ) )

Proof

Step	Hyp	Ref	Expression
1		pi1val.g	|- G = ( J pi1 Y )
2		pi1val.1	|- ( ph -> J e. ( TopOn ` X ) )
3		pi1val.2	|- ( ph -> Y e. X )
4		pi1bas2.b	|- ( ph -> B = ( Base ` G ) )
5		eqid	|- ( J Om1 Y ) = ( J Om1 Y )
6		eqidd	|- ( ph -> ( Base ` ( J Om1 Y ) ) = ( Base ` ( J Om1 Y ) ) )
7	1 2 3 5 4 6	pi1buni	|- ( ph -> U. B = ( Base ` ( J Om1 Y ) ) )
8	5 2 3 7	om1elbas	|- ( ph -> ( F e. U. B <-> ( F e. ( II Cn J ) /\ ( F ` 0 ) = Y /\ ( F ` 1 ) = Y ) ) )