Metamath Proof Explorer

Theorem axtglowdim2ALTV

Description: Alternate version of axtglowdim2 . (Contributed by Thierry Arnoux, 29-May-2019) (New usage is discouraged.)

Ref Expression
Hypotheses istrkg2d.p ⊢P=BaseG
istrkg2d.d ⊢-˙=dist⁡G
istrkg2d.i ⊢I=Itv⁡G
axtglowdim2ALTV.g ⊢φ→G∈𝒢Tarski2D
Assertion axtglowdim2ALTV ⊢φ→∃x∈P∃y∈P∃z∈P¬z∈xIy∨x∈zIy∨y∈xIz

Proof

Step Hyp Ref Expression
1 istrkg2d.p ⊢P=BaseG
2 istrkg2d.d ⊢-˙=dist⁡G
3 istrkg2d.i ⊢I=Itv⁡G
4 axtglowdim2ALTV.g ⊢φ→G∈𝒢Tarski2D
5 1 2 3 istrkg2d ⊢G∈𝒢Tarski2D↔G∈V∧∃x∈P∃y∈P∃z∈P¬z∈xIy∨x∈zIy∨y∈xIz∧∀x∈P∀y∈P∀z∈P∀u∈P∀v∈Px-˙u=x-˙v∧y-˙u=y-˙v∧z-˙u=z-˙v∧u≠v→z∈xIy∨x∈zIy∨y∈xIz
6 4 5 sylib ⊢φ→G∈V∧∃x∈P∃y∈P∃z∈P¬z∈xIy∨x∈zIy∨y∈xIz∧∀x∈P∀y∈P∀z∈P∀u∈P∀v∈Px-˙u=x-˙v∧y-˙u=y-˙v∧z-˙u=z-˙v∧u≠v→z∈xIy∨x∈zIy∨y∈xIz
7 6 simprd ⊢φ→∃x∈P∃y∈P∃z∈P¬z∈xIy∨x∈zIy∨y∈xIz∧∀x∈P∀y∈P∀z∈P∀u∈P∀v∈Px-˙u=x-˙v∧y-˙u=y-˙v∧z-˙u=z-˙v∧u≠v→z∈xIy∨x∈zIy∨y∈xIz
8 7 simpld ⊢φ→∃x∈P∃y∈P∃z∈P¬z∈xIy∨x∈zIy∨y∈xIz