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

Theorem istrkgld 28218
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)) β†’ (𝐺DimTarskiGβ‰₯𝑁 ↔ βˆƒπ‘“(𝑓:(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.
StepHypRef Expression
1 istrkg.p . . 3 𝑃 = (Baseβ€˜πΊ)
2 istrkg.d . . 3 βˆ’ = (distβ€˜πΊ)
3 istrkg.i . . 3 𝐼 = (Itvβ€˜πΊ)
4 eqidd 2727 . . . . . 6 ((𝑝 = 𝑃 ∧ 𝑑 = βˆ’ ∧ 𝑖 = 𝐼) β†’ 𝑓 = 𝑓)
5 eqidd 2727 . . . . . 6 ((𝑝 = 𝑃 ∧ 𝑑 = βˆ’ ∧ 𝑖 = 𝐼) β†’ (1..^𝑛) = (1..^𝑛))
6 simp1 1133 . . . . . . 7 ((𝑝 = 𝑃 ∧ 𝑑 = βˆ’ ∧ 𝑖 = 𝐼) β†’ 𝑝 = 𝑃)
76eqcomd 2732 . . . . . 6 ((𝑝 = 𝑃 ∧ 𝑑 = βˆ’ ∧ 𝑖 = 𝐼) β†’ 𝑃 = 𝑝)
84, 5, 7f1eq123d 6819 . . . . 5 ((𝑝 = 𝑃 ∧ 𝑑 = βˆ’ ∧ 𝑖 = 𝐼) β†’ (𝑓:(1..^𝑛)–1-1→𝑃 ↔ 𝑓:(1..^𝑛)–1-1→𝑝))
9 simp2 1134 . . . . . . . . . . . . . 14 ((𝑝 = 𝑃 ∧ 𝑑 = βˆ’ ∧ 𝑖 = 𝐼) β†’ 𝑑 = βˆ’ )
109eqcomd 2732 . . . . . . . . . . . . 13 ((𝑝 = 𝑃 ∧ 𝑑 = βˆ’ ∧ 𝑖 = 𝐼) β†’ βˆ’ = 𝑑)
1110oveqd 7422 . . . . . . . . . . . 12 ((𝑝 = 𝑃 ∧ 𝑑 = βˆ’ ∧ 𝑖 = 𝐼) β†’ ((π‘“β€˜1) βˆ’ π‘₯) = ((π‘“β€˜1)𝑑π‘₯))
1210oveqd 7422 . . . . . . . . . . . 12 ((𝑝 = 𝑃 ∧ 𝑑 = βˆ’ ∧ 𝑖 = 𝐼) β†’ ((π‘“β€˜π‘—) βˆ’ π‘₯) = ((π‘“β€˜π‘—)𝑑π‘₯))
1311, 12eqeq12d 2742 . . . . . . . . . . 11 ((𝑝 = 𝑃 ∧ 𝑑 = βˆ’ ∧ 𝑖 = 𝐼) β†’ (((π‘“β€˜1) βˆ’ π‘₯) = ((π‘“β€˜π‘—) βˆ’ π‘₯) ↔ ((π‘“β€˜1)𝑑π‘₯) = ((π‘“β€˜π‘—)𝑑π‘₯)))
1410oveqd 7422 . . . . . . . . . . . 12 ((𝑝 = 𝑃 ∧ 𝑑 = βˆ’ ∧ 𝑖 = 𝐼) β†’ ((π‘“β€˜1) βˆ’ 𝑦) = ((π‘“β€˜1)𝑑𝑦))
1510oveqd 7422 . . . . . . . . . . . 12 ((𝑝 = 𝑃 ∧ 𝑑 = βˆ’ ∧ 𝑖 = 𝐼) β†’ ((π‘“β€˜π‘—) βˆ’ 𝑦) = ((π‘“β€˜π‘—)𝑑𝑦))
1614, 15eqeq12d 2742 . . . . . . . . . . 11 ((𝑝 = 𝑃 ∧ 𝑑 = βˆ’ ∧ 𝑖 = 𝐼) β†’ (((π‘“β€˜1) βˆ’ 𝑦) = ((π‘“β€˜π‘—) βˆ’ 𝑦) ↔ ((π‘“β€˜1)𝑑𝑦) = ((π‘“β€˜π‘—)𝑑𝑦)))
1710oveqd 7422 . . . . . . . . . . . 12 ((𝑝 = 𝑃 ∧ 𝑑 = βˆ’ ∧ 𝑖 = 𝐼) β†’ ((π‘“β€˜1) βˆ’ 𝑧) = ((π‘“β€˜1)𝑑𝑧))
1810oveqd 7422 . . . . . . . . . . . 12 ((𝑝 = 𝑃 ∧ 𝑑 = βˆ’ ∧ 𝑖 = 𝐼) β†’ ((π‘“β€˜π‘—) βˆ’ 𝑧) = ((π‘“β€˜π‘—)𝑑𝑧))
1917, 18eqeq12d 2742 . . . . . . . . . . 11 ((𝑝 = 𝑃 ∧ 𝑑 = βˆ’ ∧ 𝑖 = 𝐼) β†’ (((π‘“β€˜1) βˆ’ 𝑧) = ((π‘“β€˜π‘—) βˆ’ 𝑧) ↔ ((π‘“β€˜1)𝑑𝑧) = ((π‘“β€˜π‘—)𝑑𝑧)))
2013, 16, 193anbi123d 1432 . . . . . . . . . 10 ((𝑝 = 𝑃 ∧ 𝑑 = βˆ’ ∧ 𝑖 = 𝐼) β†’ ((((π‘“β€˜1) βˆ’ π‘₯) = ((π‘“β€˜π‘—) βˆ’ π‘₯) ∧ ((π‘“β€˜1) βˆ’ 𝑦) = ((π‘“β€˜π‘—) βˆ’ 𝑦) ∧ ((π‘“β€˜1) βˆ’ 𝑧) = ((π‘“β€˜π‘—) βˆ’ 𝑧)) ↔ (((π‘“β€˜1)𝑑π‘₯) = ((π‘“β€˜π‘—)𝑑π‘₯) ∧ ((π‘“β€˜1)𝑑𝑦) = ((π‘“β€˜π‘—)𝑑𝑦) ∧ ((π‘“β€˜1)𝑑𝑧) = ((π‘“β€˜π‘—)𝑑𝑧))))
2120ralbidv 3171 . . . . . . . . 9 ((𝑝 = 𝑃 ∧ 𝑑 = βˆ’ ∧ 𝑖 = 𝐼) β†’ (βˆ€π‘— ∈ (2..^𝑛)(((π‘“β€˜1) βˆ’ π‘₯) = ((π‘“β€˜π‘—) βˆ’ π‘₯) ∧ ((π‘“β€˜1) βˆ’ 𝑦) = ((π‘“β€˜π‘—) βˆ’ 𝑦) ∧ ((π‘“β€˜1) βˆ’ 𝑧) = ((π‘“β€˜π‘—) βˆ’ 𝑧)) ↔ βˆ€π‘— ∈ (2..^𝑛)(((π‘“β€˜1)𝑑π‘₯) = ((π‘“β€˜π‘—)𝑑π‘₯) ∧ ((π‘“β€˜1)𝑑𝑦) = ((π‘“β€˜π‘—)𝑑𝑦) ∧ ((π‘“β€˜1)𝑑𝑧) = ((π‘“β€˜π‘—)𝑑𝑧))))
22 simp3 1135 . . . . . . . . . . . . . 14 ((𝑝 = 𝑃 ∧ 𝑑 = βˆ’ ∧ 𝑖 = 𝐼) β†’ 𝑖 = 𝐼)
2322eqcomd 2732 . . . . . . . . . . . . 13 ((𝑝 = 𝑃 ∧ 𝑑 = βˆ’ ∧ 𝑖 = 𝐼) β†’ 𝐼 = 𝑖)
2423oveqd 7422 . . . . . . . . . . . 12 ((𝑝 = 𝑃 ∧ 𝑑 = βˆ’ ∧ 𝑖 = 𝐼) β†’ (π‘₯𝐼𝑦) = (π‘₯𝑖𝑦))
2524eleq2d 2813 . . . . . . . . . . 11 ((𝑝 = 𝑃 ∧ 𝑑 = βˆ’ ∧ 𝑖 = 𝐼) β†’ (𝑧 ∈ (π‘₯𝐼𝑦) ↔ 𝑧 ∈ (π‘₯𝑖𝑦)))
2623oveqd 7422 . . . . . . . . . . . 12 ((𝑝 = 𝑃 ∧ 𝑑 = βˆ’ ∧ 𝑖 = 𝐼) β†’ (𝑧𝐼𝑦) = (𝑧𝑖𝑦))
2726eleq2d 2813 . . . . . . . . . . 11 ((𝑝 = 𝑃 ∧ 𝑑 = βˆ’ ∧ 𝑖 = 𝐼) β†’ (π‘₯ ∈ (𝑧𝐼𝑦) ↔ π‘₯ ∈ (𝑧𝑖𝑦)))
2823oveqd 7422 . . . . . . . . . . . 12 ((𝑝 = 𝑃 ∧ 𝑑 = βˆ’ ∧ 𝑖 = 𝐼) β†’ (π‘₯𝐼𝑧) = (π‘₯𝑖𝑧))
2928eleq2d 2813 . . . . . . . . . . 11 ((𝑝 = 𝑃 ∧ 𝑑 = βˆ’ ∧ 𝑖 = 𝐼) β†’ (𝑦 ∈ (π‘₯𝐼𝑧) ↔ 𝑦 ∈ (π‘₯𝑖𝑧)))
3025, 27, 293orbi123d 1431 . . . . . . . . . 10 ((𝑝 = 𝑃 ∧ 𝑑 = βˆ’ ∧ 𝑖 = 𝐼) β†’ ((𝑧 ∈ (π‘₯𝐼𝑦) ∨ π‘₯ ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (π‘₯𝐼𝑧)) ↔ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧))))
3130notbid 318 . . . . . . . . 9 ((𝑝 = 𝑃 ∧ 𝑑 = βˆ’ ∧ 𝑖 = 𝐼) β†’ (Β¬ (𝑧 ∈ (π‘₯𝐼𝑦) ∨ π‘₯ ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (π‘₯𝐼𝑧)) ↔ Β¬ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧))))
3221, 31anbi12d 630 . . . . . . . 8 ((𝑝 = 𝑃 ∧ 𝑑 = βˆ’ ∧ 𝑖 = 𝐼) β†’ ((βˆ€π‘— ∈ (2..^𝑛)(((π‘“β€˜1) βˆ’ π‘₯) = ((π‘“β€˜π‘—) βˆ’ π‘₯) ∧ ((π‘“β€˜1) βˆ’ 𝑦) = ((π‘“β€˜π‘—) βˆ’ 𝑦) ∧ ((π‘“β€˜1) βˆ’ 𝑧) = ((π‘“β€˜π‘—) βˆ’ 𝑧)) ∧ Β¬ (𝑧 ∈ (π‘₯𝐼𝑦) ∨ π‘₯ ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (π‘₯𝐼𝑧))) ↔ (βˆ€π‘— ∈ (2..^𝑛)(((π‘“β€˜1)𝑑π‘₯) = ((π‘“β€˜π‘—)𝑑π‘₯) ∧ ((π‘“β€˜1)𝑑𝑦) = ((π‘“β€˜π‘—)𝑑𝑦) ∧ ((π‘“β€˜1)𝑑𝑧) = ((π‘“β€˜π‘—)𝑑𝑧)) ∧ Β¬ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧)))))
337, 32rexeqbidv 3337 . . . . . . 7 ((𝑝 = 𝑃 ∧ 𝑑 = βˆ’ ∧ 𝑖 = 𝐼) β†’ (βˆƒπ‘§ ∈ 𝑃 (βˆ€π‘— ∈ (2..^𝑛)(((π‘“β€˜1) βˆ’ π‘₯) = ((π‘“β€˜π‘—) βˆ’ π‘₯) ∧ ((π‘“β€˜1) βˆ’ 𝑦) = ((π‘“β€˜π‘—) βˆ’ 𝑦) ∧ ((π‘“β€˜1) βˆ’ 𝑧) = ((π‘“β€˜π‘—) βˆ’ 𝑧)) ∧ Β¬ (𝑧 ∈ (π‘₯𝐼𝑦) ∨ π‘₯ ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (π‘₯𝐼𝑧))) ↔ βˆƒπ‘§ ∈ 𝑝 (βˆ€π‘— ∈ (2..^𝑛)(((π‘“β€˜1)𝑑π‘₯) = ((π‘“β€˜π‘—)𝑑π‘₯) ∧ ((π‘“β€˜1)𝑑𝑦) = ((π‘“β€˜π‘—)𝑑𝑦) ∧ ((π‘“β€˜1)𝑑𝑧) = ((π‘“β€˜π‘—)𝑑𝑧)) ∧ Β¬ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧)))))
347, 33rexeqbidv 3337 . . . . . 6 ((𝑝 = 𝑃 ∧ 𝑑 = βˆ’ ∧ 𝑖 = 𝐼) β†’ (βˆƒπ‘¦ ∈ 𝑃 βˆƒπ‘§ ∈ 𝑃 (βˆ€π‘— ∈ (2..^𝑛)(((π‘“β€˜1) βˆ’ π‘₯) = ((π‘“β€˜π‘—) βˆ’ π‘₯) ∧ ((π‘“β€˜1) βˆ’ 𝑦) = ((π‘“β€˜π‘—) βˆ’ 𝑦) ∧ ((π‘“β€˜1) βˆ’ 𝑧) = ((π‘“β€˜π‘—) βˆ’ 𝑧)) ∧ Β¬ (𝑧 ∈ (π‘₯𝐼𝑦) ∨ π‘₯ ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (π‘₯𝐼𝑧))) ↔ βˆƒπ‘¦ ∈ 𝑝 βˆƒπ‘§ ∈ 𝑝 (βˆ€π‘— ∈ (2..^𝑛)(((π‘“β€˜1)𝑑π‘₯) = ((π‘“β€˜π‘—)𝑑π‘₯) ∧ ((π‘“β€˜1)𝑑𝑦) = ((π‘“β€˜π‘—)𝑑𝑦) ∧ ((π‘“β€˜1)𝑑𝑧) = ((π‘“β€˜π‘—)𝑑𝑧)) ∧ Β¬ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧)))))
357, 34rexeqbidv 3337 . . . . 5 ((𝑝 = 𝑃 ∧ 𝑑 = βˆ’ ∧ 𝑖 = 𝐼) β†’ (βˆƒπ‘₯ ∈ 𝑃 βˆƒπ‘¦ ∈ 𝑃 βˆƒπ‘§ ∈ 𝑃 (βˆ€π‘— ∈ (2..^𝑛)(((π‘“β€˜1) βˆ’ π‘₯) = ((π‘“β€˜π‘—) βˆ’ π‘₯) ∧ ((π‘“β€˜1) βˆ’ 𝑦) = ((π‘“β€˜π‘—) βˆ’ 𝑦) ∧ ((π‘“β€˜1) βˆ’ 𝑧) = ((π‘“β€˜π‘—) βˆ’ 𝑧)) ∧ Β¬ (𝑧 ∈ (π‘₯𝐼𝑦) ∨ π‘₯ ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (π‘₯𝐼𝑧))) ↔ βˆƒπ‘₯ ∈ 𝑝 βˆƒπ‘¦ ∈ 𝑝 βˆƒπ‘§ ∈ 𝑝 (βˆ€π‘— ∈ (2..^𝑛)(((π‘“β€˜1)𝑑π‘₯) = ((π‘“β€˜π‘—)𝑑π‘₯) ∧ ((π‘“β€˜1)𝑑𝑦) = ((π‘“β€˜π‘—)𝑑𝑦) ∧ ((π‘“β€˜1)𝑑𝑧) = ((π‘“β€˜π‘—)𝑑𝑧)) ∧ Β¬ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧)))))
368, 35anbi12d 630 . . . 4 ((𝑝 = 𝑃 ∧ 𝑑 = βˆ’ ∧ 𝑖 = 𝐼) β†’ ((𝑓:(1..^𝑛)–1-1→𝑃 ∧ βˆƒπ‘₯ ∈ 𝑃 βˆƒπ‘¦ ∈ 𝑃 βˆƒπ‘§ ∈ 𝑃 (βˆ€π‘— ∈ (2..^𝑛)(((π‘“β€˜1) βˆ’ π‘₯) = ((π‘“β€˜π‘—) βˆ’ π‘₯) ∧ ((π‘“β€˜1) βˆ’ 𝑦) = ((π‘“β€˜π‘—) βˆ’ 𝑦) ∧ ((π‘“β€˜1) βˆ’ 𝑧) = ((π‘“β€˜π‘—) βˆ’ 𝑧)) ∧ Β¬ (𝑧 ∈ (π‘₯𝐼𝑦) ∨ π‘₯ ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (π‘₯𝐼𝑧)))) ↔ (𝑓:(1..^𝑛)–1-1→𝑝 ∧ βˆƒπ‘₯ ∈ 𝑝 βˆƒπ‘¦ ∈ 𝑝 βˆƒπ‘§ ∈ 𝑝 (βˆ€π‘— ∈ (2..^𝑛)(((π‘“β€˜1)𝑑π‘₯) = ((π‘“β€˜π‘—)𝑑π‘₯) ∧ ((π‘“β€˜1)𝑑𝑦) = ((π‘“β€˜π‘—)𝑑𝑦) ∧ ((π‘“β€˜1)𝑑𝑧) = ((π‘“β€˜π‘—)𝑑𝑧)) ∧ Β¬ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧))))))
3736exbidv 1916 . . 3 ((𝑝 = 𝑃 ∧ 𝑑 = βˆ’ ∧ 𝑖 = 𝐼) β†’ (βˆƒπ‘“(𝑓:(1..^𝑛)–1-1→𝑃 ∧ βˆƒπ‘₯ ∈ 𝑃 βˆƒπ‘¦ ∈ 𝑃 βˆƒπ‘§ ∈ 𝑃 (βˆ€π‘— ∈ (2..^𝑛)(((π‘“β€˜1) βˆ’ π‘₯) = ((π‘“β€˜π‘—) βˆ’ π‘₯) ∧ ((π‘“β€˜1) βˆ’ 𝑦) = ((π‘“β€˜π‘—) βˆ’ 𝑦) ∧ ((π‘“β€˜1) βˆ’ 𝑧) = ((π‘“β€˜π‘—) βˆ’ 𝑧)) ∧ Β¬ (𝑧 ∈ (π‘₯𝐼𝑦) ∨ π‘₯ ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (π‘₯𝐼𝑧)))) ↔ βˆƒπ‘“(𝑓:(1..^𝑛)–1-1→𝑝 ∧ βˆƒπ‘₯ ∈ 𝑝 βˆƒπ‘¦ ∈ 𝑝 βˆƒπ‘§ ∈ 𝑝 (βˆ€π‘— ∈ (2..^𝑛)(((π‘“β€˜1)𝑑π‘₯) = ((π‘“β€˜π‘—)𝑑π‘₯) ∧ ((π‘“β€˜1)𝑑𝑦) = ((π‘“β€˜π‘—)𝑑𝑦) ∧ ((π‘“β€˜1)𝑑𝑧) = ((π‘“β€˜π‘—)𝑑𝑧)) ∧ Β¬ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧))))))
381, 2, 3, 37sbcie3s 17104 . 2 (𝑔 = 𝐺 β†’ ([(Baseβ€˜π‘”) / 𝑝][(distβ€˜π‘”) / 𝑑][(Itvβ€˜π‘”) / 𝑖]βˆƒπ‘“(𝑓:(1..^𝑛)–1-1→𝑝 ∧ βˆƒπ‘₯ ∈ 𝑝 βˆƒπ‘¦ ∈ 𝑝 βˆƒπ‘§ ∈ 𝑝 (βˆ€π‘— ∈ (2..^𝑛)(((π‘“β€˜1)𝑑π‘₯) = ((π‘“β€˜π‘—)𝑑π‘₯) ∧ ((π‘“β€˜1)𝑑𝑦) = ((π‘“β€˜π‘—)𝑑𝑦) ∧ ((π‘“β€˜1)𝑑𝑧) = ((π‘“β€˜π‘—)𝑑𝑧)) ∧ Β¬ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧)))) ↔ βˆƒπ‘“(𝑓:(1..^𝑛)–1-1→𝑃 ∧ βˆƒπ‘₯ ∈ 𝑃 βˆƒπ‘¦ ∈ 𝑃 βˆƒπ‘§ ∈ 𝑃 (βˆ€π‘— ∈ (2..^𝑛)(((π‘“β€˜1) βˆ’ π‘₯) = ((π‘“β€˜π‘—) βˆ’ π‘₯) ∧ ((π‘“β€˜1) βˆ’ 𝑦) = ((π‘“β€˜π‘—) βˆ’ 𝑦) ∧ ((π‘“β€˜1) βˆ’ 𝑧) = ((π‘“β€˜π‘—) βˆ’ 𝑧)) ∧ Β¬ (𝑧 ∈ (π‘₯𝐼𝑦) ∨ π‘₯ ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (π‘₯𝐼𝑧))))))
39 eqidd 2727 . . . . 5 (𝑛 = 𝑁 β†’ 𝑓 = 𝑓)
40 oveq2 7413 . . . . 5 (𝑛 = 𝑁 β†’ (1..^𝑛) = (1..^𝑁))
41 eqidd 2727 . . . . 5 (𝑛 = 𝑁 β†’ 𝑃 = 𝑃)
4239, 40, 41f1eq123d 6819 . . . 4 (𝑛 = 𝑁 β†’ (𝑓:(1..^𝑛)–1-1→𝑃 ↔ 𝑓:(1..^𝑁)–1-1→𝑃))
43 oveq2 7413 . . . . . . . 8 (𝑛 = 𝑁 β†’ (2..^𝑛) = (2..^𝑁))
4443raleqdv 3319 . . . . . . 7 (𝑛 = 𝑁 β†’ (βˆ€π‘— ∈ (2..^𝑛)(((π‘“β€˜1) βˆ’ π‘₯) = ((π‘“β€˜π‘—) βˆ’ π‘₯) ∧ ((π‘“β€˜1) βˆ’ 𝑦) = ((π‘“β€˜π‘—) βˆ’ 𝑦) ∧ ((π‘“β€˜1) βˆ’ 𝑧) = ((π‘“β€˜π‘—) βˆ’ 𝑧)) ↔ βˆ€π‘— ∈ (2..^𝑁)(((π‘“β€˜1) βˆ’ π‘₯) = ((π‘“β€˜π‘—) βˆ’ π‘₯) ∧ ((π‘“β€˜1) βˆ’ 𝑦) = ((π‘“β€˜π‘—) βˆ’ 𝑦) ∧ ((π‘“β€˜1) βˆ’ 𝑧) = ((π‘“β€˜π‘—) βˆ’ 𝑧))))
4544anbi1d 629 . . . . . 6 (𝑛 = 𝑁 β†’ ((βˆ€π‘— ∈ (2..^𝑛)(((π‘“β€˜1) βˆ’ π‘₯) = ((π‘“β€˜π‘—) βˆ’ π‘₯) ∧ ((π‘“β€˜1) βˆ’ 𝑦) = ((π‘“β€˜π‘—) βˆ’ 𝑦) ∧ ((π‘“β€˜1) βˆ’ 𝑧) = ((π‘“β€˜π‘—) βˆ’ 𝑧)) ∧ Β¬ (𝑧 ∈ (π‘₯𝐼𝑦) ∨ π‘₯ ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (π‘₯𝐼𝑧))) ↔ (βˆ€π‘— ∈ (2..^𝑁)(((π‘“β€˜1) βˆ’ π‘₯) = ((π‘“β€˜π‘—) βˆ’ π‘₯) ∧ ((π‘“β€˜1) βˆ’ 𝑦) = ((π‘“β€˜π‘—) βˆ’ 𝑦) ∧ ((π‘“β€˜1) βˆ’ 𝑧) = ((π‘“β€˜π‘—) βˆ’ 𝑧)) ∧ Β¬ (𝑧 ∈ (π‘₯𝐼𝑦) ∨ π‘₯ ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (π‘₯𝐼𝑧)))))
4645rexbidv 3172 . . . . 5 (𝑛 = 𝑁 β†’ (βˆƒπ‘§ ∈ 𝑃 (βˆ€π‘— ∈ (2..^𝑛)(((π‘“β€˜1) βˆ’ π‘₯) = ((π‘“β€˜π‘—) βˆ’ π‘₯) ∧ ((π‘“β€˜1) βˆ’ 𝑦) = ((π‘“β€˜π‘—) βˆ’ 𝑦) ∧ ((π‘“β€˜1) βˆ’ 𝑧) = ((π‘“β€˜π‘—) βˆ’ 𝑧)) ∧ Β¬ (𝑧 ∈ (π‘₯𝐼𝑦) ∨ π‘₯ ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (π‘₯𝐼𝑧))) ↔ βˆƒπ‘§ ∈ 𝑃 (βˆ€π‘— ∈ (2..^𝑁)(((π‘“β€˜1) βˆ’ π‘₯) = ((π‘“β€˜π‘—) βˆ’ π‘₯) ∧ ((π‘“β€˜1) βˆ’ 𝑦) = ((π‘“β€˜π‘—) βˆ’ 𝑦) ∧ ((π‘“β€˜1) βˆ’ 𝑧) = ((π‘“β€˜π‘—) βˆ’ 𝑧)) ∧ Β¬ (𝑧 ∈ (π‘₯𝐼𝑦) ∨ π‘₯ ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (π‘₯𝐼𝑧)))))
47462rexbidv 3213 . . . 4 (𝑛 = 𝑁 β†’ (βˆƒπ‘₯ ∈ 𝑃 βˆƒπ‘¦ ∈ 𝑃 βˆƒπ‘§ ∈ 𝑃 (βˆ€π‘— ∈ (2..^𝑛)(((π‘“β€˜1) βˆ’ π‘₯) = ((π‘“β€˜π‘—) βˆ’ π‘₯) ∧ ((π‘“β€˜1) βˆ’ 𝑦) = ((π‘“β€˜π‘—) βˆ’ 𝑦) ∧ ((π‘“β€˜1) βˆ’ 𝑧) = ((π‘“β€˜π‘—) βˆ’ 𝑧)) ∧ Β¬ (𝑧 ∈ (π‘₯𝐼𝑦) ∨ π‘₯ ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (π‘₯𝐼𝑧))) ↔ βˆƒπ‘₯ ∈ 𝑃 βˆƒπ‘¦ ∈ 𝑃 βˆƒπ‘§ ∈ 𝑃 (βˆ€π‘— ∈ (2..^𝑁)(((π‘“β€˜1) βˆ’ π‘₯) = ((π‘“β€˜π‘—) βˆ’ π‘₯) ∧ ((π‘“β€˜1) βˆ’ 𝑦) = ((π‘“β€˜π‘—) βˆ’ 𝑦) ∧ ((π‘“β€˜1) βˆ’ 𝑧) = ((π‘“β€˜π‘—) βˆ’ 𝑧)) ∧ Β¬ (𝑧 ∈ (π‘₯𝐼𝑦) ∨ π‘₯ ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (π‘₯𝐼𝑧)))))
4842, 47anbi12d 630 . . 3 (𝑛 = 𝑁 β†’ ((𝑓:(1..^𝑛)–1-1→𝑃 ∧ βˆƒπ‘₯ ∈ 𝑃 βˆƒπ‘¦ ∈ 𝑃 βˆƒπ‘§ ∈ 𝑃 (βˆ€π‘— ∈ (2..^𝑛)(((π‘“β€˜1) βˆ’ π‘₯) = ((π‘“β€˜π‘—) βˆ’ π‘₯) ∧ ((π‘“β€˜1) βˆ’ 𝑦) = ((π‘“β€˜π‘—) βˆ’ 𝑦) ∧ ((π‘“β€˜1) βˆ’ 𝑧) = ((π‘“β€˜π‘—) βˆ’ 𝑧)) ∧ Β¬ (𝑧 ∈ (π‘₯𝐼𝑦) ∨ π‘₯ ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (π‘₯𝐼𝑧)))) ↔ (𝑓:(1..^𝑁)–1-1→𝑃 ∧ βˆƒπ‘₯ ∈ 𝑃 βˆƒπ‘¦ ∈ 𝑃 βˆƒπ‘§ ∈ 𝑃 (βˆ€π‘— ∈ (2..^𝑁)(((π‘“β€˜1) βˆ’ π‘₯) = ((π‘“β€˜π‘—) βˆ’ π‘₯) ∧ ((π‘“β€˜1) βˆ’ 𝑦) = ((π‘“β€˜π‘—) βˆ’ 𝑦) ∧ ((π‘“β€˜1) βˆ’ 𝑧) = ((π‘“β€˜π‘—) βˆ’ 𝑧)) ∧ Β¬ (𝑧 ∈ (π‘₯𝐼𝑦) ∨ π‘₯ ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (π‘₯𝐼𝑧))))))
4948exbidv 1916 . 2 (𝑛 = 𝑁 β†’ (βˆƒπ‘“(𝑓:(1..^𝑛)–1-1→𝑃 ∧ βˆƒπ‘₯ ∈ 𝑃 βˆƒπ‘¦ ∈ 𝑃 βˆƒπ‘§ ∈ 𝑃 (βˆ€π‘— ∈ (2..^𝑛)(((π‘“β€˜1) βˆ’ π‘₯) = ((π‘“β€˜π‘—) βˆ’ π‘₯) ∧ ((π‘“β€˜1) βˆ’ 𝑦) = ((π‘“β€˜π‘—) βˆ’ 𝑦) ∧ ((π‘“β€˜1) βˆ’ 𝑧) = ((π‘“β€˜π‘—) βˆ’ 𝑧)) ∧ Β¬ (𝑧 ∈ (π‘₯𝐼𝑦) ∨ π‘₯ ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (π‘₯𝐼𝑧)))) ↔ βˆƒπ‘“(𝑓:(1..^𝑁)–1-1→𝑃 ∧ βˆƒπ‘₯ ∈ 𝑃 βˆƒπ‘¦ ∈ 𝑃 βˆƒπ‘§ ∈ 𝑃 (βˆ€π‘— ∈ (2..^𝑁)(((π‘“β€˜1) βˆ’ π‘₯) = ((π‘“β€˜π‘—) βˆ’ π‘₯) ∧ ((π‘“β€˜1) βˆ’ 𝑦) = ((π‘“β€˜π‘—) βˆ’ 𝑦) ∧ ((π‘“β€˜1) βˆ’ 𝑧) = ((π‘“β€˜π‘—) βˆ’ 𝑧)) ∧ Β¬ (𝑧 ∈ (π‘₯𝐼𝑦) ∨ π‘₯ ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (π‘₯𝐼𝑧))))))
50 df-trkgld 28211 . 2 DimTarskiGβ‰₯ = {βŸ¨π‘”, π‘›βŸ© ∣ [(Baseβ€˜π‘”) / 𝑝][(distβ€˜π‘”) / 𝑑][(Itvβ€˜π‘”) / 𝑖]βˆƒπ‘“(𝑓:(1..^𝑛)–1-1→𝑝 ∧ βˆƒπ‘₯ ∈ 𝑝 βˆƒπ‘¦ ∈ 𝑝 βˆƒπ‘§ ∈ 𝑝 (βˆ€π‘— ∈ (2..^𝑛)(((π‘“β€˜1)𝑑π‘₯) = ((π‘“β€˜π‘—)𝑑π‘₯) ∧ ((π‘“β€˜1)𝑑𝑦) = ((π‘“β€˜π‘—)𝑑𝑦) ∧ ((π‘“β€˜1)𝑑𝑧) = ((π‘“β€˜π‘—)𝑑𝑧)) ∧ Β¬ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧))))}
5138, 49, 50brabg 5532 1 ((𝐺 ∈ 𝑉 ∧ 𝑁 ∈ (β„€β‰₯β€˜2)) β†’ (𝐺DimTarskiGβ‰₯𝑁 ↔ βˆƒπ‘“(𝑓:(1..^𝑁)–1-1→𝑃 ∧ βˆƒπ‘₯ ∈ 𝑃 βˆƒπ‘¦ ∈ 𝑃 βˆƒπ‘§ ∈ 𝑃 (βˆ€π‘— ∈ (2..^𝑁)(((π‘“β€˜1) βˆ’ π‘₯) = ((π‘“β€˜π‘—) βˆ’ π‘₯) ∧ ((π‘“β€˜1) βˆ’ 𝑦) = ((π‘“β€˜π‘—) βˆ’ 𝑦) ∧ ((π‘“β€˜1) βˆ’ 𝑧) = ((π‘“β€˜π‘—) βˆ’ 𝑧)) ∧ Β¬ (𝑧 ∈ (π‘₯𝐼𝑦) ∨ π‘₯ ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (π‘₯𝐼𝑧))))))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 395   ∨ w3o 1083   ∧ w3a 1084   = wceq 1533  βˆƒwex 1773   ∈ wcel 2098  βˆ€wral 3055  βˆƒwrex 3064  [wsbc 3772   class class class wbr 5141  β€“1-1β†’wf1 6534  β€˜cfv 6537  (class class class)co 7405  1c1 11113  2c2 12271  β„€β‰₯cuz 12826  ..^cfzo 13633  Basecbs 17153  distcds 17215  DimTarskiGβ‰₯cstrkgld 28190  Itvcitv 28192
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2697  ax-sep 5292  ax-nul 5299  ax-pr 5420
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2704  df-cleq 2718  df-clel 2804  df-ne 2935  df-ral 3056  df-rex 3065  df-rab 3427  df-v 3470  df-sbc 3773  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-nul 4318  df-if 4524  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-br 5142  df-opab 5204  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-iota 6489  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fv 6545  df-ov 7408  df-trkgld 28211
This theorem is referenced by:  istrkg2ld  28219  istrkg3ld  28220
  Copyright terms: Public domain W3C validator