Theorem istrkg2d 32646

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 1135	. . . . . 6 ⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → 𝑝 = 𝑃)
5	4	eqcomd 2744	. . . . 5 ⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → 𝑃 = 𝑝)
6		simp3 1137	. . . . . . . . . . . 12 ⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → 𝑖 = 𝐼)
7	6	eqcomd 2744	. . . . . . . . . . 11 ⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → 𝐼 = 𝑖)
8	7	oveqd 7292	. . . . . . . . . 10 ⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → (𝑥𝐼𝑦) = (𝑥𝑖𝑦))
9	8	eleq2d 2824	. . . . . . . . 9 ⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → (𝑧 ∈ (𝑥𝐼𝑦) ↔ 𝑧 ∈ (𝑥𝑖𝑦)))
10	7	oveqd 7292	. . . . . . . . . 10 ⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → (𝑧𝐼𝑦) = (𝑧𝑖𝑦))
11	10	eleq2d 2824	. . . . . . . . 9 ⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → (𝑥 ∈ (𝑧𝐼𝑦) ↔ 𝑥 ∈ (𝑧𝑖𝑦)))
12	7	oveqd 7292	. . . . . . . . . 10 ⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → (𝑥𝐼𝑧) = (𝑥𝑖𝑧))
13	12	eleq2d 2824	. . . . . . . . 9 ⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → (𝑦 ∈ (𝑥𝐼𝑧) ↔ 𝑦 ∈ (𝑥𝑖𝑧)))
14	9, 11, 13	3orbi123d 1434	. . . . . . . 8 ⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → ((𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)) ↔ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))))
15	14	notbid 318	. . . . . . 7 ⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → (¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)) ↔ ¬ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))))
16	5, 15	rexeqbidv 3337	. . . . . 6 ⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → (∃𝑧 ∈ 𝑃 ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)) ↔ ∃𝑧 ∈ 𝑝 ¬ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))))
17	5, 16	rexeqbidv 3337	. . . . 5 ⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → (∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)) ↔ ∃𝑦 ∈ 𝑝 ∃𝑧 ∈ 𝑝 ¬ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))))
18	5, 17	rexeqbidv 3337	. . . 4 ⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → (∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)) ↔ ∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 ∃𝑧 ∈ 𝑝 ¬ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))))
19		simp2 1136	. . . . . . . . . . . . . . 15 ⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → 𝑑 = − )
20	19	eqcomd 2744	. . . . . . . . . . . . . 14 ⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → − = 𝑑)
21	20	oveqd 7292	. . . . . . . . . . . . 13 ⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → (𝑥 − 𝑢) = (𝑥𝑑𝑢))
22	20	oveqd 7292	. . . . . . . . . . . . 13 ⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → (𝑥 − 𝑣) = (𝑥𝑑𝑣))
23	21, 22	eqeq12d 2754	. . . . . . . . . . . 12 ⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → ((𝑥 − 𝑢) = (𝑥 − 𝑣) ↔ (𝑥𝑑𝑢) = (𝑥𝑑𝑣)))
24	20	oveqd 7292	. . . . . . . . . . . . 13 ⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → (𝑦 − 𝑢) = (𝑦𝑑𝑢))
25	20	oveqd 7292	. . . . . . . . . . . . 13 ⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → (𝑦 − 𝑣) = (𝑦𝑑𝑣))
26	24, 25	eqeq12d 2754	. . . . . . . . . . . 12 ⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → ((𝑦 − 𝑢) = (𝑦 − 𝑣) ↔ (𝑦𝑑𝑢) = (𝑦𝑑𝑣)))
27	20	oveqd 7292	. . . . . . . . . . . . 13 ⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → (𝑧 − 𝑢) = (𝑧𝑑𝑢))
28	20	oveqd 7292	. . . . . . . . . . . . 13 ⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → (𝑧 − 𝑣) = (𝑧𝑑𝑣))
29	27, 28	eqeq12d 2754	. . . . . . . . . . . 12 ⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → ((𝑧 − 𝑢) = (𝑧 − 𝑣) ↔ (𝑧𝑑𝑢) = (𝑧𝑑𝑣)))
30	23, 26, 29	3anbi123d 1435	. . . . . . . . . . 11 ⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → (((𝑥 − 𝑢) = (𝑥 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑦 − 𝑣) ∧ (𝑧 − 𝑢) = (𝑧 − 𝑣)) ↔ ((𝑥𝑑𝑢) = (𝑥𝑑𝑣) ∧ (𝑦𝑑𝑢) = (𝑦𝑑𝑣) ∧ (𝑧𝑑𝑢) = (𝑧𝑑𝑣))))
31	30	anbi1d 630	. . . . . . . . . 10 ⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → ((((𝑥 − 𝑢) = (𝑥 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑦 − 𝑣) ∧ (𝑧 − 𝑢) = (𝑧 − 𝑣)) ∧ 𝑢 ≠ 𝑣) ↔ (((𝑥𝑑𝑢) = (𝑥𝑑𝑣) ∧ (𝑦𝑑𝑢) = (𝑦𝑑𝑣) ∧ (𝑧𝑑𝑢) = (𝑧𝑑𝑣)) ∧ 𝑢 ≠ 𝑣)))
32	31, 14	imbi12d 345	. . . . . . . . 9 ⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → (((((𝑥 − 𝑢) = (𝑥 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑦 − 𝑣) ∧ (𝑧 − 𝑢) = (𝑧 − 𝑣)) ∧ 𝑢 ≠ 𝑣) → (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))) ↔ ((((𝑥𝑑𝑢) = (𝑥𝑑𝑣) ∧ (𝑦𝑑𝑢) = (𝑦𝑑𝑣) ∧ (𝑧𝑑𝑢) = (𝑧𝑑𝑣)) ∧ 𝑢 ≠ 𝑣) → (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧)))))
33	5, 32	raleqbidv 3336	. . . . . . . 8 ⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → (∀𝑣 ∈ 𝑃 ((((𝑥 − 𝑢) = (𝑥 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑦 − 𝑣) ∧ (𝑧 − 𝑢) = (𝑧 − 𝑣)) ∧ 𝑢 ≠ 𝑣) → (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))) ↔ ∀𝑣 ∈ 𝑝 ((((𝑥𝑑𝑢) = (𝑥𝑑𝑣) ∧ (𝑦𝑑𝑢) = (𝑦𝑑𝑣) ∧ (𝑧𝑑𝑢) = (𝑧𝑑𝑣)) ∧ 𝑢 ≠ 𝑣) → (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧)))))
34	5, 33	raleqbidv 3336	. . . . . . 7 ⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → (∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((((𝑥 − 𝑢) = (𝑥 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑦 − 𝑣) ∧ (𝑧 − 𝑢) = (𝑧 − 𝑣)) ∧ 𝑢 ≠ 𝑣) → (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))) ↔ ∀𝑢 ∈ 𝑝 ∀𝑣 ∈ 𝑝 ((((𝑥𝑑𝑢) = (𝑥𝑑𝑣) ∧ (𝑦𝑑𝑢) = (𝑦𝑑𝑣) ∧ (𝑧𝑑𝑢) = (𝑧𝑑𝑣)) ∧ 𝑢 ≠ 𝑣) → (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧)))))
35	5, 34	raleqbidv 3336	. . . . . 6 ⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → (∀𝑧 ∈ 𝑃 ∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((((𝑥 − 𝑢) = (𝑥 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑦 − 𝑣) ∧ (𝑧 − 𝑢) = (𝑧 − 𝑣)) ∧ 𝑢 ≠ 𝑣) → (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))) ↔ ∀𝑧 ∈ 𝑝 ∀𝑢 ∈ 𝑝 ∀𝑣 ∈ 𝑝 ((((𝑥𝑑𝑢) = (𝑥𝑑𝑣) ∧ (𝑦𝑑𝑢) = (𝑦𝑑𝑣) ∧ (𝑧𝑑𝑢) = (𝑧𝑑𝑣)) ∧ 𝑢 ≠ 𝑣) → (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧)))))
36	5, 35	raleqbidv 3336	. . . . 5 ⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → (∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((((𝑥 − 𝑢) = (𝑥 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑦 − 𝑣) ∧ (𝑧 − 𝑢) = (𝑧 − 𝑣)) ∧ 𝑢 ≠ 𝑣) → (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))) ↔ ∀𝑦 ∈ 𝑝 ∀𝑧 ∈ 𝑝 ∀𝑢 ∈ 𝑝 ∀𝑣 ∈ 𝑝 ((((𝑥𝑑𝑢) = (𝑥𝑑𝑣) ∧ (𝑦𝑑𝑢) = (𝑦𝑑𝑣) ∧ (𝑧𝑑𝑢) = (𝑧𝑑𝑣)) ∧ 𝑢 ≠ 𝑣) → (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧)))))
37	5, 36	raleqbidv 3336	. . . 4 ⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((((𝑥 − 𝑢) = (𝑥 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑦 − 𝑣) ∧ (𝑧 − 𝑢) = (𝑧 − 𝑣)) ∧ 𝑢 ≠ 𝑣) → (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))) ↔ ∀𝑥 ∈ 𝑝 ∀𝑦 ∈ 𝑝 ∀𝑧 ∈ 𝑝 ∀𝑢 ∈ 𝑝 ∀𝑣 ∈ 𝑝 ((((𝑥𝑑𝑢) = (𝑥𝑑𝑣) ∧ (𝑦𝑑𝑢) = (𝑦𝑑𝑣) ∧ (𝑧𝑑𝑢) = (𝑧𝑑𝑣)) ∧ 𝑢 ≠ 𝑣) → (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧)))))
38	18, 37	anbi12d 631	. . 3 ⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → ((∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((((𝑥 − 𝑢) = (𝑥 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑦 − 𝑣) ∧ (𝑧 − 𝑢) = (𝑧 − 𝑣)) ∧ 𝑢 ≠ 𝑣) → (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)))) ↔ (∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 ∃𝑧 ∈ 𝑝 ¬ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ∀𝑥 ∈ 𝑝 ∀𝑦 ∈ 𝑝 ∀𝑧 ∈ 𝑝 ∀𝑢 ∈ 𝑝 ∀𝑣 ∈ 𝑝 ((((𝑥𝑑𝑢) = (𝑥𝑑𝑣) ∧ (𝑦𝑑𝑢) = (𝑦𝑑𝑣) ∧ (𝑧𝑑𝑢) = (𝑧𝑑𝑣)) ∧ 𝑢 ≠ 𝑣) → (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))))))
39	1, 2, 3, 38	sbcie3s 16863	. 2 ⊢ (𝑓 = 𝐺 → ([(Base‘𝑓) / 𝑝][(dist‘𝑓) / 𝑑][(Itv‘𝑓) / 𝑖](∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 ∃𝑧 ∈ 𝑝 ¬ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ∀𝑥 ∈ 𝑝 ∀𝑦 ∈ 𝑝 ∀𝑧 ∈ 𝑝 ∀𝑢 ∈ 𝑝 ∀𝑣 ∈ 𝑝 ((((𝑥𝑑𝑢) = (𝑥𝑑𝑣) ∧ (𝑦𝑑𝑢) = (𝑦𝑑𝑣) ∧ (𝑧𝑑𝑢) = (𝑧𝑑𝑣)) ∧ 𝑢 ≠ 𝑣) → (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧)))) ↔ (∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((((𝑥 − 𝑢) = (𝑥 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑦 − 𝑣) ∧ (𝑧 − 𝑢) = (𝑧 − 𝑣)) ∧ 𝑢 ≠ 𝑣) → (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))))))
40		df-trkg2d 32645	. 2 ⊢ TarskiG2D = {𝑓 ∣ [(Base‘𝑓) / 𝑝][(dist‘𝑓) / 𝑑][(Itv‘𝑓) / 𝑖](∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 ∃𝑧 ∈ 𝑝 ¬ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ∀𝑥 ∈ 𝑝 ∀𝑦 ∈ 𝑝 ∀𝑧 ∈ 𝑝 ∀𝑢 ∈ 𝑝 ∀𝑣 ∈ 𝑝 ((((𝑥𝑑𝑢) = (𝑥𝑑𝑣) ∧ (𝑦𝑑𝑢) = (𝑦𝑑𝑣) ∧ (𝑧𝑑𝑢) = (𝑧𝑑𝑣)) ∧ 𝑢 ≠ 𝑣) → (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))))}
41	39, 40	elab4g 3614	1 ⊢ (𝐺 ∈ TarskiG2D ↔ (𝐺 ∈ V ∧ (∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((((𝑥 − 𝑢) = (𝑥 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑦 − 𝑣) ∧ (𝑧 − 𝑢) = (𝑧 − 𝑣)) ∧ 𝑢 ≠ 𝑣) → (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   ∨ w3o 1085   ∧ w3a 1086   = wceq 1539   ∈ wcel 2106   ≠ wne 2943  ∀wral 3064  ∃wrex 3065  Vcvv 3432  [wsbc 3716  ‘cfv 6433  (class class class)co 7275  Basecbs 16912  distcds 16971  Itvcitv 26794  TarskiG_2Dcstrkg2d 32644

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-nul 5230

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-sbc 3717  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-iota 6391  df-fv 6441  df-ov 7278  df-trkg2d 32645

This theorem is referenced by:  axtglowdim2ALTV  32647  axtgupdim2ALTV  32648