Description: The base set of the fundamental group, written self-referentially. (Contributed by Mario Carneiro, 10-Jul-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | pi1val.g | ⊢ 𝐺 = ( 𝐽 π1 𝑌 ) | |
pi1val.1 | ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) | ||
pi1val.2 | ⊢ ( 𝜑 → 𝑌 ∈ 𝑋 ) | ||
pi1bas2.b | ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐺 ) ) | ||
Assertion | pi1bas2 | ⊢ ( 𝜑 → 𝐵 = ( ∪ 𝐵 / ( ≃ph ‘ 𝐽 ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pi1val.g | ⊢ 𝐺 = ( 𝐽 π1 𝑌 ) | |
2 | pi1val.1 | ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) | |
3 | pi1val.2 | ⊢ ( 𝜑 → 𝑌 ∈ 𝑋 ) | |
4 | pi1bas2.b | ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐺 ) ) | |
5 | eqid | ⊢ ( 𝐽 Ω1 𝑌 ) = ( 𝐽 Ω1 𝑌 ) | |
6 | eqidd | ⊢ ( 𝜑 → ( Base ‘ ( 𝐽 Ω1 𝑌 ) ) = ( Base ‘ ( 𝐽 Ω1 𝑌 ) ) ) | |
7 | 1 2 3 5 4 6 | pi1buni | ⊢ ( 𝜑 → ∪ 𝐵 = ( Base ‘ ( 𝐽 Ω1 𝑌 ) ) ) |
8 | 1 2 3 5 4 7 | pi1bas | ⊢ ( 𝜑 → 𝐵 = ( ∪ 𝐵 / ( ≃ph ‘ 𝐽 ) ) ) |