Theorem istrkg2d 30744

Description: Property of fulfilling dimension 2 axiom. (Contributed by Thierry Arnoux, 29-May-2019.) (New usage is discouraged.) (Proof modification is discouraged.)

Hypotheses

Ref	Expression
istrkg2d.p	⊢ 𝑃 = (Base‘𝐺)
istrkg2d.d	⊢ − = (dist‘𝐺)
istrkg2d.i	⊢ 𝐼 = (Itv‘𝐺)

Assertion

Ref	Expression
istrkg2d	⊢ (𝐺 ∈ TarskiG2D ↔ (𝐺 ∈ V ∧ (∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((((𝑥 − 𝑢) = (𝑥 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑦 − 𝑣) ∧ (𝑧 − 𝑢) = (𝑧 − 𝑣)) ∧ 𝑢 ≠ 𝑣) → (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))))))

Distinct variable groups:   𝑢, − ,𝑣,𝑥,𝑦,𝑧   𝑢,𝐼,𝑣,𝑥,𝑦,𝑧   𝑢,𝑃,𝑣,𝑥,𝑦,𝑧

Allowed substitution hints:   𝐺(𝑥,𝑦,𝑧,𝑣,𝑢)

Proof of Theorem istrkg2d

Dummy variables 𝑑 𝑓 𝑖 𝑝 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		istrkg2d.p	. . 3 ⊢ 𝑃 = (Base‘𝐺)
2		istrkg2d.d	. . 3 ⊢ − = (dist‘𝐺)
3		istrkg2d.i	. . 3 ⊢ 𝐼 = (Itv‘𝐺)
4		simp1 1061	. . . . . 6 ⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → 𝑝 = 𝑃)
5	4	eqcomd 2628	. . . . 5 ⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → 𝑃 = 𝑝)
6		simp3 1063	. . . . . . . . . . . 12 ⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → 𝑖 = 𝐼)
7	6	eqcomd 2628	. . . . . . . . . . 11 ⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → 𝐼 = 𝑖)
8	7	oveqd 6667	. . . . . . . . . 10 ⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → (𝑥𝐼𝑦) = (𝑥𝑖𝑦))
9	8	eleq2d 2687	. . . . . . . . 9 ⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → (𝑧 ∈ (𝑥𝐼𝑦) ↔ 𝑧 ∈ (𝑥𝑖𝑦)))
10	7	oveqd 6667	. . . . . . . . . 10 ⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → (𝑧𝐼𝑦) = (𝑧𝑖𝑦))
11	10	eleq2d 2687	. . . . . . . . 9 ⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → (𝑥 ∈ (𝑧𝐼𝑦) ↔ 𝑥 ∈ (𝑧𝑖𝑦)))
12	7	oveqd 6667	. . . . . . . . . 10 ⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → (𝑥𝐼𝑧) = (𝑥𝑖𝑧))
13	12	eleq2d 2687	. . . . . . . . 9 ⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → (𝑦 ∈ (𝑥𝐼𝑧) ↔ 𝑦 ∈ (𝑥𝑖𝑧)))
14	9, 11, 13	3orbi123d 1398	. . . . . . . 8 ⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → ((𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)) ↔ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))))
15	14	notbid 308	. . . . . . 7 ⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → (¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)) ↔ ¬ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))))
16	5, 15	rexeqbidv 3153	. . . . . 6 ⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → (∃𝑧 ∈ 𝑃 ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)) ↔ ∃𝑧 ∈ 𝑝 ¬ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))))
17	5, 16	rexeqbidv 3153	. . . . 5 ⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → (∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)) ↔ ∃𝑦 ∈ 𝑝 ∃𝑧 ∈ 𝑝 ¬ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))))
18	5, 17	rexeqbidv 3153	. . . 4 ⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → (∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)) ↔ ∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 ∃𝑧 ∈ 𝑝 ¬ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))))
19		simp2 1062	. . . . . . . . . . . . . . 15 ⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → 𝑑 = − )
20	19	eqcomd 2628	. . . . . . . . . . . . . 14 ⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → − = 𝑑)
21	20	oveqd 6667	. . . . . . . . . . . . 13 ⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → (𝑥 − 𝑢) = (𝑥𝑑𝑢))
22	20	oveqd 6667	. . . . . . . . . . . . 13 ⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → (𝑥 − 𝑣) = (𝑥𝑑𝑣))
23	21, 22	eqeq12d 2637	. . . . . . . . . . . 12 ⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → ((𝑥 − 𝑢) = (𝑥 − 𝑣) ↔ (𝑥𝑑𝑢) = (𝑥𝑑𝑣)))
24	20	oveqd 6667	. . . . . . . . . . . . 13 ⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → (𝑦 − 𝑢) = (𝑦𝑑𝑢))
25	20	oveqd 6667	. . . . . . . . . . . . 13 ⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → (𝑦 − 𝑣) = (𝑦𝑑𝑣))
26	24, 25	eqeq12d 2637	. . . . . . . . . . . 12 ⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → ((𝑦 − 𝑢) = (𝑦 − 𝑣) ↔ (𝑦𝑑𝑢) = (𝑦𝑑𝑣)))
27	20	oveqd 6667	. . . . . . . . . . . . 13 ⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → (𝑧 − 𝑢) = (𝑧𝑑𝑢))
28	20	oveqd 6667	. . . . . . . . . . . . 13 ⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → (𝑧 − 𝑣) = (𝑧𝑑𝑣))
29	27, 28	eqeq12d 2637	. . . . . . . . . . . 12 ⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → ((𝑧 − 𝑢) = (𝑧 − 𝑣) ↔ (𝑧𝑑𝑢) = (𝑧𝑑𝑣)))
30	23, 26, 29	3anbi123d 1399	. . . . . . . . . . 11 ⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → (((𝑥 − 𝑢) = (𝑥 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑦 − 𝑣) ∧ (𝑧 − 𝑢) = (𝑧 − 𝑣)) ↔ ((𝑥𝑑𝑢) = (𝑥𝑑𝑣) ∧ (𝑦𝑑𝑢) = (𝑦𝑑𝑣) ∧ (𝑧𝑑𝑢) = (𝑧𝑑𝑣))))
31	30	anbi1d 741	. . . . . . . . . 10 ⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → ((((𝑥 − 𝑢) = (𝑥 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑦 − 𝑣) ∧ (𝑧 − 𝑢) = (𝑧 − 𝑣)) ∧ 𝑢 ≠ 𝑣) ↔ (((𝑥𝑑𝑢) = (𝑥𝑑𝑣) ∧ (𝑦𝑑𝑢) = (𝑦𝑑𝑣) ∧ (𝑧𝑑𝑢) = (𝑧𝑑𝑣)) ∧ 𝑢 ≠ 𝑣)))
32	31, 14	imbi12d 334	. . . . . . . . 9 ⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → (((((𝑥 − 𝑢) = (𝑥 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑦 − 𝑣) ∧ (𝑧 − 𝑢) = (𝑧 − 𝑣)) ∧ 𝑢 ≠ 𝑣) → (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))) ↔ ((((𝑥𝑑𝑢) = (𝑥𝑑𝑣) ∧ (𝑦𝑑𝑢) = (𝑦𝑑𝑣) ∧ (𝑧𝑑𝑢) = (𝑧𝑑𝑣)) ∧ 𝑢 ≠ 𝑣) → (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧)))))
33	5, 32	raleqbidv 3152	. . . . . . . 8 ⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → (∀𝑣 ∈ 𝑃 ((((𝑥 − 𝑢) = (𝑥 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑦 − 𝑣) ∧ (𝑧 − 𝑢) = (𝑧 − 𝑣)) ∧ 𝑢 ≠ 𝑣) → (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))) ↔ ∀𝑣 ∈ 𝑝 ((((𝑥𝑑𝑢) = (𝑥𝑑𝑣) ∧ (𝑦𝑑𝑢) = (𝑦𝑑𝑣) ∧ (𝑧𝑑𝑢) = (𝑧𝑑𝑣)) ∧ 𝑢 ≠ 𝑣) → (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧)))))
34	5, 33	raleqbidv 3152	. . . . . . 7 ⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → (∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((((𝑥 − 𝑢) = (𝑥 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑦 − 𝑣) ∧ (𝑧 − 𝑢) = (𝑧 − 𝑣)) ∧ 𝑢 ≠ 𝑣) → (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))) ↔ ∀𝑢 ∈ 𝑝 ∀𝑣 ∈ 𝑝 ((((𝑥𝑑𝑢) = (𝑥𝑑𝑣) ∧ (𝑦𝑑𝑢) = (𝑦𝑑𝑣) ∧ (𝑧𝑑𝑢) = (𝑧𝑑𝑣)) ∧ 𝑢 ≠ 𝑣) → (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧)))))
35	5, 34	raleqbidv 3152	. . . . . 6 ⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → (∀𝑧 ∈ 𝑃 ∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((((𝑥 − 𝑢) = (𝑥 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑦 − 𝑣) ∧ (𝑧 − 𝑢) = (𝑧 − 𝑣)) ∧ 𝑢 ≠ 𝑣) → (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))) ↔ ∀𝑧 ∈ 𝑝 ∀𝑢 ∈ 𝑝 ∀𝑣 ∈ 𝑝 ((((𝑥𝑑𝑢) = (𝑥𝑑𝑣) ∧ (𝑦𝑑𝑢) = (𝑦𝑑𝑣) ∧ (𝑧𝑑𝑢) = (𝑧𝑑𝑣)) ∧ 𝑢 ≠ 𝑣) → (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧)))))
36	5, 35	raleqbidv 3152	. . . . 5 ⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → (∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((((𝑥 − 𝑢) = (𝑥 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑦 − 𝑣) ∧ (𝑧 − 𝑢) = (𝑧 − 𝑣)) ∧ 𝑢 ≠ 𝑣) → (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))) ↔ ∀𝑦 ∈ 𝑝 ∀𝑧 ∈ 𝑝 ∀𝑢 ∈ 𝑝 ∀𝑣 ∈ 𝑝 ((((𝑥𝑑𝑢) = (𝑥𝑑𝑣) ∧ (𝑦𝑑𝑢) = (𝑦𝑑𝑣) ∧ (𝑧𝑑𝑢) = (𝑧𝑑𝑣)) ∧ 𝑢 ≠ 𝑣) → (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧)))))
37	5, 36	raleqbidv 3152	. . . 4 ⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((((𝑥 − 𝑢) = (𝑥 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑦 − 𝑣) ∧ (𝑧 − 𝑢) = (𝑧 − 𝑣)) ∧ 𝑢 ≠ 𝑣) → (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))) ↔ ∀𝑥 ∈ 𝑝 ∀𝑦 ∈ 𝑝 ∀𝑧 ∈ 𝑝 ∀𝑢 ∈ 𝑝 ∀𝑣 ∈ 𝑝 ((((𝑥𝑑𝑢) = (𝑥𝑑𝑣) ∧ (𝑦𝑑𝑢) = (𝑦𝑑𝑣) ∧ (𝑧𝑑𝑢) = (𝑧𝑑𝑣)) ∧ 𝑢 ≠ 𝑣) → (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧)))))
38	18, 37	anbi12d 747	. . 3 ⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → ((∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((((𝑥 − 𝑢) = (𝑥 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑦 − 𝑣) ∧ (𝑧 − 𝑢) = (𝑧 − 𝑣)) ∧ 𝑢 ≠ 𝑣) → (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)))) ↔ (∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 ∃𝑧 ∈ 𝑝 ¬ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ∀𝑥 ∈ 𝑝 ∀𝑦 ∈ 𝑝 ∀𝑧 ∈ 𝑝 ∀𝑢 ∈ 𝑝 ∀𝑣 ∈ 𝑝 ((((𝑥𝑑𝑢) = (𝑥𝑑𝑣) ∧ (𝑦𝑑𝑢) = (𝑦𝑑𝑣) ∧ (𝑧𝑑𝑢) = (𝑧𝑑𝑣)) ∧ 𝑢 ≠ 𝑣) → (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))))))
39	1, 2, 3, 38	sbcie3s 15917	. 2 ⊢ (𝑓 = 𝐺 → ([(Base‘𝑓) / 𝑝][(dist‘𝑓) / 𝑑][(Itv‘𝑓) / 𝑖](∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 ∃𝑧 ∈ 𝑝 ¬ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ∀𝑥 ∈ 𝑝 ∀𝑦 ∈ 𝑝 ∀𝑧 ∈ 𝑝 ∀𝑢 ∈ 𝑝 ∀𝑣 ∈ 𝑝 ((((𝑥𝑑𝑢) = (𝑥𝑑𝑣) ∧ (𝑦𝑑𝑢) = (𝑦𝑑𝑣) ∧ (𝑧𝑑𝑢) = (𝑧𝑑𝑣)) ∧ 𝑢 ≠ 𝑣) → (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧)))) ↔ (∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((((𝑥 − 𝑢) = (𝑥 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑦 − 𝑣) ∧ (𝑧 − 𝑢) = (𝑧 − 𝑣)) ∧ 𝑢 ≠ 𝑣) → (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))))))
40		df-trkg2d 30743	. 2 ⊢ TarskiG2D = {𝑓 ∣ [(Base‘𝑓) / 𝑝][(dist‘𝑓) / 𝑑][(Itv‘𝑓) / 𝑖](∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 ∃𝑧 ∈ 𝑝 ¬ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ∀𝑥 ∈ 𝑝 ∀𝑦 ∈ 𝑝 ∀𝑧 ∈ 𝑝 ∀𝑢 ∈ 𝑝 ∀𝑣 ∈ 𝑝 ((((𝑥𝑑𝑢) = (𝑥𝑑𝑣) ∧ (𝑦𝑑𝑢) = (𝑦𝑑𝑣) ∧ (𝑧𝑑𝑢) = (𝑧𝑑𝑣)) ∧ 𝑢 ≠ 𝑣) → (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))))}
41	39, 40	elab4g 3355	1 ⊢ (𝐺 ∈ TarskiG2D ↔ (𝐺 ∈ V ∧ (∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((((𝑥 − 𝑢) = (𝑥 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑦 − 𝑣) ∧ (𝑧 − 𝑢) = (𝑧 − 𝑣)) ∧ 𝑢 ≠ 𝑣) → (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 384   ∨ w3o 1036   ∧ w3a 1037   = wceq 1483   ∈ wcel 1990   ≠ wne 2794  ∀wral 2912  ∃wrex 2913  Vcvv 3200  [wsbc 3435  ‘cfv 5888  (class class class)co 6650  Basecbs 15857  distcds 15950  Itvcitv 25335  TarskiG_2Dcstrkg2d 30742

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-nul 4789

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-iota 5851  df-fv 5896  df-ov 6653  df-trkg2d 30743

This theorem is referenced by:  axtglowdim2OLD  30745  axtgupdim2OLD  30746