Theorem pi1bas

Description: The base set of the fundamental group of a topological space at a given base point. (Contributed by Jeff Madsen, 11-Jun-2010) (Revised 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 )
	pi1val.o	|- O = ( J Om1 Y )
	pi1bas.b	|- ( ph -> B = ( Base ` G ) )
	pi1bas.k	|- ( ph -> K = ( Base ` O ) )
Assertion	pi1bas	|- ( ph -> B = ( K /. ( ~=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		pi1val.o	|- O = ( J Om1 Y )
5		pi1bas.b	|- ( ph -> B = ( Base ` G ) )
6		pi1bas.k	|- ( ph -> K = ( Base ` O ) )
7	1 2 3 4	pi1val	|- ( ph -> G = ( O /s ( ~=ph ` J ) ) )
8		eqidd	|- ( ph -> ( Base ` O ) = ( Base ` O ) )
9		fvexd	|- ( ph -> ( ~=ph ` J ) e. _V )
10	4	ovexi	|- O e. _V
11	10	a1i	|- ( ph -> O e. _V )
12	7 8 9 11	qusbas	|- ( ph -> ( ( Base ` O ) /. ( ~=ph ` J ) ) = ( Base ` G ) )
13		qseq1	|- ( K = ( Base ` O ) -> ( K /. ( ~=ph ` J ) ) = ( ( Base ` O ) /. ( ~=ph ` J ) ) )
14	6 13	syl	|- ( ph -> ( K /. ( ~=ph ` J ) ) = ( ( Base ` O ) /. ( ~=ph ` J ) ) )
15	12 14 5	3eqtr4rd	|- ( ph -> B = ( K /. ( ~=ph ` J ) ) )