Theorem axtglowdim2ALTV

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

	Ref	Expression
Hypotheses	istrkg2d.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
	istrkg2d.d	⊢ − = ( dist ‘ 𝐺 )
	istrkg2d.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	axtglowdim2ALTV.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG2D )
Assertion	axtglowdim2ALTV	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) )

Proof

Step	Hyp	Ref	Expression
1		istrkg2d.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		istrkg2d.d	⊢ − = ( dist ‘ 𝐺 )
3		istrkg2d.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
4		axtglowdim2ALTV.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG2D )
5	1 2 3	istrkg2d	⊢ ( 𝐺 ∈ TarskiG2D ↔ ( 𝐺 ∈ V ∧ ( ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( ( ( 𝑥 − 𝑢 ) = ( 𝑥 − 𝑣 ) ∧ ( 𝑦 − 𝑢 ) = ( 𝑦 − 𝑣 ) ∧ ( 𝑧 − 𝑢 ) = ( 𝑧 − 𝑣 ) ) ∧ 𝑢 ≠ 𝑣 ) → ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) ) )
6	4 5	sylib	⊢ ( 𝜑 → ( 𝐺 ∈ V ∧ ( ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( ( ( 𝑥 − 𝑢 ) = ( 𝑥 − 𝑣 ) ∧ ( 𝑦 − 𝑢 ) = ( 𝑦 − 𝑣 ) ∧ ( 𝑧 − 𝑢 ) = ( 𝑧 − 𝑣 ) ) ∧ 𝑢 ≠ 𝑣 ) → ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) ) )
7	6	simprd	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( ( ( 𝑥 − 𝑢 ) = ( 𝑥 − 𝑣 ) ∧ ( 𝑦 − 𝑢 ) = ( 𝑦 − 𝑣 ) ∧ ( 𝑧 − 𝑢 ) = ( 𝑧 − 𝑣 ) ) ∧ 𝑢 ≠ 𝑣 ) → ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) )
8	7	simpld	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) )