Theorem istrkg2d

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

	Ref	Expression
Hypotheses	istrkg2d.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
	istrkg2d.d	⊢ − = ( dist ‘ 𝐺 )
	istrkg2d.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
Assertion	istrkg2d	⊢ ( 𝐺 ∈ TarskiG2D ↔ ( 𝐺 ∈ V ∧ ( ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( ( ( 𝑥 − 𝑢 ) = ( 𝑥 − 𝑣 ) ∧ ( 𝑦 − 𝑢 ) = ( 𝑦 − 𝑣 ) ∧ ( 𝑧 − 𝑢 ) = ( 𝑧 − 𝑣 ) ) ∧ 𝑢 ≠ 𝑣 ) → ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) ) )

Proof

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