Metamath Proof Explorer


Theorem pi1bas3

Description: The base set of the fundamental group. (Contributed by Mario Carneiro, 10-Jul-2015)

Ref Expression
Hypotheses pi1val.g G = J π 1 Y
pi1val.1 φ J TopOn X
pi1val.2 φ Y X
pi1bas2.b φ B = Base G
pi1bas3.r R = ph J B × B
Assertion pi1bas3 φ B = B / R

Proof

Step Hyp Ref Expression
1 pi1val.g G = J π 1 Y
2 pi1val.1 φ J TopOn X
3 pi1val.2 φ Y X
4 pi1bas2.b φ B = Base G
5 pi1bas3.r R = ph J B × B
6 1 2 3 4 pi1bas2 φ B = B / ph J
7 eqid J Ω 1 Y = J Ω 1 Y
8 eqidd φ Base J Ω 1 Y = Base J Ω 1 Y
9 1 2 3 7 4 8 pi1buni φ B = Base J Ω 1 Y
10 1 2 3 7 4 9 pi1blem φ ph J B B B II Cn J
11 10 simpld φ ph J B B
12 qsinxp ph J B B B / ph J = B / ph J B × B
13 11 12 syl φ B / ph J = B / ph J B × B
14 6 13 eqtrd φ B = B / ph J B × B
15 qseq2 R = ph J B × B B / R = B / ph J B × B
16 5 15 ax-mp B / R = B / ph J B × B
17 14 16 eqtr4di φ B = B / R