Theorem axtgupdim2OLD 30746

Description: Upper dimension axiom for dimension 2, Axiom A9 of [Schwabhauser] p. 13. (Contributed by Thierry Arnoux, 29-May-2019.) (New usage is discouraged.) (Proof modification is discouraged.)

Hypotheses

Ref	Expression
istrkg2d.p	|- P = ( Base ` G )
istrkg2d.d	|- .- = ( dist ` G )
istrkg2d.i	|- I = (Itv ` G )
axtgupdim2OLD.x	|- ( ph -> X e. P )
axtgupdim2OLD.y	|- ( ph -> Y e. P )
axtgupdim2OLD.z	|- ( ph -> Z e. P )
axtgupdim2OLD.u	|- ( ph -> U e. P )
axtgupdim2OLD.v	|- ( ph -> V e. P )
axtgupdim2OLD.0	|- ( ph -> U =/= V )
axtgupdim2OLD.1	|- ( ph -> ( X .- U ) = ( X .- V ) )
axtgupdim2OLD.2	|- ( ph -> ( Y .- U ) = ( Y .- V ) )
axtgupdim2OLD.3	|- ( ph -> ( Z .- U ) = ( Z .- V ) )
axtgupdim2OLD.g	|- ( ph -> G e. TarskiG2D )

Assertion

Ref	Expression
axtgupdim2OLD	|- ( ph -> ( Z e. ( X I Y ) \/ X e. ( Z I Y ) \/ Y e. ( X I Z ) ) )

Proof of Theorem axtgupdim2OLD

Dummy variables u v x y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		axtgupdim2OLD.1	. . 3 |- ( ph -> ( X .- U ) = ( X .- V ) )
2		axtgupdim2OLD.2	. . 3 |- ( ph -> ( Y .- U ) = ( Y .- V ) )
3		axtgupdim2OLD.3	. . 3 |- ( ph -> ( Z .- U ) = ( Z .- V ) )
4	1, 2, 3	3jca 1242	. 2 |- ( ph -> ( ( X .- U ) = ( X .- V ) /\ ( Y .- U ) = ( Y .- V ) /\ ( Z .- U ) = ( Z .- V ) ) )
5		axtgupdim2OLD.0	. 2 |- ( ph -> U =/= V )
6		axtgupdim2OLD.g	. . . . . 6 |- ( ph -> G e. TarskiG2D )
7		istrkg2d.p	. . . . . . 7 |- P = ( Base ` G )
8		istrkg2d.d	. . . . . . 7 |- .- = ( dist ` G )
9		istrkg2d.i	. . . . . . 7 |- I = (Itv ` G )
10	7, 8, 9	istrkg2d 30744	. . . . . 6 |- ( 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 ) ) ) ) ) )
11	6, 10	sylib 208	. . . . 5 |- ( 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 ) ) ) ) ) )
12	11	simprrd 797	. . . 4 |- ( ph -> 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 ) ) ) )
13		axtgupdim2OLD.x	. . . . 5 |- ( ph -> X e. P )
14		axtgupdim2OLD.y	. . . . 5 |- ( ph -> Y e. P )
15		axtgupdim2OLD.z	. . . . 5 |- ( ph -> Z e. P )
16		oveq1 6657	. . . . . . . . . . 11 |- ( x = X -> ( x .- u ) = ( X .- u ) )
17		oveq1 6657	. . . . . . . . . . 11 |- ( x = X -> ( x .- v ) = ( X .- v ) )
18	16, 17	eqeq12d 2637	. . . . . . . . . 10 |- ( x = X -> ( ( x .- u ) = ( x .- v ) <-> ( X .- u ) = ( X .- v ) ) )
19	18	3anbi1d 1403	. . . . . . . . 9 |- ( x = X -> ( ( ( x .- u ) = ( x .- v ) /\ ( y .- u ) = ( y .- v ) /\ ( z .- u ) = ( z .- v ) ) <-> ( ( X .- u ) = ( X .- v ) /\ ( y .- u ) = ( y .- v ) /\ ( z .- u ) = ( z .- v ) ) ) )
20	19	anbi1d 741	. . . . . . . 8 |- ( x = X -> ( ( ( ( x .- u ) = ( x .- v ) /\ ( y .- u ) = ( y .- v ) /\ ( z .- u ) = ( z .- v ) ) /\ u =/= v ) <-> ( ( ( X .- u ) = ( X .- v ) /\ ( y .- u ) = ( y .- v ) /\ ( z .- u ) = ( z .- v ) ) /\ u =/= v ) ) )
21		oveq1 6657	. . . . . . . . . 10 |- ( x = X -> ( x I y ) = ( X I y ) )
22	21	eleq2d 2687	. . . . . . . . 9 |- ( x = X -> ( z e. ( x I y ) <-> z e. ( X I y ) ) )
23		eleq1 2689	. . . . . . . . 9 |- ( x = X -> ( x e. ( z I y ) <-> X e. ( z I y ) ) )
24		oveq1 6657	. . . . . . . . . 10 |- ( x = X -> ( x I z ) = ( X I z ) )
25	24	eleq2d 2687	. . . . . . . . 9 |- ( x = X -> ( y e. ( x I z ) <-> y e. ( X I z ) ) )
26	22, 23, 25	3orbi123d 1398	. . . . . . . 8 |- ( x = X -> ( ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) <-> ( z e. ( X I y ) \/ X e. ( z I y ) \/ y e. ( X I z ) ) ) )
27	20, 26	imbi12d 334	. . . . . . 7 |- ( x = X -> ( ( ( ( ( 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 ) ) ) <-> ( ( ( ( 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 ) ) ) ) )
28	27	2ralbidv 2989	. . . . . 6 |- ( x = X -> ( 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 ) ) ) <-> 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 ) ) ) ) )
29		oveq1 6657	. . . . . . . . . . 11 |- ( y = Y -> ( y .- u ) = ( Y .- u ) )
30		oveq1 6657	. . . . . . . . . . 11 |- ( y = Y -> ( y .- v ) = ( Y .- v ) )
31	29, 30	eqeq12d 2637	. . . . . . . . . 10 |- ( y = Y -> ( ( y .- u ) = ( y .- v ) <-> ( Y .- u ) = ( Y .- v ) ) )
32	31	3anbi2d 1404	. . . . . . . . 9 |- ( y = Y -> ( ( ( X .- u ) = ( X .- v ) /\ ( y .- u ) = ( y .- v ) /\ ( z .- u ) = ( z .- v ) ) <-> ( ( X .- u ) = ( X .- v ) /\ ( Y .- u ) = ( Y .- v ) /\ ( z .- u ) = ( z .- v ) ) ) )
33	32	anbi1d 741	. . . . . . . 8 |- ( y = Y -> ( ( ( ( X .- u ) = ( X .- v ) /\ ( y .- u ) = ( y .- v ) /\ ( z .- u ) = ( z .- v ) ) /\ u =/= v ) <-> ( ( ( X .- u ) = ( X .- v ) /\ ( Y .- u ) = ( Y .- v ) /\ ( z .- u ) = ( z .- v ) ) /\ u =/= v ) ) )
34		oveq2 6658	. . . . . . . . . 10 |- ( y = Y -> ( X I y ) = ( X I Y ) )
35	34	eleq2d 2687	. . . . . . . . 9 |- ( y = Y -> ( z e. ( X I y ) <-> z e. ( X I Y ) ) )
36		oveq2 6658	. . . . . . . . . 10 |- ( y = Y -> ( z I y ) = ( z I Y ) )
37	36	eleq2d 2687	. . . . . . . . 9 |- ( y = Y -> ( X e. ( z I y ) <-> X e. ( z I Y ) ) )
38		eleq1 2689	. . . . . . . . 9 |- ( y = Y -> ( y e. ( X I z ) <-> Y e. ( X I z ) ) )
39	35, 37, 38	3orbi123d 1398	. . . . . . . 8 |- ( y = Y -> ( ( z e. ( X I y ) \/ X e. ( z I y ) \/ y e. ( X I z ) ) <-> ( z e. ( X I Y ) \/ X e. ( z I Y ) \/ Y e. ( X I z ) ) ) )
40	33, 39	imbi12d 334	. . . . . . 7 |- ( y = Y -> ( ( ( ( ( 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 ) ) ) <-> ( ( ( ( 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 ) ) ) ) )
41	40	2ralbidv 2989	. . . . . 6 |- ( y = Y -> ( 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 ) ) ) <-> 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 ) ) ) ) )
42		oveq1 6657	. . . . . . . . . . 11 |- ( z = Z -> ( z .- u ) = ( Z .- u ) )
43		oveq1 6657	. . . . . . . . . . 11 |- ( z = Z -> ( z .- v ) = ( Z .- v ) )
44	42, 43	eqeq12d 2637	. . . . . . . . . 10 |- ( z = Z -> ( ( z .- u ) = ( z .- v ) <-> ( Z .- u ) = ( Z .- v ) ) )
45	44	3anbi3d 1405	. . . . . . . . 9 |- ( z = Z -> ( ( ( X .- u ) = ( X .- v ) /\ ( Y .- u ) = ( Y .- v ) /\ ( z .- u ) = ( z .- v ) ) <-> ( ( X .- u ) = ( X .- v ) /\ ( Y .- u ) = ( Y .- v ) /\ ( Z .- u ) = ( Z .- v ) ) ) )
46	45	anbi1d 741	. . . . . . . 8 |- ( z = Z -> ( ( ( ( X .- u ) = ( X .- v ) /\ ( Y .- u ) = ( Y .- v ) /\ ( z .- u ) = ( z .- v ) ) /\ u =/= v ) <-> ( ( ( X .- u ) = ( X .- v ) /\ ( Y .- u ) = ( Y .- v ) /\ ( Z .- u ) = ( Z .- v ) ) /\ u =/= v ) ) )
47		eleq1 2689	. . . . . . . . 9 |- ( z = Z -> ( z e. ( X I Y ) <-> Z e. ( X I Y ) ) )
48		oveq1 6657	. . . . . . . . . 10 |- ( z = Z -> ( z I Y ) = ( Z I Y ) )
49	48	eleq2d 2687	. . . . . . . . 9 |- ( z = Z -> ( X e. ( z I Y ) <-> X e. ( Z I Y ) ) )
50		oveq2 6658	. . . . . . . . . 10 |- ( z = Z -> ( X I z ) = ( X I Z ) )
51	50	eleq2d 2687	. . . . . . . . 9 |- ( z = Z -> ( Y e. ( X I z ) <-> Y e. ( X I Z ) ) )
52	47, 49, 51	3orbi123d 1398	. . . . . . . 8 |- ( z = Z -> ( ( z e. ( X I Y ) \/ X e. ( z I Y ) \/ Y e. ( X I z ) ) <-> ( Z e. ( X I Y ) \/ X e. ( Z I Y ) \/ Y e. ( X I Z ) ) ) )
53	46, 52	imbi12d 334	. . . . . . 7 |- ( z = Z -> ( ( ( ( ( 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 ) ) ) <-> ( ( ( ( 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 ) ) ) ) )
54	53	2ralbidv 2989	. . . . . 6 |- ( z = Z -> ( 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 ) ) ) <-> 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 ) ) ) ) )
55	28, 41, 54	rspc3v 3325	. . . . 5 |- ( ( X e. P /\ Y e. P /\ Z e. P ) -> ( 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 ) ) ) -> 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 ) ) ) ) )
56	13, 14, 15, 55	syl3anc 1326	. . . 4 |- ( ph -> ( 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 ) ) ) -> 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 ) ) ) ) )
57	12, 56	mpd 15	. . 3 |- ( ph -> 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 ) ) ) )
58		axtgupdim2OLD.u	. . . 4 |- ( ph -> U e. P )
59		axtgupdim2OLD.v	. . . 4 |- ( ph -> V e. P )
60		oveq2 6658	. . . . . . . . 9 |- ( u = U -> ( X .- u ) = ( X .- U ) )
61	60	eqeq1d 2624	. . . . . . . 8 |- ( u = U -> ( ( X .- u ) = ( X .- v ) <-> ( X .- U ) = ( X .- v ) ) )
62		oveq2 6658	. . . . . . . . 9 |- ( u = U -> ( Y .- u ) = ( Y .- U ) )
63	62	eqeq1d 2624	. . . . . . . 8 |- ( u = U -> ( ( Y .- u ) = ( Y .- v ) <-> ( Y .- U ) = ( Y .- v ) ) )
64		oveq2 6658	. . . . . . . . 9 |- ( u = U -> ( Z .- u ) = ( Z .- U ) )
65	64	eqeq1d 2624	. . . . . . . 8 |- ( u = U -> ( ( Z .- u ) = ( Z .- v ) <-> ( Z .- U ) = ( Z .- v ) ) )
66	61, 63, 65	3anbi123d 1399	. . . . . . 7 |- ( u = U -> ( ( ( X .- u ) = ( X .- v ) /\ ( Y .- u ) = ( Y .- v ) /\ ( Z .- u ) = ( Z .- v ) ) <-> ( ( X .- U ) = ( X .- v ) /\ ( Y .- U ) = ( Y .- v ) /\ ( Z .- U ) = ( Z .- v ) ) ) )
67		neeq1 2856	. . . . . . 7 |- ( u = U -> ( u =/= v <-> U =/= v ) )
68	66, 67	anbi12d 747	. . . . . 6 |- ( u = U -> ( ( ( ( X .- u ) = ( X .- v ) /\ ( Y .- u ) = ( Y .- v ) /\ ( Z .- u ) = ( Z .- v ) ) /\ u =/= v ) <-> ( ( ( X .- U ) = ( X .- v ) /\ ( Y .- U ) = ( Y .- v ) /\ ( Z .- U ) = ( Z .- v ) ) /\ U =/= v ) ) )
69	68	imbi1d 331	. . . . 5 |- ( u = U -> ( ( ( ( ( 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 ) ) ) <-> ( ( ( ( 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 ) ) ) ) )
70		oveq2 6658	. . . . . . . . 9 |- ( v = V -> ( X .- v ) = ( X .- V ) )
71	70	eqeq2d 2632	. . . . . . . 8 |- ( v = V -> ( ( X .- U ) = ( X .- v ) <-> ( X .- U ) = ( X .- V ) ) )
72		oveq2 6658	. . . . . . . . 9 |- ( v = V -> ( Y .- v ) = ( Y .- V ) )
73	72	eqeq2d 2632	. . . . . . . 8 |- ( v = V -> ( ( Y .- U ) = ( Y .- v ) <-> ( Y .- U ) = ( Y .- V ) ) )
74		oveq2 6658	. . . . . . . . 9 |- ( v = V -> ( Z .- v ) = ( Z .- V ) )
75	74	eqeq2d 2632	. . . . . . . 8 |- ( v = V -> ( ( Z .- U ) = ( Z .- v ) <-> ( Z .- U ) = ( Z .- V ) ) )
76	71, 73, 75	3anbi123d 1399	. . . . . . 7 |- ( v = V -> ( ( ( X .- U ) = ( X .- v ) /\ ( Y .- U ) = ( Y .- v ) /\ ( Z .- U ) = ( Z .- v ) ) <-> ( ( X .- U ) = ( X .- V ) /\ ( Y .- U ) = ( Y .- V ) /\ ( Z .- U ) = ( Z .- V ) ) ) )
77		neeq2 2857	. . . . . . 7 |- ( v = V -> ( U =/= v <-> U =/= V ) )
78	76, 77	anbi12d 747	. . . . . 6 |- ( v = V -> ( ( ( ( X .- U ) = ( X .- v ) /\ ( Y .- U ) = ( Y .- v ) /\ ( Z .- U ) = ( Z .- v ) ) /\ U =/= v ) <-> ( ( ( X .- U ) = ( X .- V ) /\ ( Y .- U ) = ( Y .- V ) /\ ( Z .- U ) = ( Z .- V ) ) /\ U =/= V ) ) )
79	78	imbi1d 331	. . . . 5 |- ( v = V -> ( ( ( ( ( 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 ) ) ) <-> ( ( ( ( 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 ) ) ) ) )
80	69, 79	rspc2v 3322	. . . 4 |- ( ( U e. P /\ V 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 ) ) ) -> ( ( ( ( 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 ) ) ) ) )
81	58, 59, 80	syl2anc 693	. . 3 |- ( ph -> ( 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 ) ) ) -> ( ( ( ( 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 ) ) ) ) )
82	57, 81	mpd 15	. 2 |- ( ph -> ( ( ( ( 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 ) ) ) )
83	4, 5, 82	mp2and 715	1 |- ( ph -> ( Z e. ( X I Y ) \/ X e. ( Z I Y ) \/ Y e. ( X I Z ) ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 384   \/ w3o 1036   /\ w3a 1037   = wceq 1483   e. wcel 1990   =/= wne 2794   A.wral 2912   E.wrex 2913   _Vcvv 3200   ` cfv 5888  (class class class)co 6650   Basecbs 15857   distcds 15950  Itvcitv 25335  TarskiG_2Dcstrkg2d 30742

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-nul 4789

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-iota 5851  df-fv 5896  df-ov 6653  df-trkg2d 30743

This theorem is referenced by: (None)