miriso

Description: The point inversion function is an isometry, i.e. it is conserves congruence. Because it is also a bijection, it is also a motion. Theorem 7.13 of Schwabhauser p. 50. (Contributed by Thierry Arnoux, 6-Jun-2019)

	Ref	Expression
Hypotheses	mirval.p	$⊢ P = {Base}_{G}$
	mirval.d	$⊢ \underset{˙}{-} = dist (G)$
	mirval.i	$⊢ I = Itv (G)$
	mirval.l	$⊢ L = {Line}_{𝒢} (G)$
	mirval.s	$⊢ S = {pInv}_{𝒢} (G)$
	mirval.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	mirval.a	$⊢ φ \to A \in P$
	mirfv.m	$⊢ M = S (A)$
	miriso.1	$⊢ φ \to X \in P$
	miriso.2	$⊢ φ \to Y \in P$
Assertion	miriso	$⊢ φ \to M (X) \underset{˙}{-} M (Y) = X \underset{˙}{-} Y$

Proof

Step	Hyp	Ref	Expression
1		mirval.p	$⊢ P = {Base}_{G}$
2		mirval.d	$⊢ \underset{˙}{-} = dist (G)$
3		mirval.i	$⊢ I = Itv (G)$
4		mirval.l	$⊢ L = {Line}_{𝒢} (G)$
5		mirval.s	$⊢ S = {pInv}_{𝒢} (G)$
6		mirval.g	$⊢ φ \to G \in 𝒢_{Tarski}$
7		mirval.a	$⊢ φ \to A \in P$
8		mirfv.m	$⊢ M = S (A)$
9		miriso.1	$⊢ φ \to X \in P$
10		miriso.2	$⊢ φ \to Y \in P$
11		simpr	$⊢ (φ \land X = A) \to X = A$
12	11	oveq1d	$⊢ (φ \land X = A) \to X \underset{˙}{-} Y = A \underset{˙}{-} Y$
13	6	adantr	$⊢ (φ \land X = A) \to G \in 𝒢_{Tarski}$
14	7	adantr	$⊢ (φ \land X = A) \to A \in P$
15	10	adantr	$⊢ (φ \land X = A) \to Y \in P$
16	1 2 3 4 5 13 14 8 15	mircgr	$⊢ (φ \land X = A) \to A \underset{˙}{-} M (Y) = A \underset{˙}{-} Y$
17	9	adantr	$⊢ (φ \land X = A) \to X \in P$
18	11	eqcomd	$⊢ (φ \land X = A) \to A = X$
19	18	oveq2d	$⊢ (φ \land X = A) \to A \underset{˙}{-} A = A \underset{˙}{-} X$
20	1 2 3 13 14 17	tgbtwntriv1	$⊢ (φ \land X = A) \to A \in (A I X)$
21	1 2 3 4 5 13 14 8 17 14 19 20	ismir	$⊢ (φ \land X = A) \to A = M (X)$
22	21	oveq1d	$⊢ (φ \land X = A) \to A \underset{˙}{-} M (Y) = M (X) \underset{˙}{-} M (Y)$
23	12 16 22	3eqtr2rd	$⊢ (φ \land X = A) \to M (X) \underset{˙}{-} M (Y) = X \underset{˙}{-} Y$
24	6	adantr	$⊢ (φ \land X \neq A) \to G \in 𝒢_{Tarski}$
25	24	ad2antrr	$⊢ (((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \to G \in 𝒢_{Tarski}$
26	25	ad6antr	$⊢ (((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \to G \in 𝒢_{Tarski}$
27		simplr	$⊢ (((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \to x \in P$
28	27	ad6antr	$⊢ (((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \to x \in P$
29	9	adantr	$⊢ (φ \land X \neq A) \to X \in P$
30	29	ad8antr	$⊢ (((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \to X \in P$
31	7	adantr	$⊢ (φ \land X \neq A) \to A \in P$
32	31	ad2antrr	$⊢ (((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \to A \in P$
33	32	ad6antr	$⊢ (((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \to A \in P$
34	10	adantr	$⊢ (φ \land X \neq A) \to Y \in P$
35	34	ad2antrr	$⊢ (((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \to Y \in P$
36	35	ad6antr	$⊢ (((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \to Y \in P$
37		simp-4r	$⊢ (((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \to z \in P$
38	1 2 3 4 5 24 31 8 29	mircl	$⊢ (φ \land X \neq A) \to M (X) \in P$
39	38	ad2antrr	$⊢ (((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \to M (X) \in P$
40	39	ad6antr	$⊢ (((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \to M (X) \in P$
41	1 2 3 4 5 24 31 8 34	mircl	$⊢ (φ \land X \neq A) \to M (Y) \in P$
42	41	ad8antr	$⊢ (((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \to M (Y) \in P$
43	1 2 3 4 5 26 33 8 30	mirbtwn	$⊢ (((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \to A \in (M (X) I X)$
44		simp-7r	$⊢ (((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \to (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)$
45	44	simpld	$⊢ (((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \to X \in (M (X) I x)$
46	1 2 3 26 40 33 30 28 43 45	tgbtwnexch3	$⊢ (((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \to X \in (A I x)$
47	1 2 3 26 33 30 28 46	tgbtwncom	$⊢ (((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \to X \in (x I A)$
48	1 2 3 26 40 30 28 45	tgbtwncom	$⊢ (((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \to X \in (x I M (X))$
49	1 2 3 26 40 33 30 43	tgbtwncom	$⊢ (((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \to A \in (X I M (X))$
50	1 2 3 26 28 30 33 40 48 49	tgbtwnexch2	$⊢ (((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \to A \in (x I M (X))$
51		simpllr	$⊢ (((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \to (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)$
52	51	simpld	$⊢ (((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \to M (X) \in (x I z)$
53	1 2 3 26 28 33 40 37 50 52	tgbtwnexch3	$⊢ (((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \to M (X) \in (A I z)$
54	1 2 3 26 33 40 37 53	tgbtwncom	$⊢ (((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \to M (X) \in (z I A)$
55		simp-4r	$⊢ (((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \to y \in P$
56	55	ad2antrr	$⊢ (((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \to y \in P$
57	1 2 3 4 5 26 33 8 36	mirbtwn	$⊢ (((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \to A \in (M (Y) I Y)$
58		simp-5r	$⊢ (((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \to (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)$
59	58	simpld	$⊢ (((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \to Y \in (M (Y) I y)$
60	1 2 3 26 42 33 36 56 57 59	tgbtwnexch3	$⊢ (((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \to Y \in (A I y)$
61	1 2 3 26 33 36 56 60	tgbtwncom	$⊢ (((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \to Y \in (y I A)$
62	1 2 3 4 5 26 33 8 30	mircgr	$⊢ (((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \to A \underset{˙}{-} M (X) = A \underset{˙}{-} X$
63	58	simprd	$⊢ (((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \to Y \underset{˙}{-} y = X \underset{˙}{-} A$
64	1 2 3 26 36 56 30 33 63	tgcgrcomlr	$⊢ (((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \to y \underset{˙}{-} Y = A \underset{˙}{-} X$
65	62 64	eqtr4d	$⊢ (((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \to A \underset{˙}{-} M (X) = y \underset{˙}{-} Y$
66	51	simprd	$⊢ (((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \to M (X) \underset{˙}{-} z = Y \underset{˙}{-} A$
67	1 2 3 26 33 40 37 56 36 33 53 61 65 66	tgcgrextend	$⊢ (((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \to A \underset{˙}{-} z = y \underset{˙}{-} A$
68	44	simprd	$⊢ (((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \to X \underset{˙}{-} x = Y \underset{˙}{-} A$
69	68	eqcomd	$⊢ (((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \to Y \underset{˙}{-} A = X \underset{˙}{-} x$
70	1 2 3 26 56 36 33 33 30 28 61 46 64 69	tgcgrextend	$⊢ (((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \to y \underset{˙}{-} A = A \underset{˙}{-} x$
71	67 70	eqtr2d	$⊢ (((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \to A \underset{˙}{-} x = A \underset{˙}{-} z$
72	1 2 3 26 33 28 33 37 71	tgcgrcomlr	$⊢ (((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \to x \underset{˙}{-} A = z \underset{˙}{-} A$
73	62	eqcomd	$⊢ (((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \to A \underset{˙}{-} X = A \underset{˙}{-} M (X)$
74	1 2 3 26 33 30 33 40 73	tgcgrcomlr	$⊢ (((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \to X \underset{˙}{-} A = M (X) \underset{˙}{-} A$
75		simplr	$⊢ (((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \to t \in P$
76	1 2 3 26 42 36 56 59	tgbtwncom	$⊢ (((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \to Y \in (y I M (Y))$
77	1 2 3 26 42 33 36 57	tgbtwncom	$⊢ (((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \to A \in (Y I M (Y))$
78	1 2 3 26 56 36 33 42 76 77	tgbtwnexch2	$⊢ (((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \to A \in (y I M (Y))$
79		simpr	$⊢ (((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \to (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)$
80	79	simpld	$⊢ (((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \to M (Y) \in (y I t)$
81	1 2 3 26 56 33 42 75 78 80	tgbtwnexch3	$⊢ (((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \to M (Y) \in (A I t)$
82	1 2 3 26 33 42 75 81	tgbtwncom	$⊢ (((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \to M (Y) \in (t I A)$
83	1 2 3 26 30 28 36 33 68	tgcgrcomlr	$⊢ (((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \to x \underset{˙}{-} X = A \underset{˙}{-} Y$
84	1 2 3 4 5 26 33 8 36	mircgr	$⊢ (((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \to A \underset{˙}{-} M (Y) = A \underset{˙}{-} Y$
85	83 84	eqtr4d	$⊢ (((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \to x \underset{˙}{-} X = A \underset{˙}{-} M (Y)$
86	79	simprd	$⊢ (((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \to M (Y) \underset{˙}{-} t = X \underset{˙}{-} A$
87	86	eqcomd	$⊢ (((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \to X \underset{˙}{-} A = M (Y) \underset{˙}{-} t$
88	1 2 3 26 28 30 33 33 42 75 47 81 85 87	tgcgrextend	$⊢ (((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \to x \underset{˙}{-} A = A \underset{˙}{-} t$
89	1 2 3 26 33 75	axtgcgrrflx	$⊢ (((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \to A \underset{˙}{-} t = t \underset{˙}{-} A$
90	88 89	eqtrd	$⊢ (((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \to x \underset{˙}{-} A = t \underset{˙}{-} A$
91	1 2 3 26 28 33 75 33 90	tgcgrcomlr	$⊢ (((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \to A \underset{˙}{-} x = A \underset{˙}{-} t$
92	70 91 89	3eqtrd	$⊢ (((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \to y \underset{˙}{-} A = t \underset{˙}{-} A$
93	1 2 3 26 33 42 33 36 84	tgcgrcomlr	$⊢ (((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \to M (Y) \underset{˙}{-} A = Y \underset{˙}{-} A$
94	93	eqcomd	$⊢ (((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \to Y \underset{˙}{-} A = M (Y) \underset{˙}{-} A$
95	1 2 3 26 75 37	axtgcgrrflx	$⊢ (((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \to t \underset{˙}{-} z = z \underset{˙}{-} t$
96		simp-9r	$⊢ (((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \to X \neq A$
97	96	neneqd	$⊢ (((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \to \neg X = A$
98	26	adantr	$⊢ ((((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \land x = A) \to G \in 𝒢_{Tarski}$
99	33	adantr	$⊢ ((((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \land x = A) \to A \in P$
100	30	adantr	$⊢ ((((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \land x = A) \to X \in P$
101	46	adantr	$⊢ ((((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \land x = A) \to X \in (A I x)$
102		simpr	$⊢ ((((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \land x = A) \to x = A$
103	102	oveq2d	$⊢ ((((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \land x = A) \to A I x = A I A$
104	101 103	eleqtrd	$⊢ ((((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \land x = A) \to X \in (A I A)$
105	1 2 3 98 99 100 104	axtgbtwnid	$⊢ ((((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \land x = A) \to A = X$
106	105	eqcomd	$⊢ ((((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \land x = A) \to X = A$
107	97 106	mtand	$⊢ (((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \to \neg x = A$
108	107	neqned	$⊢ (((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \to x \neq A$
109	1 2 3 26 28 33 40 37 50 52	tgbtwnexch	$⊢ (((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \to A \in (x I z)$
110	1 2 3 26 56 33 42 75 78 80	tgbtwnexch	$⊢ (((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \to A \in (y I t)$
111	1 2 3 26 56 33 75 110	tgbtwncom	$⊢ (((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \to A \in (t I y)$
112	1 2 3 26 56 33	axtgcgrrflx	$⊢ (((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \to y \underset{˙}{-} A = A \underset{˙}{-} y$
113	67 112	eqtrd	$⊢ (((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \to A \underset{˙}{-} z = A \underset{˙}{-} y$
114	1 2 3 26 28 75	axtgcgrrflx	$⊢ (((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \to x \underset{˙}{-} t = t \underset{˙}{-} x$
115	91	eqcomd	$⊢ (((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \to A \underset{˙}{-} t = A \underset{˙}{-} x$
116	1 2 3 26 28 33 37 75 33 56 75 28 108 109 111 90 113 114 115	axtg5seg	$⊢ (((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \to z \underset{˙}{-} t = y \underset{˙}{-} x$
117	95 116	eqtr2d	$⊢ (((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \to y \underset{˙}{-} x = t \underset{˙}{-} z$
118	1 2 3 26 56 36 33 28 75 42 33 37 61 82 92 94 117 71	tgifscgr	$⊢ (((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \to Y \underset{˙}{-} x = M (Y) \underset{˙}{-} z$
119	1 2 3 26 36 28 42 37 118	tgcgrcomlr	$⊢ (((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \to x \underset{˙}{-} Y = z \underset{˙}{-} M (Y)$
120	84	eqcomd	$⊢ (((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \to A \underset{˙}{-} Y = A \underset{˙}{-} M (Y)$
121	1 2 3 26 28 30 33 36 37 40 33 42 47 54 72 74 119 120	tgifscgr	$⊢ (((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \to X \underset{˙}{-} Y = M (X) \underset{˙}{-} M (Y)$
122	121	eqcomd	$⊢ (((((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \land t \in P) \land (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)) \to M (X) \underset{˙}{-} M (Y) = X \underset{˙}{-} Y$
123		simp-6l	$⊢ (((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \to (φ \land X \neq A)$
124		simpllr	$⊢ (((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \to (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)$
125	24	ad2antrr	$⊢ (((φ \land X \neq A) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \to G \in 𝒢_{Tarski}$
126		simplr	$⊢ (((φ \land X \neq A) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \to y \in P$
127	41	ad2antrr	$⊢ (((φ \land X \neq A) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \to M (Y) \in P$
128	29	ad2antrr	$⊢ (((φ \land X \neq A) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \to X \in P$
129	31	ad2antrr	$⊢ (((φ \land X \neq A) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \to A \in P$
130	1 2 3 125 126 127 128 129	axtgsegcon	$⊢ (((φ \land X \neq A) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \to \exists t \in P (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)$
131	123 55 124 130	syl21anc	$⊢ (((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \to \exists t \in P (M (Y) \in (y I t) \land M (Y) \underset{˙}{-} t = X \underset{˙}{-} A)$
132	122 131	r19.29a	$⊢ (((((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \land z \in P) \land (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)) \to M (X) \underset{˙}{-} M (Y) = X \underset{˙}{-} Y$
133	1 2 3 25 27 39 35 32	axtgsegcon	$⊢ (((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \to \exists z \in P (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)$
134	133	ad2antrr	$⊢ (((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \to \exists z \in P (M (X) \in (x I z) \land M (X) \underset{˙}{-} z = Y \underset{˙}{-} A)$
135	132 134	r19.29a	$⊢ (((((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \land y \in P) \land (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)) \to M (X) \underset{˙}{-} M (Y) = X \underset{˙}{-} Y$
136	1 2 3 24 41 34 29 31	axtgsegcon	$⊢ (φ \land X \neq A) \to \exists y \in P (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)$
137	136	ad2antrr	$⊢ (((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \to \exists y \in P (Y \in (M (Y) I y) \land Y \underset{˙}{-} y = X \underset{˙}{-} A)$
138	135 137	r19.29a	$⊢ (((φ \land X \neq A) \land x \in P) \land (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)) \to M (X) \underset{˙}{-} M (Y) = X \underset{˙}{-} Y$
139	1 2 3 24 38 29 34 31	axtgsegcon	$⊢ (φ \land X \neq A) \to \exists x \in P (X \in (M (X) I x) \land X \underset{˙}{-} x = Y \underset{˙}{-} A)$
140	138 139	r19.29a	$⊢ (φ \land X \neq A) \to M (X) \underset{˙}{-} M (Y) = X \underset{˙}{-} Y$
141	23 140	pm2.61dane	$⊢ φ \to M (X) \underset{˙}{-} M (Y) = X \underset{˙}{-} Y$

Metamath Proof Explorer

Theorem miriso

Proof