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 = Base G
istrkg2d.d ⊢ - ˙ = dist ⁡ G
istrkg2d.i ⊢ I = Itv ⁡ G
axtglowdim2ALTV.g ⊢ φ → G ∈ 𝒢 Tarski 2D
Assertion axtglowdim2ALTV ⊢ φ → ∃ x ∈ P ∃ y ∈ P ∃ z ∈ P ¬ z ∈ x I y ∨ x ∈ z I y ∨ y ∈ x I z

Proof

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