Theorem istrkgld

Description: Property of fulfilling the lower dimension N axiom. (Contributed by Thierry Arnoux, 20-Nov-2019)

	Ref	Expression
Hypotheses	istrkg.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
	istrkg.d	⊢ − = ( dist ‘ 𝐺 )
	istrkg.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
Assertion	istrkgld	⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝐺 DimTarskiG≥ 𝑁 ↔ ∃ 𝑓 ( 𝑓 : ( 1 ..^ 𝑁 ) –1-1→ 𝑃 ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ∀ 𝑗 ∈ ( 2 ..^ 𝑁 ) ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		istrkg.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		istrkg.d	⊢ − = ( dist ‘ 𝐺 )
3		istrkg.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
4		eqidd	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) → 𝑓 = 𝑓 )
5		eqidd	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) → ( 1 ..^ 𝑛 ) = ( 1 ..^ 𝑛 ) )
6		simp1	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) → 𝑝 = 𝑃 )
7	6	eqcomd	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) → 𝑃 = 𝑝 )
8	4 5 7	f1eq123d	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) → ( 𝑓 : ( 1 ..^ 𝑛 ) –1-1→ 𝑃 ↔ 𝑓 : ( 1 ..^ 𝑛 ) –1-1→ 𝑝 ) )
9		simp2	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) → 𝑑 = − )
10	9	eqcomd	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) → − = 𝑑 )
11	10	oveqd	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) → ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 1 ) 𝑑 𝑥 ) )
12	10	oveqd	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) → ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑥 ) )
13	11 12	eqeq12d	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) → ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) ↔ ( ( 𝑓 ‘ 1 ) 𝑑 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑥 ) ) )
14	10	oveqd	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) → ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 1 ) 𝑑 𝑦 ) )
15	10	oveqd	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) → ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑦 ) )
16	14 15	eqeq12d	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) → ( ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) ↔ ( ( 𝑓 ‘ 1 ) 𝑑 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑦 ) ) )
17	10	oveqd	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) → ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 1 ) 𝑑 𝑧 ) )
18	10	oveqd	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) → ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑧 ) )
19	17 18	eqeq12d	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) → ( ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) ↔ ( ( 𝑓 ‘ 1 ) 𝑑 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑧 ) ) )
20	13 16 19	3anbi123d	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) → ( ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) ) ↔ ( ( ( 𝑓 ‘ 1 ) 𝑑 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) 𝑑 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) 𝑑 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑧 ) ) ) )
21	20	ralbidv	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) → ( ∀ 𝑗 ∈ ( 2 ..^ 𝑛 ) ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) ) ↔ ∀ 𝑗 ∈ ( 2 ..^ 𝑛 ) ( ( ( 𝑓 ‘ 1 ) 𝑑 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) 𝑑 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) 𝑑 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑧 ) ) ) )
22		simp3	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) → 𝑖 = 𝐼 )
23	22	eqcomd	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) → 𝐼 = 𝑖 )
24	23	oveqd	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) → ( 𝑥 𝐼 𝑦 ) = ( 𝑥 𝑖 𝑦 ) )
25	24	eleq2d	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) → ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ↔ 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ) )
26	23	oveqd	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) → ( 𝑧 𝐼 𝑦 ) = ( 𝑧 𝑖 𝑦 ) )
27	26	eleq2d	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) → ( 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ↔ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ) )
28	23	oveqd	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) → ( 𝑥 𝐼 𝑧 ) = ( 𝑥 𝑖 𝑧 ) )
29	28	eleq2d	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) → ( 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ↔ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) )
30	25 27 29	3orbi123d	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) → ( ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ↔ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) ) )
31	30	notbid	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) → ( ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ↔ ¬ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) ) )
32	21 31	anbi12d	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) → ( ( ∀ 𝑗 ∈ ( 2 ..^ 𝑛 ) ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ↔ ( ∀ 𝑗 ∈ ( 2 ..^ 𝑛 ) ( ( ( 𝑓 ‘ 1 ) 𝑑 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) 𝑑 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) 𝑑 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) ) ) )
33	7 32	rexeqbidv	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) → ( ∃ 𝑧 ∈ 𝑃 ( ∀ 𝑗 ∈ ( 2 ..^ 𝑛 ) ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ↔ ∃ 𝑧 ∈ 𝑝 ( ∀ 𝑗 ∈ ( 2 ..^ 𝑛 ) ( ( ( 𝑓 ‘ 1 ) 𝑑 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) 𝑑 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) 𝑑 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) ) ) )
34	7 33	rexeqbidv	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) → ( ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ∀ 𝑗 ∈ ( 2 ..^ 𝑛 ) ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ↔ ∃ 𝑦 ∈ 𝑝 ∃ 𝑧 ∈ 𝑝 ( ∀ 𝑗 ∈ ( 2 ..^ 𝑛 ) ( ( ( 𝑓 ‘ 1 ) 𝑑 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) 𝑑 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) 𝑑 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) ) ) )
35	7 34	rexeqbidv	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) → ( ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ∀ 𝑗 ∈ ( 2 ..^ 𝑛 ) ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ↔ ∃ 𝑥 ∈ 𝑝 ∃ 𝑦 ∈ 𝑝 ∃ 𝑧 ∈ 𝑝 ( ∀ 𝑗 ∈ ( 2 ..^ 𝑛 ) ( ( ( 𝑓 ‘ 1 ) 𝑑 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) 𝑑 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) 𝑑 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) ) ) )
36	8 35	anbi12d	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) → ( ( 𝑓 : ( 1 ..^ 𝑛 ) –1-1→ 𝑃 ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ∀ 𝑗 ∈ ( 2 ..^ 𝑛 ) ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) ↔ ( 𝑓 : ( 1 ..^ 𝑛 ) –1-1→ 𝑝 ∧ ∃ 𝑥 ∈ 𝑝 ∃ 𝑦 ∈ 𝑝 ∃ 𝑧 ∈ 𝑝 ( ∀ 𝑗 ∈ ( 2 ..^ 𝑛 ) ( ( ( 𝑓 ‘ 1 ) 𝑑 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) 𝑑 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) 𝑑 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) ) ) ) )
37	36	exbidv	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) → ( ∃ 𝑓 ( 𝑓 : ( 1 ..^ 𝑛 ) –1-1→ 𝑃 ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ∀ 𝑗 ∈ ( 2 ..^ 𝑛 ) ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) ↔ ∃ 𝑓 ( 𝑓 : ( 1 ..^ 𝑛 ) –1-1→ 𝑝 ∧ ∃ 𝑥 ∈ 𝑝 ∃ 𝑦 ∈ 𝑝 ∃ 𝑧 ∈ 𝑝 ( ∀ 𝑗 ∈ ( 2 ..^ 𝑛 ) ( ( ( 𝑓 ‘ 1 ) 𝑑 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) 𝑑 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) 𝑑 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) ) ) ) )
38	1 2 3 37	sbcie3s	⊢ ( 𝑔 = 𝐺 → ( [ ( Base ‘ 𝑔 ) / 𝑝 ] [ ( dist ‘ 𝑔 ) / 𝑑 ] [ ( Itv ‘ 𝑔 ) / 𝑖 ] ∃ 𝑓 ( 𝑓 : ( 1 ..^ 𝑛 ) –1-1→ 𝑝 ∧ ∃ 𝑥 ∈ 𝑝 ∃ 𝑦 ∈ 𝑝 ∃ 𝑧 ∈ 𝑝 ( ∀ 𝑗 ∈ ( 2 ..^ 𝑛 ) ( ( ( 𝑓 ‘ 1 ) 𝑑 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) 𝑑 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) 𝑑 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) ) ) ↔ ∃ 𝑓 ( 𝑓 : ( 1 ..^ 𝑛 ) –1-1→ 𝑃 ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ∀ 𝑗 ∈ ( 2 ..^ 𝑛 ) ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) ) )
39		eqidd	⊢ ( 𝑛 = 𝑁 → 𝑓 = 𝑓 )
40		oveq2	⊢ ( 𝑛 = 𝑁 → ( 1 ..^ 𝑛 ) = ( 1 ..^ 𝑁 ) )
41		eqidd	⊢ ( 𝑛 = 𝑁 → 𝑃 = 𝑃 )
42	39 40 41	f1eq123d	⊢ ( 𝑛 = 𝑁 → ( 𝑓 : ( 1 ..^ 𝑛 ) –1-1→ 𝑃 ↔ 𝑓 : ( 1 ..^ 𝑁 ) –1-1→ 𝑃 ) )
43		oveq2	⊢ ( 𝑛 = 𝑁 → ( 2 ..^ 𝑛 ) = ( 2 ..^ 𝑁 ) )
44	43	raleqdv	⊢ ( 𝑛 = 𝑁 → ( ∀ 𝑗 ∈ ( 2 ..^ 𝑛 ) ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) ) ↔ ∀ 𝑗 ∈ ( 2 ..^ 𝑁 ) ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) ) ) )
45	44	anbi1d	⊢ ( 𝑛 = 𝑁 → ( ( ∀ 𝑗 ∈ ( 2 ..^ 𝑛 ) ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ↔ ( ∀ 𝑗 ∈ ( 2 ..^ 𝑁 ) ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) )
46	45	rexbidv	⊢ ( 𝑛 = 𝑁 → ( ∃ 𝑧 ∈ 𝑃 ( ∀ 𝑗 ∈ ( 2 ..^ 𝑛 ) ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ↔ ∃ 𝑧 ∈ 𝑃 ( ∀ 𝑗 ∈ ( 2 ..^ 𝑁 ) ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) )
47	46	2rexbidv	⊢ ( 𝑛 = 𝑁 → ( ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ∀ 𝑗 ∈ ( 2 ..^ 𝑛 ) ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ↔ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ∀ 𝑗 ∈ ( 2 ..^ 𝑁 ) ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) )
48	42 47	anbi12d	⊢ ( 𝑛 = 𝑁 → ( ( 𝑓 : ( 1 ..^ 𝑛 ) –1-1→ 𝑃 ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ∀ 𝑗 ∈ ( 2 ..^ 𝑛 ) ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) ↔ ( 𝑓 : ( 1 ..^ 𝑁 ) –1-1→ 𝑃 ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ∀ 𝑗 ∈ ( 2 ..^ 𝑁 ) ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) ) )
49	48	exbidv	⊢ ( 𝑛 = 𝑁 → ( ∃ 𝑓 ( 𝑓 : ( 1 ..^ 𝑛 ) –1-1→ 𝑃 ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ∀ 𝑗 ∈ ( 2 ..^ 𝑛 ) ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) ↔ ∃ 𝑓 ( 𝑓 : ( 1 ..^ 𝑁 ) –1-1→ 𝑃 ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ∀ 𝑗 ∈ ( 2 ..^ 𝑁 ) ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) ) )
50		df-trkgld	⊢ DimTarskiG≥ = { ⟨ 𝑔 , 𝑛 ⟩ ∣ [ ( Base ‘ 𝑔 ) / 𝑝 ] [ ( dist ‘ 𝑔 ) / 𝑑 ] [ ( Itv ‘ 𝑔 ) / 𝑖 ] ∃ 𝑓 ( 𝑓 : ( 1 ..^ 𝑛 ) –1-1→ 𝑝 ∧ ∃ 𝑥 ∈ 𝑝 ∃ 𝑦 ∈ 𝑝 ∃ 𝑧 ∈ 𝑝 ( ∀ 𝑗 ∈ ( 2 ..^ 𝑛 ) ( ( ( 𝑓 ‘ 1 ) 𝑑 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) 𝑑 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) 𝑑 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) ) ) }
51	38 49 50	brabg	⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝐺 DimTarskiG≥ 𝑁 ↔ ∃ 𝑓 ( 𝑓 : ( 1 ..^ 𝑁 ) –1-1→ 𝑃 ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ∀ 𝑗 ∈ ( 2 ..^ 𝑁 ) ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) ) )