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	|- ( ph -> G e. TarskiG2D )
Assertion	axtglowdim2ALTV	|- ( ph -> E. x e. P E. y e. P E. z e. P -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( 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	|- ( ph -> G e. TarskiG2D )
5	1 2 3	istrkg2d	|- ( G e. TarskiG2D <-> ( G e. _V /\ ( E. x e. P E. y e. P E. z e. P -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) /\ A. x e. P A. y e. P A. z e. P A. u e. P A. v e. P ( ( ( ( x .- u ) = ( x .- v ) /\ ( y .- u ) = ( y .- v ) /\ ( z .- u ) = ( z .- v ) ) /\ u =/= v ) -> ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) ) )
6	4 5	sylib	|- ( ph -> ( G e. _V /\ ( E. x e. P E. y e. P E. z e. P -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) /\ A. x e. P A. y e. P A. z e. P A. u e. P A. v e. P ( ( ( ( x .- u ) = ( x .- v ) /\ ( y .- u ) = ( y .- v ) /\ ( z .- u ) = ( z .- v ) ) /\ u =/= v ) -> ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) ) )
7	6	simprd	|- ( ph -> ( E. x e. P E. y e. P E. z e. P -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) /\ A. x e. P A. y e. P A. z e. P A. u e. P A. v e. P ( ( ( ( x .- u ) = ( x .- v ) /\ ( y .- u ) = ( y .- v ) /\ ( z .- u ) = ( z .- v ) ) /\ u =/= v ) -> ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) )
8	7	simpld	|- ( ph -> E. x e. P E. y e. P E. z e. P -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) )