Theorem pi1bas2

Description: The base set of the fundamental group, written self-referentially. (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	pi1bas2	|- ( ph -> B = ( U. B /. ( ~=ph ` J ) ) )

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	1 2 3 5 4 7	pi1bas	|- ( ph -> B = ( U. B /. ( ~=ph ` J ) ) )