Metamath Proof Explorer


Theorem tgldim0itv

Description: In dimension zero, any two points are equal. (Contributed by Thierry Arnoux, 12-Apr-2019)

Ref Expression
Hypotheses tgbtwndiff.p 𝑃 = ( Base ‘ 𝐺 )
tgbtwndiff.d = ( dist ‘ 𝐺 )
tgbtwndiff.i 𝐼 = ( Itv ‘ 𝐺 )
tgbtwndiff.g ( 𝜑𝐺 ∈ TarskiG )
tgbtwndiff.a ( 𝜑𝐴𝑃 )
tgbtwndiff.b ( 𝜑𝐵𝑃 )
tgldim0itv.c ( 𝜑𝐶𝑃 )
tgldim0itv.p ( 𝜑 → ( ♯ ‘ 𝑃 ) = 1 )
Assertion tgldim0itv ( 𝜑𝐴 ∈ ( 𝐵 𝐼 𝐶 ) )

Proof

Step Hyp Ref Expression
1 tgbtwndiff.p 𝑃 = ( Base ‘ 𝐺 )
2 tgbtwndiff.d = ( dist ‘ 𝐺 )
3 tgbtwndiff.i 𝐼 = ( Itv ‘ 𝐺 )
4 tgbtwndiff.g ( 𝜑𝐺 ∈ TarskiG )
5 tgbtwndiff.a ( 𝜑𝐴𝑃 )
6 tgbtwndiff.b ( 𝜑𝐵𝑃 )
7 tgldim0itv.c ( 𝜑𝐶𝑃 )
8 tgldim0itv.p ( 𝜑 → ( ♯ ‘ 𝑃 ) = 1 )
9 1 8 5 6 tgldim0eq ( 𝜑𝐴 = 𝐵 )
10 1 2 3 4 6 7 tgbtwntriv1 ( 𝜑𝐵 ∈ ( 𝐵 𝐼 𝐶 ) )
11 9 10 eqeltrd ( 𝜑𝐴 ∈ ( 𝐵 𝐼 𝐶 ) )