eengtrkg

Description: The geometry structure for EE ^ N is a Tarski geometry. (Contributed by Thierry Arnoux, 15-Mar-2019)

		Ref	Expression
	Assertion	eengtrkg	$⊢ N \in ℕ \to 𝔼_{𝒢} (N) \in 𝒢_{Tarski}$

Proof

Step	Hyp	Ref	Expression
1		fvexd	$⊢ N \in ℕ \to 𝔼_{𝒢} (N) \in V$
2		simpl	$⊢ (N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \to N \in ℕ$
3		simprl	$⊢ (N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \to x \in {Base}_{𝔼_{𝒢} (N)}$
4		eengbas	$⊢ N \in ℕ \to 𝔼 (N) = {Base}_{𝔼_{𝒢} (N)}$
5	4	adantr	$⊢ (N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \to 𝔼 (N) = {Base}_{𝔼_{𝒢} (N)}$
6	3 5	eleqtrrd	$⊢ (N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \to x \in 𝔼 (N)$
7		simprr	$⊢ (N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \to y \in {Base}_{𝔼_{𝒢} (N)}$
8	7 5	eleqtrrd	$⊢ (N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \to y \in 𝔼 (N)$
9		axcgrrflx	$⊢ (N \in ℕ \land x \in 𝔼 (N) \land y \in 𝔼 (N)) \to ⟨x, y⟩ Cgr ⟨y, x⟩$
10	2 6 8 9	syl3anc	$⊢ (N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \to ⟨x, y⟩ Cgr ⟨y, x⟩$
11		eqid	$⊢ {Base}_{𝔼_{𝒢} (N)} = {Base}_{𝔼_{𝒢} (N)}$
12		eqid	$⊢ dist (𝔼_{𝒢} (N)) = dist (𝔼_{𝒢} (N))$
13	2 11 12 3 7 7 3	ecgrtg	$⊢ (N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \to (⟨x, y⟩ Cgr ⟨y, x⟩ \leftrightarrow x dist (𝔼_{𝒢} (N)) y = y dist (𝔼_{𝒢} (N)) x)$
14	10 13	mpbid	$⊢ (N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \to x dist (𝔼_{𝒢} (N)) y = y dist (𝔼_{𝒢} (N)) x$
15	14	ralrimivva	$⊢ N \in ℕ \to \forall x \in {Base}_{𝔼_{𝒢} (N)} \forall y \in {Base}_{𝔼_{𝒢} (N)} x dist (𝔼_{𝒢} (N)) y = y dist (𝔼_{𝒢} (N)) x$
16		simpl	$⊢ (N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)} \land z \in {Base}_{𝔼_{𝒢} (N)})) \to N \in ℕ$
17		simpr1	$⊢ (N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)} \land z \in {Base}_{𝔼_{𝒢} (N)})) \to x \in {Base}_{𝔼_{𝒢} (N)}$
18		simpr2	$⊢ (N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)} \land z \in {Base}_{𝔼_{𝒢} (N)})) \to y \in {Base}_{𝔼_{𝒢} (N)}$
19		simpr3	$⊢ (N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)} \land z \in {Base}_{𝔼_{𝒢} (N)})) \to z \in {Base}_{𝔼_{𝒢} (N)}$
20	16 11 12 17 18 19 19	ecgrtg	$⊢ (N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)} \land z \in {Base}_{𝔼_{𝒢} (N)})) \to (⟨x, y⟩ Cgr ⟨z, z⟩ \leftrightarrow x dist (𝔼_{𝒢} (N)) y = z dist (𝔼_{𝒢} (N)) z)$
21	6	3adantr3	$⊢ (N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)} \land z \in {Base}_{𝔼_{𝒢} (N)})) \to x \in 𝔼 (N)$
22	8	3adantr3	$⊢ (N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)} \land z \in {Base}_{𝔼_{𝒢} (N)})) \to y \in 𝔼 (N)$
23	4	adantr	$⊢ (N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)} \land z \in {Base}_{𝔼_{𝒢} (N)})) \to 𝔼 (N) = {Base}_{𝔼_{𝒢} (N)}$
24	19 23	eleqtrrd	$⊢ (N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)} \land z \in {Base}_{𝔼_{𝒢} (N)})) \to z \in 𝔼 (N)$
25		axcgrid	$⊢ (N \in ℕ \land (x \in 𝔼 (N) \land y \in 𝔼 (N) \land z \in 𝔼 (N))) \to (⟨x, y⟩ Cgr ⟨z, z⟩ \to x = y)$
26	16 21 22 24 25	syl13anc	$⊢ (N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)} \land z \in {Base}_{𝔼_{𝒢} (N)})) \to (⟨x, y⟩ Cgr ⟨z, z⟩ \to x = y)$
27	20 26	sylbird	$⊢ (N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)} \land z \in {Base}_{𝔼_{𝒢} (N)})) \to (x dist (𝔼_{𝒢} (N)) y = z dist (𝔼_{𝒢} (N)) z \to x = y)$
28	27	ralrimivvva	$⊢ N \in ℕ \to \forall x \in {Base}_{𝔼_{𝒢} (N)} \forall y \in {Base}_{𝔼_{𝒢} (N)} \forall z \in {Base}_{𝔼_{𝒢} (N)} (x dist (𝔼_{𝒢} (N)) y = z dist (𝔼_{𝒢} (N)) z \to x = y)$
29	1 15 28	jca32	$⊢ N \in ℕ \to (𝔼_{𝒢} (N) \in V \land (\forall x \in {Base}_{𝔼_{𝒢} (N)} \forall y \in {Base}_{𝔼_{𝒢} (N)} x dist (𝔼_{𝒢} (N)) y = y dist (𝔼_{𝒢} (N)) x \land \forall x \in {Base}_{𝔼_{𝒢} (N)} \forall y \in {Base}_{𝔼_{𝒢} (N)} \forall z \in {Base}_{𝔼_{𝒢} (N)} (x dist (𝔼_{𝒢} (N)) y = z dist (𝔼_{𝒢} (N)) z \to x = y)))$
30		eqid	$⊢ Itv (𝔼_{𝒢} (N)) = Itv (𝔼_{𝒢} (N))$
31	11 12 30	istrkgc	$⊢ 𝔼_{𝒢} (N) \in 𝒢_{Tarski}^{C} \leftrightarrow (𝔼_{𝒢} (N) \in V \land (\forall x \in {Base}_{𝔼_{𝒢} (N)} \forall y \in {Base}_{𝔼_{𝒢} (N)} x dist (𝔼_{𝒢} (N)) y = y dist (𝔼_{𝒢} (N)) x \land \forall x \in {Base}_{𝔼_{𝒢} (N)} \forall y \in {Base}_{𝔼_{𝒢} (N)} \forall z \in {Base}_{𝔼_{𝒢} (N)} (x dist (𝔼_{𝒢} (N)) y = z dist (𝔼_{𝒢} (N)) z \to x = y)))$
32	29 31	sylibr	$⊢ N \in ℕ \to 𝔼_{𝒢} (N) \in 𝒢_{Tarski}^{C}$
33	2 11 30 3 3 7	ebtwntg	$⊢ (N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \to (y Btwn ⟨x, x⟩ \leftrightarrow y \in (x Itv (𝔼_{𝒢} (N)) x))$
34		axbtwnid	$⊢ (N \in ℕ \land y \in 𝔼 (N) \land x \in 𝔼 (N)) \to (y Btwn ⟨x, x⟩ \to y = x)$
35	2 8 6 34	syl3anc	$⊢ (N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \to (y Btwn ⟨x, x⟩ \to y = x)$
36	33 35	sylbird	$⊢ (N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \to (y \in (x Itv (𝔼_{𝒢} (N)) x) \to y = x)$
37	36	imp	$⊢ ((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land y \in (x Itv (𝔼_{𝒢} (N)) x)) \to y = x$
38	37	equcomd	$⊢ ((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land y \in (x Itv (𝔼_{𝒢} (N)) x)) \to x = y$
39	38	ex	$⊢ (N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \to (y \in (x Itv (𝔼_{𝒢} (N)) x) \to x = y)$
40	39	ralrimivva	$⊢ N \in ℕ \to \forall x \in {Base}_{𝔼_{𝒢} (N)} \forall y \in {Base}_{𝔼_{𝒢} (N)} (y \in (x Itv (𝔼_{𝒢} (N)) x) \to x = y)$
41		simpll	$⊢ ((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (z \in {Base}_{𝔼_{𝒢} (N)} \land u \in {Base}_{𝔼_{𝒢} (N)} \land v \in {Base}_{𝔼_{𝒢} (N)})) \to N \in ℕ$
42	6	adantr	$⊢ ((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (z \in {Base}_{𝔼_{𝒢} (N)} \land u \in {Base}_{𝔼_{𝒢} (N)} \land v \in {Base}_{𝔼_{𝒢} (N)})) \to x \in 𝔼 (N)$
43	8	adantr	$⊢ ((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (z \in {Base}_{𝔼_{𝒢} (N)} \land u \in {Base}_{𝔼_{𝒢} (N)} \land v \in {Base}_{𝔼_{𝒢} (N)})) \to y \in 𝔼 (N)$
44	3	adantr	$⊢ ((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (z \in {Base}_{𝔼_{𝒢} (N)} \land u \in {Base}_{𝔼_{𝒢} (N)} \land v \in {Base}_{𝔼_{𝒢} (N)})) \to x \in {Base}_{𝔼_{𝒢} (N)}$
45	7	adantr	$⊢ ((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (z \in {Base}_{𝔼_{𝒢} (N)} \land u \in {Base}_{𝔼_{𝒢} (N)} \land v \in {Base}_{𝔼_{𝒢} (N)})) \to y \in {Base}_{𝔼_{𝒢} (N)}$
46		simpr1	$⊢ ((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (z \in {Base}_{𝔼_{𝒢} (N)} \land u \in {Base}_{𝔼_{𝒢} (N)} \land v \in {Base}_{𝔼_{𝒢} (N)})) \to z \in {Base}_{𝔼_{𝒢} (N)}$
47	41 44 45 46 24	syl13anc	$⊢ ((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (z \in {Base}_{𝔼_{𝒢} (N)} \land u \in {Base}_{𝔼_{𝒢} (N)} \land v \in {Base}_{𝔼_{𝒢} (N)})) \to z \in 𝔼 (N)$
48		simpr2	$⊢ ((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (z \in {Base}_{𝔼_{𝒢} (N)} \land u \in {Base}_{𝔼_{𝒢} (N)} \land v \in {Base}_{𝔼_{𝒢} (N)})) \to u \in {Base}_{𝔼_{𝒢} (N)}$
49	41 4	syl	$⊢ ((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (z \in {Base}_{𝔼_{𝒢} (N)} \land u \in {Base}_{𝔼_{𝒢} (N)} \land v \in {Base}_{𝔼_{𝒢} (N)})) \to 𝔼 (N) = {Base}_{𝔼_{𝒢} (N)}$
50	48 49	eleqtrrd	$⊢ ((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (z \in {Base}_{𝔼_{𝒢} (N)} \land u \in {Base}_{𝔼_{𝒢} (N)} \land v \in {Base}_{𝔼_{𝒢} (N)})) \to u \in 𝔼 (N)$
51		simpr3	$⊢ ((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (z \in {Base}_{𝔼_{𝒢} (N)} \land u \in {Base}_{𝔼_{𝒢} (N)} \land v \in {Base}_{𝔼_{𝒢} (N)})) \to v \in {Base}_{𝔼_{𝒢} (N)}$
52	51 49	eleqtrrd	$⊢ ((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (z \in {Base}_{𝔼_{𝒢} (N)} \land u \in {Base}_{𝔼_{𝒢} (N)} \land v \in {Base}_{𝔼_{𝒢} (N)})) \to v \in 𝔼 (N)$
53		axpasch	$⊢ (N \in ℕ \land (x \in 𝔼 (N) \land y \in 𝔼 (N) \land z \in 𝔼 (N)) \land (u \in 𝔼 (N) \land v \in 𝔼 (N))) \to ((u Btwn ⟨x, z⟩ \land v Btwn ⟨y, z⟩) \to \exists a \in 𝔼 (N) (a Btwn ⟨u, y⟩ \land a Btwn ⟨v, x⟩))$
54	41 42 43 47 50 52 53	syl132anc	$⊢ ((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (z \in {Base}_{𝔼_{𝒢} (N)} \land u \in {Base}_{𝔼_{𝒢} (N)} \land v \in {Base}_{𝔼_{𝒢} (N)})) \to ((u Btwn ⟨x, z⟩ \land v Btwn ⟨y, z⟩) \to \exists a \in 𝔼 (N) (a Btwn ⟨u, y⟩ \land a Btwn ⟨v, x⟩))$
55	41 11 30 44 46 48	ebtwntg	$⊢ ((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (z \in {Base}_{𝔼_{𝒢} (N)} \land u \in {Base}_{𝔼_{𝒢} (N)} \land v \in {Base}_{𝔼_{𝒢} (N)})) \to (u Btwn ⟨x, z⟩ \leftrightarrow u \in (x Itv (𝔼_{𝒢} (N)) z))$
56	41 11 30 45 46 51	ebtwntg	$⊢ ((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (z \in {Base}_{𝔼_{𝒢} (N)} \land u \in {Base}_{𝔼_{𝒢} (N)} \land v \in {Base}_{𝔼_{𝒢} (N)})) \to (v Btwn ⟨y, z⟩ \leftrightarrow v \in (y Itv (𝔼_{𝒢} (N)) z))$
57	55 56	anbi12d	$⊢ ((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (z \in {Base}_{𝔼_{𝒢} (N)} \land u \in {Base}_{𝔼_{𝒢} (N)} \land v \in {Base}_{𝔼_{𝒢} (N)})) \to ((u Btwn ⟨x, z⟩ \land v Btwn ⟨y, z⟩) \leftrightarrow (u \in (x Itv (𝔼_{𝒢} (N)) z) \land v \in (y Itv (𝔼_{𝒢} (N)) z)))$
58		simplll	$⊢ (((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (z \in {Base}_{𝔼_{𝒢} (N)} \land u \in {Base}_{𝔼_{𝒢} (N)} \land v \in {Base}_{𝔼_{𝒢} (N)})) \land a \in 𝔼 (N)) \to N \in ℕ$
59	48	adantr	$⊢ (((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (z \in {Base}_{𝔼_{𝒢} (N)} \land u \in {Base}_{𝔼_{𝒢} (N)} \land v \in {Base}_{𝔼_{𝒢} (N)})) \land a \in 𝔼 (N)) \to u \in {Base}_{𝔼_{𝒢} (N)}$
60	45	adantr	$⊢ (((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (z \in {Base}_{𝔼_{𝒢} (N)} \land u \in {Base}_{𝔼_{𝒢} (N)} \land v \in {Base}_{𝔼_{𝒢} (N)})) \land a \in 𝔼 (N)) \to y \in {Base}_{𝔼_{𝒢} (N)}$
61		simpr	$⊢ (((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (z \in {Base}_{𝔼_{𝒢} (N)} \land u \in {Base}_{𝔼_{𝒢} (N)} \land v \in {Base}_{𝔼_{𝒢} (N)})) \land a \in 𝔼 (N)) \to a \in 𝔼 (N)$
62	49	adantr	$⊢ (((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (z \in {Base}_{𝔼_{𝒢} (N)} \land u \in {Base}_{𝔼_{𝒢} (N)} \land v \in {Base}_{𝔼_{𝒢} (N)})) \land a \in 𝔼 (N)) \to 𝔼 (N) = {Base}_{𝔼_{𝒢} (N)}$
63	61 62	eleqtrd	$⊢ (((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (z \in {Base}_{𝔼_{𝒢} (N)} \land u \in {Base}_{𝔼_{𝒢} (N)} \land v \in {Base}_{𝔼_{𝒢} (N)})) \land a \in 𝔼 (N)) \to a \in {Base}_{𝔼_{𝒢} (N)}$
64	58 11 30 59 60 63	ebtwntg	$⊢ (((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (z \in {Base}_{𝔼_{𝒢} (N)} \land u \in {Base}_{𝔼_{𝒢} (N)} \land v \in {Base}_{𝔼_{𝒢} (N)})) \land a \in 𝔼 (N)) \to (a Btwn ⟨u, y⟩ \leftrightarrow a \in (u Itv (𝔼_{𝒢} (N)) y))$
65	51	adantr	$⊢ (((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (z \in {Base}_{𝔼_{𝒢} (N)} \land u \in {Base}_{𝔼_{𝒢} (N)} \land v \in {Base}_{𝔼_{𝒢} (N)})) \land a \in 𝔼 (N)) \to v \in {Base}_{𝔼_{𝒢} (N)}$
66	44	adantr	$⊢ (((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (z \in {Base}_{𝔼_{𝒢} (N)} \land u \in {Base}_{𝔼_{𝒢} (N)} \land v \in {Base}_{𝔼_{𝒢} (N)})) \land a \in 𝔼 (N)) \to x \in {Base}_{𝔼_{𝒢} (N)}$
67	58 11 30 65 66 63	ebtwntg	$⊢ (((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (z \in {Base}_{𝔼_{𝒢} (N)} \land u \in {Base}_{𝔼_{𝒢} (N)} \land v \in {Base}_{𝔼_{𝒢} (N)})) \land a \in 𝔼 (N)) \to (a Btwn ⟨v, x⟩ \leftrightarrow a \in (v Itv (𝔼_{𝒢} (N)) x))$
68	64 67	anbi12d	$⊢ (((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (z \in {Base}_{𝔼_{𝒢} (N)} \land u \in {Base}_{𝔼_{𝒢} (N)} \land v \in {Base}_{𝔼_{𝒢} (N)})) \land a \in 𝔼 (N)) \to ((a Btwn ⟨u, y⟩ \land a Btwn ⟨v, x⟩) \leftrightarrow (a \in (u Itv (𝔼_{𝒢} (N)) y) \land a \in (v Itv (𝔼_{𝒢} (N)) x)))$
69	49 68	rexeqbidva	$⊢ ((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (z \in {Base}_{𝔼_{𝒢} (N)} \land u \in {Base}_{𝔼_{𝒢} (N)} \land v \in {Base}_{𝔼_{𝒢} (N)})) \to (\exists a \in 𝔼 (N) (a Btwn ⟨u, y⟩ \land a Btwn ⟨v, x⟩) \leftrightarrow \exists a \in {Base}_{𝔼_{𝒢} (N)} (a \in (u Itv (𝔼_{𝒢} (N)) y) \land a \in (v Itv (𝔼_{𝒢} (N)) x)))$
70	54 57 69	3imtr3d	$⊢ ((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (z \in {Base}_{𝔼_{𝒢} (N)} \land u \in {Base}_{𝔼_{𝒢} (N)} \land v \in {Base}_{𝔼_{𝒢} (N)})) \to ((u \in (x Itv (𝔼_{𝒢} (N)) z) \land v \in (y Itv (𝔼_{𝒢} (N)) z)) \to \exists a \in {Base}_{𝔼_{𝒢} (N)} (a \in (u Itv (𝔼_{𝒢} (N)) y) \land a \in (v Itv (𝔼_{𝒢} (N)) x)))$
71	70	ralrimivvva	$⊢ (N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \to \forall z \in {Base}_{𝔼_{𝒢} (N)} \forall u \in {Base}_{𝔼_{𝒢} (N)} \forall v \in {Base}_{𝔼_{𝒢} (N)} ((u \in (x Itv (𝔼_{𝒢} (N)) z) \land v \in (y Itv (𝔼_{𝒢} (N)) z)) \to \exists a \in {Base}_{𝔼_{𝒢} (N)} (a \in (u Itv (𝔼_{𝒢} (N)) y) \land a \in (v Itv (𝔼_{𝒢} (N)) x)))$
72	71	ralrimivva	$⊢ N \in ℕ \to \forall x \in {Base}_{𝔼_{𝒢} (N)} \forall y \in {Base}_{𝔼_{𝒢} (N)} \forall z \in {Base}_{𝔼_{𝒢} (N)} \forall u \in {Base}_{𝔼_{𝒢} (N)} \forall v \in {Base}_{𝔼_{𝒢} (N)} ((u \in (x Itv (𝔼_{𝒢} (N)) z) \land v \in (y Itv (𝔼_{𝒢} (N)) z)) \to \exists a \in {Base}_{𝔼_{𝒢} (N)} (a \in (u Itv (𝔼_{𝒢} (N)) y) \land a \in (v Itv (𝔼_{𝒢} (N)) x)))$
73		simpl	$⊢ (N \in ℕ \land (s \in 𝒫 {Base}_{𝔼_{𝒢} (N)} \land t \in 𝒫 {Base}_{𝔼_{𝒢} (N)})) \to N \in ℕ$
74		elpwi	$⊢ s \in 𝒫 {Base}_{𝔼_{𝒢} (N)} \to s \subseteq {Base}_{𝔼_{𝒢} (N)}$
75	74	ad2antrl	$⊢ (N \in ℕ \land (s \in 𝒫 {Base}_{𝔼_{𝒢} (N)} \land t \in 𝒫 {Base}_{𝔼_{𝒢} (N)})) \to s \subseteq {Base}_{𝔼_{𝒢} (N)}$
76	4	adantr	$⊢ (N \in ℕ \land (s \in 𝒫 {Base}_{𝔼_{𝒢} (N)} \land t \in 𝒫 {Base}_{𝔼_{𝒢} (N)})) \to 𝔼 (N) = {Base}_{𝔼_{𝒢} (N)}$
77	75 76	sseqtrrd	$⊢ (N \in ℕ \land (s \in 𝒫 {Base}_{𝔼_{𝒢} (N)} \land t \in 𝒫 {Base}_{𝔼_{𝒢} (N)})) \to s \subseteq 𝔼 (N)$
78		elpwi	$⊢ t \in 𝒫 {Base}_{𝔼_{𝒢} (N)} \to t \subseteq {Base}_{𝔼_{𝒢} (N)}$
79	78	ad2antll	$⊢ (N \in ℕ \land (s \in 𝒫 {Base}_{𝔼_{𝒢} (N)} \land t \in 𝒫 {Base}_{𝔼_{𝒢} (N)})) \to t \subseteq {Base}_{𝔼_{𝒢} (N)}$
80	79 76	sseqtrrd	$⊢ (N \in ℕ \land (s \in 𝒫 {Base}_{𝔼_{𝒢} (N)} \land t \in 𝒫 {Base}_{𝔼_{𝒢} (N)})) \to t \subseteq 𝔼 (N)$
81		simpll	$⊢ ((N \in ℕ \land (s \subseteq 𝔼 (N) \land t \subseteq 𝔼 (N))) \land \exists a \in 𝔼 (N) \forall x \in s \forall y \in t x Btwn ⟨a, y⟩) \to N \in ℕ$
82		simplrl	$⊢ ((N \in ℕ \land (s \subseteq 𝔼 (N) \land t \subseteq 𝔼 (N))) \land \exists a \in 𝔼 (N) \forall x \in s \forall y \in t x Btwn ⟨a, y⟩) \to s \subseteq 𝔼 (N)$
83		simplrr	$⊢ ((N \in ℕ \land (s \subseteq 𝔼 (N) \land t \subseteq 𝔼 (N))) \land \exists a \in 𝔼 (N) \forall x \in s \forall y \in t x Btwn ⟨a, y⟩) \to t \subseteq 𝔼 (N)$
84		simpr	$⊢ ((N \in ℕ \land (s \subseteq 𝔼 (N) \land t \subseteq 𝔼 (N))) \land \exists a \in 𝔼 (N) \forall x \in s \forall y \in t x Btwn ⟨a, y⟩) \to \exists a \in 𝔼 (N) \forall x \in s \forall y \in t x Btwn ⟨a, y⟩$
85		axcont	$⊢ (N \in ℕ \land (s \subseteq 𝔼 (N) \land t \subseteq 𝔼 (N) \land \exists a \in 𝔼 (N) \forall x \in s \forall y \in t x Btwn ⟨a, y⟩)) \to \exists b \in 𝔼 (N) \forall x \in s \forall y \in t b Btwn ⟨x, y⟩$
86	81 82 83 84 85	syl13anc	$⊢ ((N \in ℕ \land (s \subseteq 𝔼 (N) \land t \subseteq 𝔼 (N))) \land \exists a \in 𝔼 (N) \forall x \in s \forall y \in t x Btwn ⟨a, y⟩) \to \exists b \in 𝔼 (N) \forall x \in s \forall y \in t b Btwn ⟨x, y⟩$
87	86	ex	$⊢ (N \in ℕ \land (s \subseteq 𝔼 (N) \land t \subseteq 𝔼 (N))) \to (\exists a \in 𝔼 (N) \forall x \in s \forall y \in t x Btwn ⟨a, y⟩ \to \exists b \in 𝔼 (N) \forall x \in s \forall y \in t b Btwn ⟨x, y⟩)$
88	73 77 80 87	syl12anc	$⊢ (N \in ℕ \land (s \in 𝒫 {Base}_{𝔼_{𝒢} (N)} \land t \in 𝒫 {Base}_{𝔼_{𝒢} (N)})) \to (\exists a \in 𝔼 (N) \forall x \in s \forall y \in t x Btwn ⟨a, y⟩ \to \exists b \in 𝔼 (N) \forall x \in s \forall y \in t b Btwn ⟨x, y⟩)$
89		simplll	$⊢ (((N \in ℕ \land (s \in 𝒫 {Base}_{𝔼_{𝒢} (N)} \land t \in 𝒫 {Base}_{𝔼_{𝒢} (N)})) \land a \in 𝔼 (N)) \land (x \in s \land y \in t)) \to N \in ℕ$
90		simplr	$⊢ (((N \in ℕ \land (s \in 𝒫 {Base}_{𝔼_{𝒢} (N)} \land t \in 𝒫 {Base}_{𝔼_{𝒢} (N)})) \land a \in 𝔼 (N)) \land (x \in s \land y \in t)) \to a \in 𝔼 (N)$
91	76	ad2antrr	$⊢ (((N \in ℕ \land (s \in 𝒫 {Base}_{𝔼_{𝒢} (N)} \land t \in 𝒫 {Base}_{𝔼_{𝒢} (N)})) \land a \in 𝔼 (N)) \land (x \in s \land y \in t)) \to 𝔼 (N) = {Base}_{𝔼_{𝒢} (N)}$
92	90 91	eleqtrd	$⊢ (((N \in ℕ \land (s \in 𝒫 {Base}_{𝔼_{𝒢} (N)} \land t \in 𝒫 {Base}_{𝔼_{𝒢} (N)})) \land a \in 𝔼 (N)) \land (x \in s \land y \in t)) \to a \in {Base}_{𝔼_{𝒢} (N)}$
93	79	ad2antrr	$⊢ (((N \in ℕ \land (s \in 𝒫 {Base}_{𝔼_{𝒢} (N)} \land t \in 𝒫 {Base}_{𝔼_{𝒢} (N)})) \land a \in 𝔼 (N)) \land (x \in s \land y \in t)) \to t \subseteq {Base}_{𝔼_{𝒢} (N)}$
94		simprr	$⊢ (((N \in ℕ \land (s \in 𝒫 {Base}_{𝔼_{𝒢} (N)} \land t \in 𝒫 {Base}_{𝔼_{𝒢} (N)})) \land a \in 𝔼 (N)) \land (x \in s \land y \in t)) \to y \in t$
95	93 94	sseldd	$⊢ (((N \in ℕ \land (s \in 𝒫 {Base}_{𝔼_{𝒢} (N)} \land t \in 𝒫 {Base}_{𝔼_{𝒢} (N)})) \land a \in 𝔼 (N)) \land (x \in s \land y \in t)) \to y \in {Base}_{𝔼_{𝒢} (N)}$
96	75	ad2antrr	$⊢ (((N \in ℕ \land (s \in 𝒫 {Base}_{𝔼_{𝒢} (N)} \land t \in 𝒫 {Base}_{𝔼_{𝒢} (N)})) \land a \in 𝔼 (N)) \land (x \in s \land y \in t)) \to s \subseteq {Base}_{𝔼_{𝒢} (N)}$
97		simprl	$⊢ (((N \in ℕ \land (s \in 𝒫 {Base}_{𝔼_{𝒢} (N)} \land t \in 𝒫 {Base}_{𝔼_{𝒢} (N)})) \land a \in 𝔼 (N)) \land (x \in s \land y \in t)) \to x \in s$
98	96 97	sseldd	$⊢ (((N \in ℕ \land (s \in 𝒫 {Base}_{𝔼_{𝒢} (N)} \land t \in 𝒫 {Base}_{𝔼_{𝒢} (N)})) \land a \in 𝔼 (N)) \land (x \in s \land y \in t)) \to x \in {Base}_{𝔼_{𝒢} (N)}$
99	89 11 30 92 95 98	ebtwntg	$⊢ (((N \in ℕ \land (s \in 𝒫 {Base}_{𝔼_{𝒢} (N)} \land t \in 𝒫 {Base}_{𝔼_{𝒢} (N)})) \land a \in 𝔼 (N)) \land (x \in s \land y \in t)) \to (x Btwn ⟨a, y⟩ \leftrightarrow x \in (a Itv (𝔼_{𝒢} (N)) y))$
100	99	2ralbidva	$⊢ ((N \in ℕ \land (s \in 𝒫 {Base}_{𝔼_{𝒢} (N)} \land t \in 𝒫 {Base}_{𝔼_{𝒢} (N)})) \land a \in 𝔼 (N)) \to (\forall x \in s \forall y \in t x Btwn ⟨a, y⟩ \leftrightarrow \forall x \in s \forall y \in t x \in (a Itv (𝔼_{𝒢} (N)) y))$
101	76 100	rexeqbidva	$⊢ (N \in ℕ \land (s \in 𝒫 {Base}_{𝔼_{𝒢} (N)} \land t \in 𝒫 {Base}_{𝔼_{𝒢} (N)})) \to (\exists a \in 𝔼 (N) \forall x \in s \forall y \in t x Btwn ⟨a, y⟩ \leftrightarrow \exists a \in {Base}_{𝔼_{𝒢} (N)} \forall x \in s \forall y \in t x \in (a Itv (𝔼_{𝒢} (N)) y))$
102		simplll	$⊢ (((N \in ℕ \land (s \in 𝒫 {Base}_{𝔼_{𝒢} (N)} \land t \in 𝒫 {Base}_{𝔼_{𝒢} (N)})) \land b \in 𝔼 (N)) \land (x \in s \land y \in t)) \to N \in ℕ$
103	75	ad2antrr	$⊢ (((N \in ℕ \land (s \in 𝒫 {Base}_{𝔼_{𝒢} (N)} \land t \in 𝒫 {Base}_{𝔼_{𝒢} (N)})) \land b \in 𝔼 (N)) \land (x \in s \land y \in t)) \to s \subseteq {Base}_{𝔼_{𝒢} (N)}$
104		simprl	$⊢ (((N \in ℕ \land (s \in 𝒫 {Base}_{𝔼_{𝒢} (N)} \land t \in 𝒫 {Base}_{𝔼_{𝒢} (N)})) \land b \in 𝔼 (N)) \land (x \in s \land y \in t)) \to x \in s$
105	103 104	sseldd	$⊢ (((N \in ℕ \land (s \in 𝒫 {Base}_{𝔼_{𝒢} (N)} \land t \in 𝒫 {Base}_{𝔼_{𝒢} (N)})) \land b \in 𝔼 (N)) \land (x \in s \land y \in t)) \to x \in {Base}_{𝔼_{𝒢} (N)}$
106	79	ad2antrr	$⊢ (((N \in ℕ \land (s \in 𝒫 {Base}_{𝔼_{𝒢} (N)} \land t \in 𝒫 {Base}_{𝔼_{𝒢} (N)})) \land b \in 𝔼 (N)) \land (x \in s \land y \in t)) \to t \subseteq {Base}_{𝔼_{𝒢} (N)}$
107		simprr	$⊢ (((N \in ℕ \land (s \in 𝒫 {Base}_{𝔼_{𝒢} (N)} \land t \in 𝒫 {Base}_{𝔼_{𝒢} (N)})) \land b \in 𝔼 (N)) \land (x \in s \land y \in t)) \to y \in t$
108	106 107	sseldd	$⊢ (((N \in ℕ \land (s \in 𝒫 {Base}_{𝔼_{𝒢} (N)} \land t \in 𝒫 {Base}_{𝔼_{𝒢} (N)})) \land b \in 𝔼 (N)) \land (x \in s \land y \in t)) \to y \in {Base}_{𝔼_{𝒢} (N)}$
109		simplr	$⊢ (((N \in ℕ \land (s \in 𝒫 {Base}_{𝔼_{𝒢} (N)} \land t \in 𝒫 {Base}_{𝔼_{𝒢} (N)})) \land b \in 𝔼 (N)) \land (x \in s \land y \in t)) \to b \in 𝔼 (N)$
110	76	ad2antrr	$⊢ (((N \in ℕ \land (s \in 𝒫 {Base}_{𝔼_{𝒢} (N)} \land t \in 𝒫 {Base}_{𝔼_{𝒢} (N)})) \land b \in 𝔼 (N)) \land (x \in s \land y \in t)) \to 𝔼 (N) = {Base}_{𝔼_{𝒢} (N)}$
111	109 110	eleqtrd	$⊢ (((N \in ℕ \land (s \in 𝒫 {Base}_{𝔼_{𝒢} (N)} \land t \in 𝒫 {Base}_{𝔼_{𝒢} (N)})) \land b \in 𝔼 (N)) \land (x \in s \land y \in t)) \to b \in {Base}_{𝔼_{𝒢} (N)}$
112	102 11 30 105 108 111	ebtwntg	$⊢ (((N \in ℕ \land (s \in 𝒫 {Base}_{𝔼_{𝒢} (N)} \land t \in 𝒫 {Base}_{𝔼_{𝒢} (N)})) \land b \in 𝔼 (N)) \land (x \in s \land y \in t)) \to (b Btwn ⟨x, y⟩ \leftrightarrow b \in (x Itv (𝔼_{𝒢} (N)) y))$
113	112	2ralbidva	$⊢ ((N \in ℕ \land (s \in 𝒫 {Base}_{𝔼_{𝒢} (N)} \land t \in 𝒫 {Base}_{𝔼_{𝒢} (N)})) \land b \in 𝔼 (N)) \to (\forall x \in s \forall y \in t b Btwn ⟨x, y⟩ \leftrightarrow \forall x \in s \forall y \in t b \in (x Itv (𝔼_{𝒢} (N)) y))$
114	76 113	rexeqbidva	$⊢ (N \in ℕ \land (s \in 𝒫 {Base}_{𝔼_{𝒢} (N)} \land t \in 𝒫 {Base}_{𝔼_{𝒢} (N)})) \to (\exists b \in 𝔼 (N) \forall x \in s \forall y \in t b Btwn ⟨x, y⟩ \leftrightarrow \exists b \in {Base}_{𝔼_{𝒢} (N)} \forall x \in s \forall y \in t b \in (x Itv (𝔼_{𝒢} (N)) y))$
115	88 101 114	3imtr3d	$⊢ (N \in ℕ \land (s \in 𝒫 {Base}_{𝔼_{𝒢} (N)} \land t \in 𝒫 {Base}_{𝔼_{𝒢} (N)})) \to (\exists a \in {Base}_{𝔼_{𝒢} (N)} \forall x \in s \forall y \in t x \in (a Itv (𝔼_{𝒢} (N)) y) \to \exists b \in {Base}_{𝔼_{𝒢} (N)} \forall x \in s \forall y \in t b \in (x Itv (𝔼_{𝒢} (N)) y))$
116	115	ralrimivva	$⊢ N \in ℕ \to \forall s \in 𝒫 {Base}_{𝔼_{𝒢} (N)} \forall t \in 𝒫 {Base}_{𝔼_{𝒢} (N)} (\exists a \in {Base}_{𝔼_{𝒢} (N)} \forall x \in s \forall y \in t x \in (a Itv (𝔼_{𝒢} (N)) y) \to \exists b \in {Base}_{𝔼_{𝒢} (N)} \forall x \in s \forall y \in t b \in (x Itv (𝔼_{𝒢} (N)) y))$
117	40 72 116	3jca	$⊢ N \in ℕ \to (\forall x \in {Base}_{𝔼_{𝒢} (N)} \forall y \in {Base}_{𝔼_{𝒢} (N)} (y \in (x Itv (𝔼_{𝒢} (N)) x) \to x = y) \land \forall x \in {Base}_{𝔼_{𝒢} (N)} \forall y \in {Base}_{𝔼_{𝒢} (N)} \forall z \in {Base}_{𝔼_{𝒢} (N)} \forall u \in {Base}_{𝔼_{𝒢} (N)} \forall v \in {Base}_{𝔼_{𝒢} (N)} ((u \in (x Itv (𝔼_{𝒢} (N)) z) \land v \in (y Itv (𝔼_{𝒢} (N)) z)) \to \exists a \in {Base}_{𝔼_{𝒢} (N)} (a \in (u Itv (𝔼_{𝒢} (N)) y) \land a \in (v Itv (𝔼_{𝒢} (N)) x))) \land \forall s \in 𝒫 {Base}_{𝔼_{𝒢} (N)} \forall t \in 𝒫 {Base}_{𝔼_{𝒢} (N)} (\exists a \in {Base}_{𝔼_{𝒢} (N)} \forall x \in s \forall y \in t x \in (a Itv (𝔼_{𝒢} (N)) y) \to \exists b \in {Base}_{𝔼_{𝒢} (N)} \forall x \in s \forall y \in t b \in (x Itv (𝔼_{𝒢} (N)) y)))$
118	11 12 30	istrkgb	$⊢ 𝔼_{𝒢} (N) \in 𝒢_{Tarski}^{B} \leftrightarrow (𝔼_{𝒢} (N) \in V \land (\forall x \in {Base}_{𝔼_{𝒢} (N)} \forall y \in {Base}_{𝔼_{𝒢} (N)} (y \in (x Itv (𝔼_{𝒢} (N)) x) \to x = y) \land \forall x \in {Base}_{𝔼_{𝒢} (N)} \forall y \in {Base}_{𝔼_{𝒢} (N)} \forall z \in {Base}_{𝔼_{𝒢} (N)} \forall u \in {Base}_{𝔼_{𝒢} (N)} \forall v \in {Base}_{𝔼_{𝒢} (N)} ((u \in (x Itv (𝔼_{𝒢} (N)) z) \land v \in (y Itv (𝔼_{𝒢} (N)) z)) \to \exists a \in {Base}_{𝔼_{𝒢} (N)} (a \in (u Itv (𝔼_{𝒢} (N)) y) \land a \in (v Itv (𝔼_{𝒢} (N)) x))) \land \forall s \in 𝒫 {Base}_{𝔼_{𝒢} (N)} \forall t \in 𝒫 {Base}_{𝔼_{𝒢} (N)} (\exists a \in {Base}_{𝔼_{𝒢} (N)} \forall x \in s \forall y \in t x \in (a Itv (𝔼_{𝒢} (N)) y) \to \exists b \in {Base}_{𝔼_{𝒢} (N)} \forall x \in s \forall y \in t b \in (x Itv (𝔼_{𝒢} (N)) y))))$
119	1 117 118	sylanbrc	$⊢ N \in ℕ \to 𝔼_{𝒢} (N) \in 𝒢_{Tarski}^{B}$
120	32 119	elind	$⊢ N \in ℕ \to 𝔼_{𝒢} (N) \in (𝒢_{Tarski}^{C} \cap 𝒢_{Tarski}^{B})$
121		simplll	$⊢ (((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (z \in {Base}_{𝔼_{𝒢} (N)} \land u \in {Base}_{𝔼_{𝒢} (N)} \land a \in {Base}_{𝔼_{𝒢} (N)})) \land (b \in {Base}_{𝔼_{𝒢} (N)} \land c \in {Base}_{𝔼_{𝒢} (N)} \land v \in {Base}_{𝔼_{𝒢} (N)})) \to N \in ℕ$
122	3	ad2antrr	$⊢ (((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (z \in {Base}_{𝔼_{𝒢} (N)} \land u \in {Base}_{𝔼_{𝒢} (N)} \land a \in {Base}_{𝔼_{𝒢} (N)})) \land (b \in {Base}_{𝔼_{𝒢} (N)} \land c \in {Base}_{𝔼_{𝒢} (N)} \land v \in {Base}_{𝔼_{𝒢} (N)})) \to x \in {Base}_{𝔼_{𝒢} (N)}$
123	121 4	syl	$⊢ (((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (z \in {Base}_{𝔼_{𝒢} (N)} \land u \in {Base}_{𝔼_{𝒢} (N)} \land a \in {Base}_{𝔼_{𝒢} (N)})) \land (b \in {Base}_{𝔼_{𝒢} (N)} \land c \in {Base}_{𝔼_{𝒢} (N)} \land v \in {Base}_{𝔼_{𝒢} (N)})) \to 𝔼 (N) = {Base}_{𝔼_{𝒢} (N)}$
124	122 123	eleqtrrd	$⊢ (((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (z \in {Base}_{𝔼_{𝒢} (N)} \land u \in {Base}_{𝔼_{𝒢} (N)} \land a \in {Base}_{𝔼_{𝒢} (N)})) \land (b \in {Base}_{𝔼_{𝒢} (N)} \land c \in {Base}_{𝔼_{𝒢} (N)} \land v \in {Base}_{𝔼_{𝒢} (N)})) \to x \in 𝔼 (N)$
125	7	ad2antrr	$⊢ (((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (z \in {Base}_{𝔼_{𝒢} (N)} \land u \in {Base}_{𝔼_{𝒢} (N)} \land a \in {Base}_{𝔼_{𝒢} (N)})) \land (b \in {Base}_{𝔼_{𝒢} (N)} \land c \in {Base}_{𝔼_{𝒢} (N)} \land v \in {Base}_{𝔼_{𝒢} (N)})) \to y \in {Base}_{𝔼_{𝒢} (N)}$
126	125 123	eleqtrrd	$⊢ (((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (z \in {Base}_{𝔼_{𝒢} (N)} \land u \in {Base}_{𝔼_{𝒢} (N)} \land a \in {Base}_{𝔼_{𝒢} (N)})) \land (b \in {Base}_{𝔼_{𝒢} (N)} \land c \in {Base}_{𝔼_{𝒢} (N)} \land v \in {Base}_{𝔼_{𝒢} (N)})) \to y \in 𝔼 (N)$
127		simplr1	$⊢ (((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (z \in {Base}_{𝔼_{𝒢} (N)} \land u \in {Base}_{𝔼_{𝒢} (N)} \land a \in {Base}_{𝔼_{𝒢} (N)})) \land (b \in {Base}_{𝔼_{𝒢} (N)} \land c \in {Base}_{𝔼_{𝒢} (N)} \land v \in {Base}_{𝔼_{𝒢} (N)})) \to z \in {Base}_{𝔼_{𝒢} (N)}$
128	127 123	eleqtrrd	$⊢ (((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (z \in {Base}_{𝔼_{𝒢} (N)} \land u \in {Base}_{𝔼_{𝒢} (N)} \land a \in {Base}_{𝔼_{𝒢} (N)})) \land (b \in {Base}_{𝔼_{𝒢} (N)} \land c \in {Base}_{𝔼_{𝒢} (N)} \land v \in {Base}_{𝔼_{𝒢} (N)})) \to z \in 𝔼 (N)$
129		simplr2	$⊢ (((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (z \in {Base}_{𝔼_{𝒢} (N)} \land u \in {Base}_{𝔼_{𝒢} (N)} \land a \in {Base}_{𝔼_{𝒢} (N)})) \land (b \in {Base}_{𝔼_{𝒢} (N)} \land c \in {Base}_{𝔼_{𝒢} (N)} \land v \in {Base}_{𝔼_{𝒢} (N)})) \to u \in {Base}_{𝔼_{𝒢} (N)}$
130	129 123	eleqtrrd	$⊢ (((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (z \in {Base}_{𝔼_{𝒢} (N)} \land u \in {Base}_{𝔼_{𝒢} (N)} \land a \in {Base}_{𝔼_{𝒢} (N)})) \land (b \in {Base}_{𝔼_{𝒢} (N)} \land c \in {Base}_{𝔼_{𝒢} (N)} \land v \in {Base}_{𝔼_{𝒢} (N)})) \to u \in 𝔼 (N)$
131		simplr3	$⊢ (((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (z \in {Base}_{𝔼_{𝒢} (N)} \land u \in {Base}_{𝔼_{𝒢} (N)} \land a \in {Base}_{𝔼_{𝒢} (N)})) \land (b \in {Base}_{𝔼_{𝒢} (N)} \land c \in {Base}_{𝔼_{𝒢} (N)} \land v \in {Base}_{𝔼_{𝒢} (N)})) \to a \in {Base}_{𝔼_{𝒢} (N)}$
132	131 123	eleqtrrd	$⊢ (((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (z \in {Base}_{𝔼_{𝒢} (N)} \land u \in {Base}_{𝔼_{𝒢} (N)} \land a \in {Base}_{𝔼_{𝒢} (N)})) \land (b \in {Base}_{𝔼_{𝒢} (N)} \land c \in {Base}_{𝔼_{𝒢} (N)} \land v \in {Base}_{𝔼_{𝒢} (N)})) \to a \in 𝔼 (N)$
133		simpr1	$⊢ (((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (z \in {Base}_{𝔼_{𝒢} (N)} \land u \in {Base}_{𝔼_{𝒢} (N)} \land a \in {Base}_{𝔼_{𝒢} (N)})) \land (b \in {Base}_{𝔼_{𝒢} (N)} \land c \in {Base}_{𝔼_{𝒢} (N)} \land v \in {Base}_{𝔼_{𝒢} (N)})) \to b \in {Base}_{𝔼_{𝒢} (N)}$
134	133 123	eleqtrrd	$⊢ (((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (z \in {Base}_{𝔼_{𝒢} (N)} \land u \in {Base}_{𝔼_{𝒢} (N)} \land a \in {Base}_{𝔼_{𝒢} (N)})) \land (b \in {Base}_{𝔼_{𝒢} (N)} \land c \in {Base}_{𝔼_{𝒢} (N)} \land v \in {Base}_{𝔼_{𝒢} (N)})) \to b \in 𝔼 (N)$
135		simpr2	$⊢ (((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (z \in {Base}_{𝔼_{𝒢} (N)} \land u \in {Base}_{𝔼_{𝒢} (N)} \land a \in {Base}_{𝔼_{𝒢} (N)})) \land (b \in {Base}_{𝔼_{𝒢} (N)} \land c \in {Base}_{𝔼_{𝒢} (N)} \land v \in {Base}_{𝔼_{𝒢} (N)})) \to c \in {Base}_{𝔼_{𝒢} (N)}$
136	135 123	eleqtrrd	$⊢ (((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (z \in {Base}_{𝔼_{𝒢} (N)} \land u \in {Base}_{𝔼_{𝒢} (N)} \land a \in {Base}_{𝔼_{𝒢} (N)})) \land (b \in {Base}_{𝔼_{𝒢} (N)} \land c \in {Base}_{𝔼_{𝒢} (N)} \land v \in {Base}_{𝔼_{𝒢} (N)})) \to c \in 𝔼 (N)$
137		simpr3	$⊢ (((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (z \in {Base}_{𝔼_{𝒢} (N)} \land u \in {Base}_{𝔼_{𝒢} (N)} \land a \in {Base}_{𝔼_{𝒢} (N)})) \land (b \in {Base}_{𝔼_{𝒢} (N)} \land c \in {Base}_{𝔼_{𝒢} (N)} \land v \in {Base}_{𝔼_{𝒢} (N)})) \to v \in {Base}_{𝔼_{𝒢} (N)}$
138	137 123	eleqtrrd	$⊢ (((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (z \in {Base}_{𝔼_{𝒢} (N)} \land u \in {Base}_{𝔼_{𝒢} (N)} \land a \in {Base}_{𝔼_{𝒢} (N)})) \land (b \in {Base}_{𝔼_{𝒢} (N)} \land c \in {Base}_{𝔼_{𝒢} (N)} \land v \in {Base}_{𝔼_{𝒢} (N)})) \to v \in 𝔼 (N)$
139		3anass	$⊢ ((x \neq y \land y Btwn ⟨x, z⟩ \land b Btwn ⟨a, c⟩) \land (⟨x, y⟩ Cgr ⟨a, b⟩ \land ⟨y, z⟩ Cgr ⟨b, c⟩) \land (⟨x, u⟩ Cgr ⟨a, v⟩ \land ⟨y, u⟩ Cgr ⟨b, v⟩)) \leftrightarrow ((x \neq y \land y Btwn ⟨x, z⟩ \land b Btwn ⟨a, c⟩) \land ((⟨x, y⟩ Cgr ⟨a, b⟩ \land ⟨y, z⟩ Cgr ⟨b, c⟩) \land (⟨x, u⟩ Cgr ⟨a, v⟩ \land ⟨y, u⟩ Cgr ⟨b, v⟩)))$
140		ax5seg	$⊢ ((N \in ℕ \land x \in 𝔼 (N) \land y \in 𝔼 (N)) \land (z \in 𝔼 (N) \land u \in 𝔼 (N) \land a \in 𝔼 (N)) \land (b \in 𝔼 (N) \land c \in 𝔼 (N) \land v \in 𝔼 (N))) \to (((x \neq y \land y Btwn ⟨x, z⟩ \land b Btwn ⟨a, c⟩) \land (⟨x, y⟩ Cgr ⟨a, b⟩ \land ⟨y, z⟩ Cgr ⟨b, c⟩) \land (⟨x, u⟩ Cgr ⟨a, v⟩ \land ⟨y, u⟩ Cgr ⟨b, v⟩)) \to ⟨z, u⟩ Cgr ⟨c, v⟩)$
141	139 140	syl5bir	$⊢ ((N \in ℕ \land x \in 𝔼 (N) \land y \in 𝔼 (N)) \land (z \in 𝔼 (N) \land u \in 𝔼 (N) \land a \in 𝔼 (N)) \land (b \in 𝔼 (N) \land c \in 𝔼 (N) \land v \in 𝔼 (N))) \to (((x \neq y \land y Btwn ⟨x, z⟩ \land b Btwn ⟨a, c⟩) \land ((⟨x, y⟩ Cgr ⟨a, b⟩ \land ⟨y, z⟩ Cgr ⟨b, c⟩) \land (⟨x, u⟩ Cgr ⟨a, v⟩ \land ⟨y, u⟩ Cgr ⟨b, v⟩))) \to ⟨z, u⟩ Cgr ⟨c, v⟩)$
142	121 124 126 128 130 132 134 136 138 141	syl333anc	$⊢ (((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (z \in {Base}_{𝔼_{𝒢} (N)} \land u \in {Base}_{𝔼_{𝒢} (N)} \land a \in {Base}_{𝔼_{𝒢} (N)})) \land (b \in {Base}_{𝔼_{𝒢} (N)} \land c \in {Base}_{𝔼_{𝒢} (N)} \land v \in {Base}_{𝔼_{𝒢} (N)})) \to (((x \neq y \land y Btwn ⟨x, z⟩ \land b Btwn ⟨a, c⟩) \land ((⟨x, y⟩ Cgr ⟨a, b⟩ \land ⟨y, z⟩ Cgr ⟨b, c⟩) \land (⟨x, u⟩ Cgr ⟨a, v⟩ \land ⟨y, u⟩ Cgr ⟨b, v⟩))) \to ⟨z, u⟩ Cgr ⟨c, v⟩)$
143	121 11 30 122 127 125	ebtwntg	$⊢ (((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (z \in {Base}_{𝔼_{𝒢} (N)} \land u \in {Base}_{𝔼_{𝒢} (N)} \land a \in {Base}_{𝔼_{𝒢} (N)})) \land (b \in {Base}_{𝔼_{𝒢} (N)} \land c \in {Base}_{𝔼_{𝒢} (N)} \land v \in {Base}_{𝔼_{𝒢} (N)})) \to (y Btwn ⟨x, z⟩ \leftrightarrow y \in (x Itv (𝔼_{𝒢} (N)) z))$
144	121 11 30 131 135 133	ebtwntg	$⊢ (((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (z \in {Base}_{𝔼_{𝒢} (N)} \land u \in {Base}_{𝔼_{𝒢} (N)} \land a \in {Base}_{𝔼_{𝒢} (N)})) \land (b \in {Base}_{𝔼_{𝒢} (N)} \land c \in {Base}_{𝔼_{𝒢} (N)} \land v \in {Base}_{𝔼_{𝒢} (N)})) \to (b Btwn ⟨a, c⟩ \leftrightarrow b \in (a Itv (𝔼_{𝒢} (N)) c))$
145	143 144	3anbi23d	$⊢ (((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (z \in {Base}_{𝔼_{𝒢} (N)} \land u \in {Base}_{𝔼_{𝒢} (N)} \land a \in {Base}_{𝔼_{𝒢} (N)})) \land (b \in {Base}_{𝔼_{𝒢} (N)} \land c \in {Base}_{𝔼_{𝒢} (N)} \land v \in {Base}_{𝔼_{𝒢} (N)})) \to ((x \neq y \land y Btwn ⟨x, z⟩ \land b Btwn ⟨a, c⟩) \leftrightarrow (x \neq y \land y \in (x Itv (𝔼_{𝒢} (N)) z) \land b \in (a Itv (𝔼_{𝒢} (N)) c)))$
146	121 11 12 122 125 131 133	ecgrtg	$⊢ (((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (z \in {Base}_{𝔼_{𝒢} (N)} \land u \in {Base}_{𝔼_{𝒢} (N)} \land a \in {Base}_{𝔼_{𝒢} (N)})) \land (b \in {Base}_{𝔼_{𝒢} (N)} \land c \in {Base}_{𝔼_{𝒢} (N)} \land v \in {Base}_{𝔼_{𝒢} (N)})) \to (⟨x, y⟩ Cgr ⟨a, b⟩ \leftrightarrow x dist (𝔼_{𝒢} (N)) y = a dist (𝔼_{𝒢} (N)) b)$
147	121 11 12 125 127 133 135	ecgrtg	$⊢ (((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (z \in {Base}_{𝔼_{𝒢} (N)} \land u \in {Base}_{𝔼_{𝒢} (N)} \land a \in {Base}_{𝔼_{𝒢} (N)})) \land (b \in {Base}_{𝔼_{𝒢} (N)} \land c \in {Base}_{𝔼_{𝒢} (N)} \land v \in {Base}_{𝔼_{𝒢} (N)})) \to (⟨y, z⟩ Cgr ⟨b, c⟩ \leftrightarrow y dist (𝔼_{𝒢} (N)) z = b dist (𝔼_{𝒢} (N)) c)$
148	146 147	anbi12d	$⊢ (((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (z \in {Base}_{𝔼_{𝒢} (N)} \land u \in {Base}_{𝔼_{𝒢} (N)} \land a \in {Base}_{𝔼_{𝒢} (N)})) \land (b \in {Base}_{𝔼_{𝒢} (N)} \land c \in {Base}_{𝔼_{𝒢} (N)} \land v \in {Base}_{𝔼_{𝒢} (N)})) \to ((⟨x, y⟩ Cgr ⟨a, b⟩ \land ⟨y, z⟩ Cgr ⟨b, c⟩) \leftrightarrow (x dist (𝔼_{𝒢} (N)) y = a dist (𝔼_{𝒢} (N)) b \land y dist (𝔼_{𝒢} (N)) z = b dist (𝔼_{𝒢} (N)) c))$
149	121 11 12 122 129 131 137	ecgrtg	$⊢ (((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (z \in {Base}_{𝔼_{𝒢} (N)} \land u \in {Base}_{𝔼_{𝒢} (N)} \land a \in {Base}_{𝔼_{𝒢} (N)})) \land (b \in {Base}_{𝔼_{𝒢} (N)} \land c \in {Base}_{𝔼_{𝒢} (N)} \land v \in {Base}_{𝔼_{𝒢} (N)})) \to (⟨x, u⟩ Cgr ⟨a, v⟩ \leftrightarrow x dist (𝔼_{𝒢} (N)) u = a dist (𝔼_{𝒢} (N)) v)$
150	121 11 12 125 129 133 137	ecgrtg	$⊢ (((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (z \in {Base}_{𝔼_{𝒢} (N)} \land u \in {Base}_{𝔼_{𝒢} (N)} \land a \in {Base}_{𝔼_{𝒢} (N)})) \land (b \in {Base}_{𝔼_{𝒢} (N)} \land c \in {Base}_{𝔼_{𝒢} (N)} \land v \in {Base}_{𝔼_{𝒢} (N)})) \to (⟨y, u⟩ Cgr ⟨b, v⟩ \leftrightarrow y dist (𝔼_{𝒢} (N)) u = b dist (𝔼_{𝒢} (N)) v)$
151	149 150	anbi12d	$⊢ (((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (z \in {Base}_{𝔼_{𝒢} (N)} \land u \in {Base}_{𝔼_{𝒢} (N)} \land a \in {Base}_{𝔼_{𝒢} (N)})) \land (b \in {Base}_{𝔼_{𝒢} (N)} \land c \in {Base}_{𝔼_{𝒢} (N)} \land v \in {Base}_{𝔼_{𝒢} (N)})) \to ((⟨x, u⟩ Cgr ⟨a, v⟩ \land ⟨y, u⟩ Cgr ⟨b, v⟩) \leftrightarrow (x dist (𝔼_{𝒢} (N)) u = a dist (𝔼_{𝒢} (N)) v \land y dist (𝔼_{𝒢} (N)) u = b dist (𝔼_{𝒢} (N)) v))$
152	148 151	anbi12d	$⊢ (((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (z \in {Base}_{𝔼_{𝒢} (N)} \land u \in {Base}_{𝔼_{𝒢} (N)} \land a \in {Base}_{𝔼_{𝒢} (N)})) \land (b \in {Base}_{𝔼_{𝒢} (N)} \land c \in {Base}_{𝔼_{𝒢} (N)} \land v \in {Base}_{𝔼_{𝒢} (N)})) \to (((⟨x, y⟩ Cgr ⟨a, b⟩ \land ⟨y, z⟩ Cgr ⟨b, c⟩) \land (⟨x, u⟩ Cgr ⟨a, v⟩ \land ⟨y, u⟩ Cgr ⟨b, v⟩)) \leftrightarrow ((x dist (𝔼_{𝒢} (N)) y = a dist (𝔼_{𝒢} (N)) b \land y dist (𝔼_{𝒢} (N)) z = b dist (𝔼_{𝒢} (N)) c) \land (x dist (𝔼_{𝒢} (N)) u = a dist (𝔼_{𝒢} (N)) v \land y dist (𝔼_{𝒢} (N)) u = b dist (𝔼_{𝒢} (N)) v)))$
153	145 152	anbi12d	$⊢ (((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (z \in {Base}_{𝔼_{𝒢} (N)} \land u \in {Base}_{𝔼_{𝒢} (N)} \land a \in {Base}_{𝔼_{𝒢} (N)})) \land (b \in {Base}_{𝔼_{𝒢} (N)} \land c \in {Base}_{𝔼_{𝒢} (N)} \land v \in {Base}_{𝔼_{𝒢} (N)})) \to (((x \neq y \land y Btwn ⟨x, z⟩ \land b Btwn ⟨a, c⟩) \land ((⟨x, y⟩ Cgr ⟨a, b⟩ \land ⟨y, z⟩ Cgr ⟨b, c⟩) \land (⟨x, u⟩ Cgr ⟨a, v⟩ \land ⟨y, u⟩ Cgr ⟨b, v⟩))) \leftrightarrow ((x \neq y \land y \in (x Itv (𝔼_{𝒢} (N)) z) \land b \in (a Itv (𝔼_{𝒢} (N)) c)) \land ((x dist (𝔼_{𝒢} (N)) y = a dist (𝔼_{𝒢} (N)) b \land y dist (𝔼_{𝒢} (N)) z = b dist (𝔼_{𝒢} (N)) c) \land (x dist (𝔼_{𝒢} (N)) u = a dist (𝔼_{𝒢} (N)) v \land y dist (𝔼_{𝒢} (N)) u = b dist (𝔼_{𝒢} (N)) v))))$
154	121 11 12 127 129 135 137	ecgrtg	$⊢ (((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (z \in {Base}_{𝔼_{𝒢} (N)} \land u \in {Base}_{𝔼_{𝒢} (N)} \land a \in {Base}_{𝔼_{𝒢} (N)})) \land (b \in {Base}_{𝔼_{𝒢} (N)} \land c \in {Base}_{𝔼_{𝒢} (N)} \land v \in {Base}_{𝔼_{𝒢} (N)})) \to (⟨z, u⟩ Cgr ⟨c, v⟩ \leftrightarrow z dist (𝔼_{𝒢} (N)) u = c dist (𝔼_{𝒢} (N)) v)$
155	142 153 154	3imtr3d	$⊢ (((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (z \in {Base}_{𝔼_{𝒢} (N)} \land u \in {Base}_{𝔼_{𝒢} (N)} \land a \in {Base}_{𝔼_{𝒢} (N)})) \land (b \in {Base}_{𝔼_{𝒢} (N)} \land c \in {Base}_{𝔼_{𝒢} (N)} \land v \in {Base}_{𝔼_{𝒢} (N)})) \to (((x \neq y \land y \in (x Itv (𝔼_{𝒢} (N)) z) \land b \in (a Itv (𝔼_{𝒢} (N)) c)) \land ((x dist (𝔼_{𝒢} (N)) y = a dist (𝔼_{𝒢} (N)) b \land y dist (𝔼_{𝒢} (N)) z = b dist (𝔼_{𝒢} (N)) c) \land (x dist (𝔼_{𝒢} (N)) u = a dist (𝔼_{𝒢} (N)) v \land y dist (𝔼_{𝒢} (N)) u = b dist (𝔼_{𝒢} (N)) v))) \to z dist (𝔼_{𝒢} (N)) u = c dist (𝔼_{𝒢} (N)) v)$
156	155	ralrimivvva	$⊢ ((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (z \in {Base}_{𝔼_{𝒢} (N)} \land u \in {Base}_{𝔼_{𝒢} (N)} \land a \in {Base}_{𝔼_{𝒢} (N)})) \to \forall b \in {Base}_{𝔼_{𝒢} (N)} \forall c \in {Base}_{𝔼_{𝒢} (N)} \forall v \in {Base}_{𝔼_{𝒢} (N)} (((x \neq y \land y \in (x Itv (𝔼_{𝒢} (N)) z) \land b \in (a Itv (𝔼_{𝒢} (N)) c)) \land ((x dist (𝔼_{𝒢} (N)) y = a dist (𝔼_{𝒢} (N)) b \land y dist (𝔼_{𝒢} (N)) z = b dist (𝔼_{𝒢} (N)) c) \land (x dist (𝔼_{𝒢} (N)) u = a dist (𝔼_{𝒢} (N)) v \land y dist (𝔼_{𝒢} (N)) u = b dist (𝔼_{𝒢} (N)) v))) \to z dist (𝔼_{𝒢} (N)) u = c dist (𝔼_{𝒢} (N)) v)$
157	156	ralrimivvva	$⊢ (N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \to \forall z \in {Base}_{𝔼_{𝒢} (N)} \forall u \in {Base}_{𝔼_{𝒢} (N)} \forall a \in {Base}_{𝔼_{𝒢} (N)} \forall b \in {Base}_{𝔼_{𝒢} (N)} \forall c \in {Base}_{𝔼_{𝒢} (N)} \forall v \in {Base}_{𝔼_{𝒢} (N)} (((x \neq y \land y \in (x Itv (𝔼_{𝒢} (N)) z) \land b \in (a Itv (𝔼_{𝒢} (N)) c)) \land ((x dist (𝔼_{𝒢} (N)) y = a dist (𝔼_{𝒢} (N)) b \land y dist (𝔼_{𝒢} (N)) z = b dist (𝔼_{𝒢} (N)) c) \land (x dist (𝔼_{𝒢} (N)) u = a dist (𝔼_{𝒢} (N)) v \land y dist (𝔼_{𝒢} (N)) u = b dist (𝔼_{𝒢} (N)) v))) \to z dist (𝔼_{𝒢} (N)) u = c dist (𝔼_{𝒢} (N)) v)$
158	157	ralrimivva	$⊢ N \in ℕ \to \forall x \in {Base}_{𝔼_{𝒢} (N)} \forall y \in {Base}_{𝔼_{𝒢} (N)} \forall z \in {Base}_{𝔼_{𝒢} (N)} \forall u \in {Base}_{𝔼_{𝒢} (N)} \forall a \in {Base}_{𝔼_{𝒢} (N)} \forall b \in {Base}_{𝔼_{𝒢} (N)} \forall c \in {Base}_{𝔼_{𝒢} (N)} \forall v \in {Base}_{𝔼_{𝒢} (N)} (((x \neq y \land y \in (x Itv (𝔼_{𝒢} (N)) z) \land b \in (a Itv (𝔼_{𝒢} (N)) c)) \land ((x dist (𝔼_{𝒢} (N)) y = a dist (𝔼_{𝒢} (N)) b \land y dist (𝔼_{𝒢} (N)) z = b dist (𝔼_{𝒢} (N)) c) \land (x dist (𝔼_{𝒢} (N)) u = a dist (𝔼_{𝒢} (N)) v \land y dist (𝔼_{𝒢} (N)) u = b dist (𝔼_{𝒢} (N)) v))) \to z dist (𝔼_{𝒢} (N)) u = c dist (𝔼_{𝒢} (N)) v)$
159		simpll	$⊢ ((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (a \in {Base}_{𝔼_{𝒢} (N)} \land b \in {Base}_{𝔼_{𝒢} (N)})) \to N \in ℕ$
160	6	adantr	$⊢ ((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (a \in {Base}_{𝔼_{𝒢} (N)} \land b \in {Base}_{𝔼_{𝒢} (N)})) \to x \in 𝔼 (N)$
161	8	adantr	$⊢ ((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (a \in {Base}_{𝔼_{𝒢} (N)} \land b \in {Base}_{𝔼_{𝒢} (N)})) \to y \in 𝔼 (N)$
162		simprl	$⊢ ((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (a \in {Base}_{𝔼_{𝒢} (N)} \land b \in {Base}_{𝔼_{𝒢} (N)})) \to a \in {Base}_{𝔼_{𝒢} (N)}$
163	159 4	syl	$⊢ ((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (a \in {Base}_{𝔼_{𝒢} (N)} \land b \in {Base}_{𝔼_{𝒢} (N)})) \to 𝔼 (N) = {Base}_{𝔼_{𝒢} (N)}$
164	162 163	eleqtrrd	$⊢ ((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (a \in {Base}_{𝔼_{𝒢} (N)} \land b \in {Base}_{𝔼_{𝒢} (N)})) \to a \in 𝔼 (N)$
165		simprr	$⊢ ((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (a \in {Base}_{𝔼_{𝒢} (N)} \land b \in {Base}_{𝔼_{𝒢} (N)})) \to b \in {Base}_{𝔼_{𝒢} (N)}$
166	165 163	eleqtrrd	$⊢ ((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (a \in {Base}_{𝔼_{𝒢} (N)} \land b \in {Base}_{𝔼_{𝒢} (N)})) \to b \in 𝔼 (N)$
167		axsegcon	$⊢ (N \in ℕ \land (x \in 𝔼 (N) \land y \in 𝔼 (N)) \land (a \in 𝔼 (N) \land b \in 𝔼 (N))) \to \exists z \in 𝔼 (N) (y Btwn ⟨x, z⟩ \land ⟨y, z⟩ Cgr ⟨a, b⟩)$
168	159 160 161 164 166 167	syl122anc	$⊢ ((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (a \in {Base}_{𝔼_{𝒢} (N)} \land b \in {Base}_{𝔼_{𝒢} (N)})) \to \exists z \in 𝔼 (N) (y Btwn ⟨x, z⟩ \land ⟨y, z⟩ Cgr ⟨a, b⟩)$
169		simplll	$⊢ (((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (a \in {Base}_{𝔼_{𝒢} (N)} \land b \in {Base}_{𝔼_{𝒢} (N)})) \land z \in 𝔼 (N)) \to N \in ℕ$
170	3	ad2antrr	$⊢ (((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (a \in {Base}_{𝔼_{𝒢} (N)} \land b \in {Base}_{𝔼_{𝒢} (N)})) \land z \in 𝔼 (N)) \to x \in {Base}_{𝔼_{𝒢} (N)}$
171		simpr	$⊢ (((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (a \in {Base}_{𝔼_{𝒢} (N)} \land b \in {Base}_{𝔼_{𝒢} (N)})) \land z \in 𝔼 (N)) \to z \in 𝔼 (N)$
172	163	adantr	$⊢ (((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (a \in {Base}_{𝔼_{𝒢} (N)} \land b \in {Base}_{𝔼_{𝒢} (N)})) \land z \in 𝔼 (N)) \to 𝔼 (N) = {Base}_{𝔼_{𝒢} (N)}$
173	171 172	eleqtrd	$⊢ (((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (a \in {Base}_{𝔼_{𝒢} (N)} \land b \in {Base}_{𝔼_{𝒢} (N)})) \land z \in 𝔼 (N)) \to z \in {Base}_{𝔼_{𝒢} (N)}$
174	7	ad2antrr	$⊢ (((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (a \in {Base}_{𝔼_{𝒢} (N)} \land b \in {Base}_{𝔼_{𝒢} (N)})) \land z \in 𝔼 (N)) \to y \in {Base}_{𝔼_{𝒢} (N)}$
175	169 11 30 170 173 174	ebtwntg	$⊢ (((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (a \in {Base}_{𝔼_{𝒢} (N)} \land b \in {Base}_{𝔼_{𝒢} (N)})) \land z \in 𝔼 (N)) \to (y Btwn ⟨x, z⟩ \leftrightarrow y \in (x Itv (𝔼_{𝒢} (N)) z))$
176		simplrl	$⊢ (((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (a \in {Base}_{𝔼_{𝒢} (N)} \land b \in {Base}_{𝔼_{𝒢} (N)})) \land z \in 𝔼 (N)) \to a \in {Base}_{𝔼_{𝒢} (N)}$
177		simplrr	$⊢ (((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (a \in {Base}_{𝔼_{𝒢} (N)} \land b \in {Base}_{𝔼_{𝒢} (N)})) \land z \in 𝔼 (N)) \to b \in {Base}_{𝔼_{𝒢} (N)}$
178	169 11 12 174 173 176 177	ecgrtg	$⊢ (((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (a \in {Base}_{𝔼_{𝒢} (N)} \land b \in {Base}_{𝔼_{𝒢} (N)})) \land z \in 𝔼 (N)) \to (⟨y, z⟩ Cgr ⟨a, b⟩ \leftrightarrow y dist (𝔼_{𝒢} (N)) z = a dist (𝔼_{𝒢} (N)) b)$
179	175 178	anbi12d	$⊢ (((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (a \in {Base}_{𝔼_{𝒢} (N)} \land b \in {Base}_{𝔼_{𝒢} (N)})) \land z \in 𝔼 (N)) \to ((y Btwn ⟨x, z⟩ \land ⟨y, z⟩ Cgr ⟨a, b⟩) \leftrightarrow (y \in (x Itv (𝔼_{𝒢} (N)) z) \land y dist (𝔼_{𝒢} (N)) z = a dist (𝔼_{𝒢} (N)) b))$
180	163 179	rexeqbidva	$⊢ ((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (a \in {Base}_{𝔼_{𝒢} (N)} \land b \in {Base}_{𝔼_{𝒢} (N)})) \to (\exists z \in 𝔼 (N) (y Btwn ⟨x, z⟩ \land ⟨y, z⟩ Cgr ⟨a, b⟩) \leftrightarrow \exists z \in {Base}_{𝔼_{𝒢} (N)} (y \in (x Itv (𝔼_{𝒢} (N)) z) \land y dist (𝔼_{𝒢} (N)) z = a dist (𝔼_{𝒢} (N)) b))$
181	168 180	mpbid	$⊢ ((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \land (a \in {Base}_{𝔼_{𝒢} (N)} \land b \in {Base}_{𝔼_{𝒢} (N)})) \to \exists z \in {Base}_{𝔼_{𝒢} (N)} (y \in (x Itv (𝔼_{𝒢} (N)) z) \land y dist (𝔼_{𝒢} (N)) z = a dist (𝔼_{𝒢} (N)) b)$
182	181	ralrimivva	$⊢ (N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \to \forall a \in {Base}_{𝔼_{𝒢} (N)} \forall b \in {Base}_{𝔼_{𝒢} (N)} \exists z \in {Base}_{𝔼_{𝒢} (N)} (y \in (x Itv (𝔼_{𝒢} (N)) z) \land y dist (𝔼_{𝒢} (N)) z = a dist (𝔼_{𝒢} (N)) b)$
183	182	ralrimivva	$⊢ N \in ℕ \to \forall x \in {Base}_{𝔼_{𝒢} (N)} \forall y \in {Base}_{𝔼_{𝒢} (N)} \forall a \in {Base}_{𝔼_{𝒢} (N)} \forall b \in {Base}_{𝔼_{𝒢} (N)} \exists z \in {Base}_{𝔼_{𝒢} (N)} (y \in (x Itv (𝔼_{𝒢} (N)) z) \land y dist (𝔼_{𝒢} (N)) z = a dist (𝔼_{𝒢} (N)) b)$
184	1 158 183	jca32	$⊢ N \in ℕ \to (𝔼_{𝒢} (N) \in V \land (\forall x \in {Base}_{𝔼_{𝒢} (N)} \forall y \in {Base}_{𝔼_{𝒢} (N)} \forall z \in {Base}_{𝔼_{𝒢} (N)} \forall u \in {Base}_{𝔼_{𝒢} (N)} \forall a \in {Base}_{𝔼_{𝒢} (N)} \forall b \in {Base}_{𝔼_{𝒢} (N)} \forall c \in {Base}_{𝔼_{𝒢} (N)} \forall v \in {Base}_{𝔼_{𝒢} (N)} (((x \neq y \land y \in (x Itv (𝔼_{𝒢} (N)) z) \land b \in (a Itv (𝔼_{𝒢} (N)) c)) \land ((x dist (𝔼_{𝒢} (N)) y = a dist (𝔼_{𝒢} (N)) b \land y dist (𝔼_{𝒢} (N)) z = b dist (𝔼_{𝒢} (N)) c) \land (x dist (𝔼_{𝒢} (N)) u = a dist (𝔼_{𝒢} (N)) v \land y dist (𝔼_{𝒢} (N)) u = b dist (𝔼_{𝒢} (N)) v))) \to z dist (𝔼_{𝒢} (N)) u = c dist (𝔼_{𝒢} (N)) v) \land \forall x \in {Base}_{𝔼_{𝒢} (N)} \forall y \in {Base}_{𝔼_{𝒢} (N)} \forall a \in {Base}_{𝔼_{𝒢} (N)} \forall b \in {Base}_{𝔼_{𝒢} (N)} \exists z \in {Base}_{𝔼_{𝒢} (N)} (y \in (x Itv (𝔼_{𝒢} (N)) z) \land y dist (𝔼_{𝒢} (N)) z = a dist (𝔼_{𝒢} (N)) b)))$
185	11 12 30	istrkgcb	$⊢ 𝔼_{𝒢} (N) \in 𝒢_{Tarski}^{CB} \leftrightarrow (𝔼_{𝒢} (N) \in V \land (\forall x \in {Base}_{𝔼_{𝒢} (N)} \forall y \in {Base}_{𝔼_{𝒢} (N)} \forall z \in {Base}_{𝔼_{𝒢} (N)} \forall u \in {Base}_{𝔼_{𝒢} (N)} \forall a \in {Base}_{𝔼_{𝒢} (N)} \forall b \in {Base}_{𝔼_{𝒢} (N)} \forall c \in {Base}_{𝔼_{𝒢} (N)} \forall v \in {Base}_{𝔼_{𝒢} (N)} (((x \neq y \land y \in (x Itv (𝔼_{𝒢} (N)) z) \land b \in (a Itv (𝔼_{𝒢} (N)) c)) \land ((x dist (𝔼_{𝒢} (N)) y = a dist (𝔼_{𝒢} (N)) b \land y dist (𝔼_{𝒢} (N)) z = b dist (𝔼_{𝒢} (N)) c) \land (x dist (𝔼_{𝒢} (N)) u = a dist (𝔼_{𝒢} (N)) v \land y dist (𝔼_{𝒢} (N)) u = b dist (𝔼_{𝒢} (N)) v))) \to z dist (𝔼_{𝒢} (N)) u = c dist (𝔼_{𝒢} (N)) v) \land \forall x \in {Base}_{𝔼_{𝒢} (N)} \forall y \in {Base}_{𝔼_{𝒢} (N)} \forall a \in {Base}_{𝔼_{𝒢} (N)} \forall b \in {Base}_{𝔼_{𝒢} (N)} \exists z \in {Base}_{𝔼_{𝒢} (N)} (y \in (x Itv (𝔼_{𝒢} (N)) z) \land y dist (𝔼_{𝒢} (N)) z = a dist (𝔼_{𝒢} (N)) b)))$
186	184 185	sylibr	$⊢ N \in ℕ \to 𝔼_{𝒢} (N) \in 𝒢_{Tarski}^{CB}$
187	11 30	elntg	$⊢ N \in ℕ \to {Line}_{𝒢} (𝔼_{𝒢} (N)) = (x \in {Base}_{𝔼_{𝒢} (N)}, y \in ({Base}_{𝔼_{𝒢} (N)} ∖ \{x\}) ⟼ \{z \in {Base}_{𝔼_{𝒢} (N)} \| (z \in (x Itv (𝔼_{𝒢} (N)) y) \lor x \in (z Itv (𝔼_{𝒢} (N)) y) \lor y \in (x Itv (𝔼_{𝒢} (N)) z))\})$
188	11 12 30	istrkgl	$⊢ 𝔼_{𝒢} (N) \in \{f \| \underset{˙}{[} {Base}_{f} / p \underset{˙}{]} \underset{˙}{[} Itv (f) / i \underset{˙}{]} {Line}_{𝒢} (f) = (x \in p, y \in (p ∖ \{x\}) ⟼ \{z \in p \| (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))\})\} \leftrightarrow (𝔼_{𝒢} (N) \in V \land {Line}_{𝒢} (𝔼_{𝒢} (N)) = (x \in {Base}_{𝔼_{𝒢} (N)}, y \in ({Base}_{𝔼_{𝒢} (N)} ∖ \{x\}) ⟼ \{z \in {Base}_{𝔼_{𝒢} (N)} \| (z \in (x Itv (𝔼_{𝒢} (N)) y) \lor x \in (z Itv (𝔼_{𝒢} (N)) y) \lor y \in (x Itv (𝔼_{𝒢} (N)) z))\}))$
189	1 187 188	sylanbrc	$⊢ N \in ℕ \to 𝔼_{𝒢} (N) \in \{f \| \underset{˙}{[} {Base}_{f} / p \underset{˙}{]} \underset{˙}{[} Itv (f) / i \underset{˙}{]} {Line}_{𝒢} (f) = (x \in p, y \in (p ∖ \{x\}) ⟼ \{z \in p \| (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))\})\}$
190	186 189	elind	$⊢ N \in ℕ \to 𝔼_{𝒢} (N) \in (𝒢_{Tarski}^{CB} \cap \{f \| \underset{˙}{[} {Base}_{f} / p \underset{˙}{]} \underset{˙}{[} Itv (f) / i \underset{˙}{]} {Line}_{𝒢} (f) = (x \in p, y \in (p ∖ \{x\}) ⟼ \{z \in p \| (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))\})\})$
191	120 190	elind	$⊢ N \in ℕ \to 𝔼_{𝒢} (N) \in ((𝒢_{Tarski}^{C} \cap 𝒢_{Tarski}^{B}) \cap (𝒢_{Tarski}^{CB} \cap \{f \| \underset{˙}{[} {Base}_{f} / p \underset{˙}{]} \underset{˙}{[} Itv (f) / i \underset{˙}{]} {Line}_{𝒢} (f) = (x \in p, y \in (p ∖ \{x\}) ⟼ \{z \in p \| (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))\})\}))$
192		df-trkg	$⊢ 𝒢_{Tarski} = (𝒢_{Tarski}^{C} \cap 𝒢_{Tarski}^{B}) \cap (𝒢_{Tarski}^{CB} \cap \{f \| \underset{˙}{[} {Base}_{f} / p \underset{˙}{]} \underset{˙}{[} Itv (f) / i \underset{˙}{]} {Line}_{𝒢} (f) = (x \in p, y \in (p ∖ \{x\}) ⟼ \{z \in p \| (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))\})\})$
193	191 192	eleqtrrdi	$⊢ N \in ℕ \to 𝔼_{𝒢} (N) \in 𝒢_{Tarski}$

Metamath Proof Explorer

Theorem eengtrkg

Proof