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	⊢ 𝐺 = ( 𝐽 π1 𝑌 )
	pi1val.1	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
	pi1val.2	⊢ ( 𝜑 → 𝑌 ∈ 𝑋 )
	pi1val.o	⊢ 𝑂 = ( 𝐽 Ω1 𝑌 )
	pi1bas.b	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐺 ) )
	pi1bas.k	⊢ ( 𝜑 → 𝐾 = ( Base ‘ 𝑂 ) )
Assertion	pi1buni	⊢ ( 𝜑 → ∪ 𝐵 = 𝐾 )

Proof

Step	Hyp	Ref	Expression
1		pi1val.g	⊢ 𝐺 = ( 𝐽 π1 𝑌 )
2		pi1val.1	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
3		pi1val.2	⊢ ( 𝜑 → 𝑌 ∈ 𝑋 )
4		pi1val.o	⊢ 𝑂 = ( 𝐽 Ω1 𝑌 )
5		pi1bas.b	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐺 ) )
6		pi1bas.k	⊢ ( 𝜑 → 𝐾 = ( Base ‘ 𝑂 ) )
7	1 2 3 4 5 6	pi1bas	⊢ ( 𝜑 → 𝐵 = ( 𝐾 / ( ≃ph ‘ 𝐽 ) ) )
8	1 2 3 4 5 6	pi1blem	⊢ ( 𝜑 → ( ( ( ≃ph ‘ 𝐽 ) “ 𝐾 ) ⊆ 𝐾 ∧ 𝐾 ⊆ ( II Cn 𝐽 ) ) )
9	8	simpld	⊢ ( 𝜑 → ( ( ≃ph ‘ 𝐽 ) “ 𝐾 ) ⊆ 𝐾 )
10		qsinxp	⊢ ( ( ( ≃ph ‘ 𝐽 ) “ 𝐾 ) ⊆ 𝐾 → ( 𝐾 / ( ≃ph ‘ 𝐽 ) ) = ( 𝐾 / ( ( ≃ph ‘ 𝐽 ) ∩ ( 𝐾 × 𝐾 ) ) ) )
11	9 10	syl	⊢ ( 𝜑 → ( 𝐾 / ( ≃ph ‘ 𝐽 ) ) = ( 𝐾 / ( ( ≃ph ‘ 𝐽 ) ∩ ( 𝐾 × 𝐾 ) ) ) )
12	7 11	eqtrd	⊢ ( 𝜑 → 𝐵 = ( 𝐾 / ( ( ≃ph ‘ 𝐽 ) ∩ ( 𝐾 × 𝐾 ) ) ) )
13	12	unieqd	⊢ ( 𝜑 → ∪ 𝐵 = ∪ ( 𝐾 / ( ( ≃ph ‘ 𝐽 ) ∩ ( 𝐾 × 𝐾 ) ) ) )
14		phtpcer	⊢ ( ≃ph ‘ 𝐽 ) Er ( II Cn 𝐽 )
15	14	a1i	⊢ ( 𝜑 → ( ≃ph ‘ 𝐽 ) Er ( II Cn 𝐽 ) )
16	8	simprd	⊢ ( 𝜑 → 𝐾 ⊆ ( II Cn 𝐽 ) )
17	15 16	erinxp	⊢ ( 𝜑 → ( ( ≃ph ‘ 𝐽 ) ∩ ( 𝐾 × 𝐾 ) ) Er 𝐾 )
18		fvex	⊢ ( ≃ph ‘ 𝐽 ) ∈ V
19	18	inex1	⊢ ( ( ≃ph ‘ 𝐽 ) ∩ ( 𝐾 × 𝐾 ) ) ∈ V
20	19	a1i	⊢ ( 𝜑 → ( ( ≃ph ‘ 𝐽 ) ∩ ( 𝐾 × 𝐾 ) ) ∈ V )
21	17 20	uniqs2	⊢ ( 𝜑 → ∪ ( 𝐾 / ( ( ≃ph ‘ 𝐽 ) ∩ ( 𝐾 × 𝐾 ) ) ) = 𝐾 )
22	13 21	eqtrd	⊢ ( 𝜑 → ∪ 𝐵 = 𝐾 )