Theorem pi1buni

Description: Another way to write the loop space base in terms of the base 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 )
	pi1val.o	|- O = ( J Om1 Y )
	pi1bas.b	|- ( ph -> B = ( Base ` G ) )
	pi1bas.k	|- ( ph -> K = ( Base ` O ) )
Assertion	pi1buni	|- ( ph -> U. B = K )

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 5 6	pi1bas	|- ( ph -> B = ( K /. ( ~=ph ` J ) ) )
8	1 2 3 4 5 6	pi1blem	|- ( ph -> ( ( ( ~=ph ` J ) " K ) C_ K /\ K C_ ( II Cn J ) ) )
9	8	simpld	|- ( ph -> ( ( ~=ph ` J ) " K ) C_ K )
10		qsinxp	|- ( ( ( ~=ph ` J ) " K ) C_ K -> ( K /. ( ~=ph ` J ) ) = ( K /. ( ( ~=ph ` J ) i^i ( K X. K ) ) ) )
11	9 10	syl	|- ( ph -> ( K /. ( ~=ph ` J ) ) = ( K /. ( ( ~=ph ` J ) i^i ( K X. K ) ) ) )
12	7 11	eqtrd	|- ( ph -> B = ( K /. ( ( ~=ph ` J ) i^i ( K X. K ) ) ) )
13	12	unieqd	|- ( ph -> U. B = U. ( K /. ( ( ~=ph ` J ) i^i ( K X. K ) ) ) )
14		phtpcer	|- ( ~=ph ` J ) Er ( II Cn J )
15	14	a1i	|- ( ph -> ( ~=ph ` J ) Er ( II Cn J ) )
16	8	simprd	|- ( ph -> K C_ ( II Cn J ) )
17	15 16	erinxp	|- ( ph -> ( ( ~=ph ` J ) i^i ( K X. K ) ) Er K )
18		fvex	|- ( ~=ph ` J ) e. _V
19	18	inex1	|- ( ( ~=ph ` J ) i^i ( K X. K ) ) e. _V
20	19	a1i	|- ( ph -> ( ( ~=ph ` J ) i^i ( K X. K ) ) e. _V )
21	17 20	uniqs2	|- ( ph -> U. ( K /. ( ( ~=ph ` J ) i^i ( K X. K ) ) ) = K )
22	13 21	eqtrd	|- ( ph -> U. B = K )