Theorem tgldim0eq

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

	Ref	Expression
Hypotheses	tgldim0.g	⊢ 𝑃 = ( 𝐸 ‘ 𝐹 )
	tgldim0.p	⊢ ( 𝜑 → ( ♯ ‘ 𝑃 ) = 1 )
	tgldim0.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
	tgldim0.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
Assertion	tgldim0eq	⊢ ( 𝜑 → 𝐴 = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		tgldim0.g	⊢ 𝑃 = ( 𝐸 ‘ 𝐹 )
2		tgldim0.p	⊢ ( 𝜑 → ( ♯ ‘ 𝑃 ) = 1 )
3		tgldim0.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
4		tgldim0.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
5	1	fvexi	⊢ 𝑃 ∈ V
6		hash1snb	⊢ ( 𝑃 ∈ V → ( ( ♯ ‘ 𝑃 ) = 1 ↔ ∃ 𝑥 𝑃 = { 𝑥 } ) )
7	5 6	ax-mp	⊢ ( ( ♯ ‘ 𝑃 ) = 1 ↔ ∃ 𝑥 𝑃 = { 𝑥 } )
8	2 7	sylib	⊢ ( 𝜑 → ∃ 𝑥 𝑃 = { 𝑥 } )
9	3	adantr	⊢ ( ( 𝜑 ∧ 𝑃 = { 𝑥 } ) → 𝐴 ∈ 𝑃 )
10		simpr	⊢ ( ( 𝜑 ∧ 𝑃 = { 𝑥 } ) → 𝑃 = { 𝑥 } )
11	9 10	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑃 = { 𝑥 } ) → 𝐴 ∈ { 𝑥 } )
12		elsni	⊢ ( 𝐴 ∈ { 𝑥 } → 𝐴 = 𝑥 )
13	11 12	syl	⊢ ( ( 𝜑 ∧ 𝑃 = { 𝑥 } ) → 𝐴 = 𝑥 )
14	4	adantr	⊢ ( ( 𝜑 ∧ 𝑃 = { 𝑥 } ) → 𝐵 ∈ 𝑃 )
15	14 10	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑃 = { 𝑥 } ) → 𝐵 ∈ { 𝑥 } )
16		elsni	⊢ ( 𝐵 ∈ { 𝑥 } → 𝐵 = 𝑥 )
17	15 16	syl	⊢ ( ( 𝜑 ∧ 𝑃 = { 𝑥 } ) → 𝐵 = 𝑥 )
18	13 17	eqtr4d	⊢ ( ( 𝜑 ∧ 𝑃 = { 𝑥 } ) → 𝐴 = 𝐵 )
19	8 18	exlimddv	⊢ ( 𝜑 → 𝐴 = 𝐵 )