Theorem axtgcgrid

Description: Axiom of identity of congruence, Axiom A3 of Schwabhauser p. 10. (Contributed by Thierry Arnoux, 14-Mar-2019)

	Ref	Expression
Hypotheses	axtrkg.p	$$⊢P={\mathrm{Base}}_G$$
	axtrkg.d	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
	axtrkg.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
	axtrkg.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
	axtgcgrid.1	$$⊢\phi \to X\in P$$
	axtgcgrid.2	$$⊢\phi \to Y\in P$$
	axtgcgrid.3	$$⊢\phi \to Z\in P$$
	axtgcgrid.4	$$⊢\phi \to X\underset{\dot{}}{-}Y=Z\underset{\dot{}}{-}Z$$
Assertion	axtgcgrid	$$⊢\phi \to X=Y$$

Proof

Step	Hyp	Ref	Expression
1		axtrkg.p	$$⊢P={\mathrm{Base}}_G$$
2		axtrkg.d	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
3		axtrkg.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
4		axtrkg.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
5		axtgcgrid.1	$$⊢\phi \to X\in P$$
6		axtgcgrid.2	$$⊢\phi \to Y\in P$$
7		axtgcgrid.3	$$⊢\phi \to Z\in P$$
8		axtgcgrid.4	$$⊢\phi \to X\underset{\dot{}}{-}Y=Z\underset{\dot{}}{-}Z$$
9		df-trkg	$$⊢{𝒢}_{\mathrm{Tarski}}=\left({𝒢}_{\mathrm{Tarski}}^C\cap {𝒢}_{\mathrm{Tarski}}^B\right)\cap \left({𝒢}_{\mathrm{Tarski}}^{\mathrm{CB}}\cap \left\{f|\underset{\dot{}}{[}{\mathrm{Base}}_f/p\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{Itv}\left(f\right)/i\underset{\dot{}}{]}{Line}_{𝒢}\left(f\right)=\left(x\in p,y\in \left(p\setminus \left\{x\right\}\right)⟼\left\{z\in p|\left(z\in \left(xiy\right)\vee x\in \left(ziy\right)\vee y\in \left(xiz\right)\right)\right\}\right)\right\}\right)$$
10		inss1	$$⊢\left({𝒢}_{\mathrm{Tarski}}^C\cap {𝒢}_{\mathrm{Tarski}}^B\right)\cap \left({𝒢}_{\mathrm{Tarski}}^{\mathrm{CB}}\cap \left\{f|\underset{\dot{}}{[}{\mathrm{Base}}_f/p\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{Itv}\left(f\right)/i\underset{\dot{}}{]}{Line}_{𝒢}\left(f\right)=\left(x\in p,y\in \left(p\setminus \left\{x\right\}\right)⟼\left\{z\in p|\left(z\in \left(xiy\right)\vee x\in \left(ziy\right)\vee y\in \left(xiz\right)\right)\right\}\right)\right\}\right)\subseteq {𝒢}_{\mathrm{Tarski}}^C\cap {𝒢}_{\mathrm{Tarski}}^B$$
11		inss1	$$⊢{𝒢}_{\mathrm{Tarski}}^C\cap {𝒢}_{\mathrm{Tarski}}^B\subseteq {𝒢}_{\mathrm{Tarski}}^C$$
12	10 11	sstri	$$⊢\left({𝒢}_{\mathrm{Tarski}}^C\cap {𝒢}_{\mathrm{Tarski}}^B\right)\cap \left({𝒢}_{\mathrm{Tarski}}^{\mathrm{CB}}\cap \left\{f|\underset{\dot{}}{[}{\mathrm{Base}}_f/p\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{Itv}\left(f\right)/i\underset{\dot{}}{]}{Line}_{𝒢}\left(f\right)=\left(x\in p,y\in \left(p\setminus \left\{x\right\}\right)⟼\left\{z\in p|\left(z\in \left(xiy\right)\vee x\in \left(ziy\right)\vee y\in \left(xiz\right)\right)\right\}\right)\right\}\right)\subseteq {𝒢}_{\mathrm{Tarski}}^C$$
13	9 12	eqsstri	$$⊢{𝒢}_{\mathrm{Tarski}}\subseteq {𝒢}_{\mathrm{Tarski}}^C$$
14	13 4	sseldi	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}^C$$
15	1 2 3	istrkgc	$$⊢G\in {𝒢}_{\mathrm{Tarski}}^C\leftrightarrow \left(G\in \mathrm{V}\wedge \left(\forall x\in P\forall y\in Px\underset{\dot{}}{-}y=y\underset{\dot{}}{-}x\wedge \forall x\in P\forall y\in P\forall z\in P\left(x\underset{\dot{}}{-}y=z\underset{\dot{}}{-}z\to x=y\right)\right)\right)$$
16	15	simprbi	$$⊢G\in {𝒢}_{\mathrm{Tarski}}^C\to \left(\forall x\in P\forall y\in Px\underset{\dot{}}{-}y=y\underset{\dot{}}{-}x\wedge \forall x\in P\forall y\in P\forall z\in P\left(x\underset{\dot{}}{-}y=z\underset{\dot{}}{-}z\to x=y\right)\right)$$
17	16	simprd	$$⊢G\in {𝒢}_{\mathrm{Tarski}}^C\to \forall x\in P\forall y\in P\forall z\in P\left(x\underset{\dot{}}{-}y=z\underset{\dot{}}{-}z\to x=y\right)$$
18	14 17	syl	$$⊢\phi \to \forall x\in P\forall y\in P\forall z\in P\left(x\underset{\dot{}}{-}y=z\underset{\dot{}}{-}z\to x=y\right)$$
19		oveq1	$$⊢x=X\to x\underset{\dot{}}{-}y=X\underset{\dot{}}{-}y$$
20	19	eqeq1d	$$⊢x=X\to \left(x\underset{\dot{}}{-}y=z\underset{\dot{}}{-}z\leftrightarrow X\underset{\dot{}}{-}y=z\underset{\dot{}}{-}z\right)$$
21		eqeq1	$$⊢x=X\to \left(x=y\leftrightarrow X=y\right)$$
22	20 21	imbi12d	$$⊢x=X\to \left(\left(x\underset{\dot{}}{-}y=z\underset{\dot{}}{-}z\to x=y\right)\leftrightarrow \left(X\underset{\dot{}}{-}y=z\underset{\dot{}}{-}z\to X=y\right)\right)$$
23		oveq2	$$⊢y=Y\to X\underset{\dot{}}{-}y=X\underset{\dot{}}{-}Y$$
24	23	eqeq1d	$$⊢y=Y\to \left(X\underset{\dot{}}{-}y=z\underset{\dot{}}{-}z\leftrightarrow X\underset{\dot{}}{-}Y=z\underset{\dot{}}{-}z\right)$$
25		eqeq2	$$⊢y=Y\to \left(X=y\leftrightarrow X=Y\right)$$
26	24 25	imbi12d	$$⊢y=Y\to \left(\left(X\underset{\dot{}}{-}y=z\underset{\dot{}}{-}z\to X=y\right)\leftrightarrow \left(X\underset{\dot{}}{-}Y=z\underset{\dot{}}{-}z\to X=Y\right)\right)$$
27		id	$$⊢z=Z\to z=Z$$
28	27 27	oveq12d	$$⊢z=Z\to z\underset{\dot{}}{-}z=Z\underset{\dot{}}{-}Z$$
29	28	eqeq2d	$$⊢z=Z\to \left(X\underset{\dot{}}{-}Y=z\underset{\dot{}}{-}z\leftrightarrow X\underset{\dot{}}{-}Y=Z\underset{\dot{}}{-}Z\right)$$
30	29	imbi1d	$$⊢z=Z\to \left(\left(X\underset{\dot{}}{-}Y=z\underset{\dot{}}{-}z\to X=Y\right)\leftrightarrow \left(X\underset{\dot{}}{-}Y=Z\underset{\dot{}}{-}Z\to X=Y\right)\right)$$
31	22 26 30	rspc3v	$$⊢\left(X\in P\wedge Y\in P\wedge Z\in P\right)\to \left(\forall x\in P\forall y\in P\forall z\in P\left(x\underset{\dot{}}{-}y=z\underset{\dot{}}{-}z\to x=y\right)\to \left(X\underset{\dot{}}{-}Y=Z\underset{\dot{}}{-}Z\to X=Y\right)\right)$$
32	5 6 7 31	syl3anc	$$⊢\phi \to \left(\forall x\in P\forall y\in P\forall z\in P\left(x\underset{\dot{}}{-}y=z\underset{\dot{}}{-}z\to x=y\right)\to \left(X\underset{\dot{}}{-}Y=Z\underset{\dot{}}{-}Z\to X=Y\right)\right)$$
33	18 8 32	mp2d	$$⊢\phi \to X=Y$$