Theorem axtgcgrrflx

Description: Axiom of reflexivity of congruence, Axiom A1 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}}$$
	axtgcgrrflx.1	$$⊢\phi \to X\in P$$
	axtgcgrrflx.2	$$⊢\phi \to Y\in P$$
Assertion	axtgcgrrflx	$$⊢\phi \to X\underset{\dot{}}{-}Y=Y\underset{\dot{}}{-}X$$

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		axtgcgrrflx.1	$$⊢\phi \to X\in P$$
6		axtgcgrrflx.2	$$⊢\phi \to Y\in P$$
7		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)$$
8		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$$
9		inss1	$$⊢{𝒢}_{\mathrm{Tarski}}^C\cap {𝒢}_{\mathrm{Tarski}}^B\subseteq {𝒢}_{\mathrm{Tarski}}^C$$
10	8 9	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$$
11	7 10	eqsstri	$$⊢{𝒢}_{\mathrm{Tarski}}\subseteq {𝒢}_{\mathrm{Tarski}}^C$$
12	11 4	sseldi	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}^C$$
13	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)$$
14	13	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)$$
15	14	simpld	$$⊢G\in {𝒢}_{\mathrm{Tarski}}^C\to \forall x\in P\forall y\in Px\underset{\dot{}}{-}y=y\underset{\dot{}}{-}x$$
16	12 15	syl	$$⊢\phi \to \forall x\in P\forall y\in Px\underset{\dot{}}{-}y=y\underset{\dot{}}{-}x$$
17		oveq1	$$⊢x=X\to x\underset{\dot{}}{-}y=X\underset{\dot{}}{-}y$$
18		oveq2	$$⊢x=X\to y\underset{\dot{}}{-}x=y\underset{\dot{}}{-}X$$
19	17 18	eqeq12d	$$⊢x=X\to \left(x\underset{\dot{}}{-}y=y\underset{\dot{}}{-}x\leftrightarrow X\underset{\dot{}}{-}y=y\underset{\dot{}}{-}X\right)$$
20		oveq2	$$⊢y=Y\to X\underset{\dot{}}{-}y=X\underset{\dot{}}{-}Y$$
21		oveq1	$$⊢y=Y\to y\underset{\dot{}}{-}X=Y\underset{\dot{}}{-}X$$
22	20 21	eqeq12d	$$⊢y=Y\to \left(X\underset{\dot{}}{-}y=y\underset{\dot{}}{-}X\leftrightarrow X\underset{\dot{}}{-}Y=Y\underset{\dot{}}{-}X\right)$$
23	19 22	rspc2v	$$⊢\left(X\in P\wedge Y\in P\right)\to \left(\forall x\in P\forall y\in Px\underset{\dot{}}{-}y=y\underset{\dot{}}{-}x\to X\underset{\dot{}}{-}Y=Y\underset{\dot{}}{-}X\right)$$
24	5 6 23	syl2anc	$$⊢\phi \to \left(\forall x\in P\forall y\in Px\underset{\dot{}}{-}y=y\underset{\dot{}}{-}x\to X\underset{\dot{}}{-}Y=Y\underset{\dot{}}{-}X\right)$$
25	16 24	mpd	$$⊢\phi \to X\underset{\dot{}}{-}Y=Y\underset{\dot{}}{-}X$$