Theorem tgldim0eq

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

	Ref	Expression
Hypotheses	tgldim0.g	$$⊢P=E\left(F\right)$$
	tgldim0.p	$$⊢\phi \to \left|P\right|=1$$
	tgldim0.a	$$⊢\phi \to A\in P$$
	tgldim0.b	$$⊢\phi \to B\in P$$
Assertion	tgldim0eq	$$⊢\phi \to A=B$$

Proof

Step	Hyp	Ref	Expression
1		tgldim0.g	$$⊢P=E\left(F\right)$$
2		tgldim0.p	$$⊢\phi \to \left|P\right|=1$$
3		tgldim0.a	$$⊢\phi \to A\in P$$
4		tgldim0.b	$$⊢\phi \to B\in P$$
5	1	fvexi	$$⊢P\in \mathrm{V}$$
6		hash1snb	$$⊢P\in \mathrm{V}\to \left(\left|P\right|=1\leftrightarrow \exists xP=\left\{x\right\}\right)$$
7	5 6	ax-mp	$$⊢\left|P\right|=1\leftrightarrow \exists xP=\left\{x\right\}$$
8	2 7	sylib	$$⊢\phi \to \exists xP=\left\{x\right\}$$
9	3	adantr	$$⊢\left(\phi \wedge P=\left\{x\right\}\right)\to A\in P$$
10		simpr	$$⊢\left(\phi \wedge P=\left\{x\right\}\right)\to P=\left\{x\right\}$$
11	9 10	eleqtrd	$$⊢\left(\phi \wedge P=\left\{x\right\}\right)\to A\in \left\{x\right\}$$
12		elsni	$$⊢A\in \left\{x\right\}\to A=x$$
13	11 12	syl	$$⊢\left(\phi \wedge P=\left\{x\right\}\right)\to A=x$$
14	4	adantr	$$⊢\left(\phi \wedge P=\left\{x\right\}\right)\to B\in P$$
15	14 10	eleqtrd	$$⊢\left(\phi \wedge P=\left\{x\right\}\right)\to B\in \left\{x\right\}$$
16		elsni	$$⊢B\in \left\{x\right\}\to B=x$$
17	15 16	syl	$$⊢\left(\phi \wedge P=\left\{x\right\}\right)\to B=x$$
18	13 17	eqtr4d	$$⊢\left(\phi \wedge P=\left\{x\right\}\right)\to A=B$$
19	8 18	exlimddv	$$⊢\phi \to A=B$$