istrkgld - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > istrkgld		Structured version Visualization version GIF version

Theorem istrkgld 28694

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

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

**Assertion**
Ref	Expression
istrkgld	⊢ ((𝐺 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘2)) → (𝐺Dim_TarskiG≥𝑁 ↔ ∃𝑓(𝑓:(1..^𝑁)–1-1→𝑃 ∧ ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (∀𝑗 ∈ (2..^𝑁)(((𝑓‘1) − 𝑥) = ((𝑓‘𝑗) − 𝑥) ∧ ((𝑓‘1) − 𝑦) = ((𝑓‘𝑗) − 𝑦) ∧ ((𝑓‘1) − 𝑧) = ((𝑓‘𝑗) − 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))))))

Distinct variable groups: 𝑓,𝐺 𝑓,𝑗,𝑥,𝑦,𝑧,𝐼 𝑃,𝑓,𝑗,𝑥,𝑦,𝑧 − ,𝑓,𝑗,𝑥,𝑦,𝑧 𝑓,𝑁,𝑗,𝑥,𝑦,𝑧 Allowed substitution hints: 𝐺(𝑥,𝑦,𝑧,𝑗) 𝑉(𝑥,𝑦,𝑧,𝑓,𝑗)

Proof of Theorem istrkgld Dummy variables 𝑑 𝑔 𝑖 𝑛 𝑝 are mutually distinct and distinct from all other variables.

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

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 400 ∨ w3o 1100 ∧ w3a 1101 = wceq 1567 ∃wex 1806 ∈ wcel 2149 ∀wral 3085 ∃wrex 3095 [wsbc 3753 class class class wbr 5113 –1-1→wf1 6534 ‘cfv 6537 (class class class)co 7411 1c1 11101 2c2 12295 ℤ_≥cuz 12862 ..^cfzo 13682 Basecbs 17269 distcds 17319 Dim_TarskiG≥cstrkgld 28666 Itvcitv 28668

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-ext 2741 ax-sep 5261 ax-nul 5271 ax-pr 5405

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-sb 2098 df-clab 2748 df-cleq 2761 df-clel 2844 df-ne 2965 df-ral 3086 df-rex 3096 df-rab 3424 df-v 3465 df-sbc 3754 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-nul 4295 df-if 4493 df-sn 4595 df-pr 4597 df-op 4601 df-uni 4877 df-br 5114 df-opab 5178 df-rel 5669 df-cnv 5670 df-co 5671 df-dm 5672 df-rn 5673 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fv 6545 df-ov 7414 df-trkgld 28687

This theorem is referenced by: istrkg2ld 28695 istrkg3ld 28696

W3C validator