Theorem pi1bas3

Description: The base set of the fundamental group. (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 ) )
	pi1bas3.r	|- R = ( ( ~=ph ` J ) i^i ( U. B X. U. B ) )
Assertion	pi1bas3	|- ( ph -> B = ( U. B /. R ) )

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		pi1bas3.r	|- R = ( ( ~=ph ` J ) i^i ( U. B X. U. B ) )
6	1 2 3 4	pi1bas2	|- ( ph -> B = ( U. B /. ( ~=ph ` J ) ) )
7		eqid	|- ( J Om1 Y ) = ( J Om1 Y )
8		eqidd	|- ( ph -> ( Base ` ( J Om1 Y ) ) = ( Base ` ( J Om1 Y ) ) )
9	1 2 3 7 4 8	pi1buni	|- ( ph -> U. B = ( Base ` ( J Om1 Y ) ) )
10	1 2 3 7 4 9	pi1blem	|- ( ph -> ( ( ( ~=ph ` J ) " U. B ) C_ U. B /\ U. B C_ ( II Cn J ) ) )
11	10	simpld	|- ( ph -> ( ( ~=ph ` J ) " U. B ) C_ U. B )
12		qsinxp	|- ( ( ( ~=ph ` J ) " U. B ) C_ U. B -> ( U. B /. ( ~=ph ` J ) ) = ( U. B /. ( ( ~=ph ` J ) i^i ( U. B X. U. B ) ) ) )
13	11 12	syl	|- ( ph -> ( U. B /. ( ~=ph ` J ) ) = ( U. B /. ( ( ~=ph ` J ) i^i ( U. B X. U. B ) ) ) )
14	6 13	eqtrd	|- ( ph -> B = ( U. B /. ( ( ~=ph ` J ) i^i ( U. B X. U. B ) ) ) )
15		qseq2	|- ( R = ( ( ~=ph ` J ) i^i ( U. B X. U. B ) ) -> ( U. B /. R ) = ( U. B /. ( ( ~=ph ` J ) i^i ( U. B X. U. B ) ) ) )
16	5 15	ax-mp	|- ( U. B /. R ) = ( U. B /. ( ( ~=ph ` J ) i^i ( U. B X. U. B ) ) )
17	14 16	eqtr4di	|- ( ph -> B = ( U. B /. R ) )