eengtrkge

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

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

Proof

Step	Hyp	Ref	Expression
1		fvexd	$⊢ N \in ℕ \to 𝔼_{𝒢} (N) \in V$
2		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 ℕ$
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	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)$
8		simprr	$⊢ (N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \to y \in {Base}_{𝔼_{𝒢} (N)}$
9	8 5	eleqtrrd	$⊢ (N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)})) \to y \in 𝔼 (N)$
10	9	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)$
11	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)}$
12	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 {Base}_{𝔼_{𝒢} (N)}$
13		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)}$
14		simpr3	$⊢ (N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)} \land z \in {Base}_{𝔼_{𝒢} (N)})) \to z \in {Base}_{𝔼_{𝒢} (N)}$
15	4	adantr	$⊢ (N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)} \land z \in {Base}_{𝔼_{𝒢} (N)})) \to 𝔼 (N) = {Base}_{𝔼_{𝒢} (N)}$
16	14 15	eleqtrrd	$⊢ (N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in {Base}_{𝔼_{𝒢} (N)} \land z \in {Base}_{𝔼_{𝒢} (N)})) \to z \in 𝔼 (N)$
17	2 11 12 13 16	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)$
18		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)}$
19	4	ad2antrr	$⊢ ((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)}$
20	18 19	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)$
21		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)}$
22	21 19	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)$
23		axeuclid	$⊢ (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, v⟩ \land u Btwn ⟨y, z⟩ \land x \neq u) \to \exists a \in 𝔼 (N) \exists b \in 𝔼 (N) (y Btwn ⟨x, a⟩ \land z Btwn ⟨x, b⟩ \land v Btwn ⟨a, b⟩))$
24	2 7 10 17 20 22 23	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, v⟩ \land u Btwn ⟨y, z⟩ \land x \neq u) \to \exists a \in 𝔼 (N) \exists b \in 𝔼 (N) (y Btwn ⟨x, a⟩ \land z Btwn ⟨x, b⟩ \land v Btwn ⟨a, b⟩))$
25		eqid	$⊢ {Base}_{𝔼_{𝒢} (N)} = {Base}_{𝔼_{𝒢} (N)}$
26		eqid	$⊢ Itv (𝔼_{𝒢} (N)) = Itv (𝔼_{𝒢} (N))$
27	2 25 26 11 21 18	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, v⟩ \leftrightarrow u \in (x Itv (𝔼_{𝒢} (N)) v))$
28	2 25 26 12 13 18	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 ⟨y, z⟩ \leftrightarrow u \in (y Itv (𝔼_{𝒢} (N)) z))$
29	27 28	3anbi12d	$⊢ ((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, v⟩ \land u Btwn ⟨y, z⟩ \land x \neq u) \leftrightarrow (u \in (x Itv (𝔼_{𝒢} (N)) v) \land u \in (y Itv (𝔼_{𝒢} (N)) z) \land x \neq u))$
30	19	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)}$
31	2	ad2antrr	$⊢ ((((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)) \land b \in 𝔼 (N)) \to N \in ℕ$
32	11	ad2antrr	$⊢ ((((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)) \land b \in 𝔼 (N)) \to x \in {Base}_{𝔼_{𝒢} (N)}$
33		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)$
34	33 30	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)}$
35	34	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)) \land b \in 𝔼 (N)) \to a \in {Base}_{𝔼_{𝒢} (N)}$
36	12	ad2antrr	$⊢ ((((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)) \land b \in 𝔼 (N)) \to y \in {Base}_{𝔼_{𝒢} (N)}$
37	31 25 26 32 35 36	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)) \land b \in 𝔼 (N)) \to (y Btwn ⟨x, a⟩ \leftrightarrow y \in (x Itv (𝔼_{𝒢} (N)) a))$
38		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)) \land b \in 𝔼 (N)) \to b \in 𝔼 (N)$
39	19	ad2antrr	$⊢ ((((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)) \land b \in 𝔼 (N)) \to 𝔼 (N) = {Base}_{𝔼_{𝒢} (N)}$
40	38 39	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)) \land b \in 𝔼 (N)) \to b \in {Base}_{𝔼_{𝒢} (N)}$
41	13	ad2antrr	$⊢ ((((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)) \land b \in 𝔼 (N)) \to z \in {Base}_{𝔼_{𝒢} (N)}$
42	31 25 26 32 40 41	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)) \land b \in 𝔼 (N)) \to (z Btwn ⟨x, b⟩ \leftrightarrow z \in (x Itv (𝔼_{𝒢} (N)) b))$
43	21	ad2antrr	$⊢ ((((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)) \land b \in 𝔼 (N)) \to v \in {Base}_{𝔼_{𝒢} (N)}$
44	31 25 26 35 40 43	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)) \land b \in 𝔼 (N)) \to (v Btwn ⟨a, b⟩ \leftrightarrow v \in (a Itv (𝔼_{𝒢} (N)) b))$
45	37 42 44	3anbi123d	$⊢ ((((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)) \land b \in 𝔼 (N)) \to ((y Btwn ⟨x, a⟩ \land z Btwn ⟨x, b⟩ \land v Btwn ⟨a, b⟩) \leftrightarrow (y \in (x Itv (𝔼_{𝒢} (N)) a) \land z \in (x Itv (𝔼_{𝒢} (N)) b) \land v \in (a Itv (𝔼_{𝒢} (N)) b)))$
46	30 45	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)})) \land a \in 𝔼 (N)) \to (\exists b \in 𝔼 (N) (y Btwn ⟨x, a⟩ \land z Btwn ⟨x, b⟩ \land v Btwn ⟨a, b⟩) \leftrightarrow \exists b \in {Base}_{𝔼_{𝒢} (N)} (y \in (x Itv (𝔼_{𝒢} (N)) a) \land z \in (x Itv (𝔼_{𝒢} (N)) b) \land v \in (a Itv (𝔼_{𝒢} (N)) b)))$
47	19 46	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) \exists b \in 𝔼 (N) (y Btwn ⟨x, a⟩ \land z Btwn ⟨x, b⟩ \land v Btwn ⟨a, b⟩) \leftrightarrow \exists a \in {Base}_{𝔼_{𝒢} (N)} \exists b \in {Base}_{𝔼_{𝒢} (N)} (y \in (x Itv (𝔼_{𝒢} (N)) a) \land z \in (x Itv (𝔼_{𝒢} (N)) b) \land v \in (a Itv (𝔼_{𝒢} (N)) b)))$
48	24 29 47	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)) v) \land u \in (y Itv (𝔼_{𝒢} (N)) z) \land x \neq u) \to \exists a \in {Base}_{𝔼_{𝒢} (N)} \exists b \in {Base}_{𝔼_{𝒢} (N)} (y \in (x Itv (𝔼_{𝒢} (N)) a) \land z \in (x Itv (𝔼_{𝒢} (N)) b) \land v \in (a Itv (𝔼_{𝒢} (N)) b)))$
49	48	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)) v) \land u \in (y Itv (𝔼_{𝒢} (N)) z) \land x \neq u) \to \exists a \in {Base}_{𝔼_{𝒢} (N)} \exists b \in {Base}_{𝔼_{𝒢} (N)} (y \in (x Itv (𝔼_{𝒢} (N)) a) \land z \in (x Itv (𝔼_{𝒢} (N)) b) \land v \in (a Itv (𝔼_{𝒢} (N)) b)))$
50	49	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)) v) \land u \in (y Itv (𝔼_{𝒢} (N)) z) \land x \neq u) \to \exists a \in {Base}_{𝔼_{𝒢} (N)} \exists b \in {Base}_{𝔼_{𝒢} (N)} (y \in (x Itv (𝔼_{𝒢} (N)) a) \land z \in (x Itv (𝔼_{𝒢} (N)) b) \land v \in (a Itv (𝔼_{𝒢} (N)) b)))$
51		eqid	$⊢ dist (𝔼_{𝒢} (N)) = dist (𝔼_{𝒢} (N))$
52	25 51 26	istrkge	$⊢ 𝔼_{𝒢} (N) \in 𝒢_{Tarski}^{E} \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 v \in {Base}_{𝔼_{𝒢} (N)} ((u \in (x Itv (𝔼_{𝒢} (N)) v) \land u \in (y Itv (𝔼_{𝒢} (N)) z) \land x \neq u) \to \exists a \in {Base}_{𝔼_{𝒢} (N)} \exists b \in {Base}_{𝔼_{𝒢} (N)} (y \in (x Itv (𝔼_{𝒢} (N)) a) \land z \in (x Itv (𝔼_{𝒢} (N)) b) \land v \in (a Itv (𝔼_{𝒢} (N)) b))))$
53	1 50 52	sylanbrc	$⊢ N \in ℕ \to 𝔼_{𝒢} (N) \in 𝒢_{Tarski}^{E}$

Metamath Proof Explorer

Theorem eengtrkge

Proof