axtgupdim2

Description: Upper dimension axiom for dimension 2, Axiom A9 of Schwabhauser p. 13. Three points X , Y and Z equidistant to two given two points U and V must be colinear. (Contributed by Thierry Arnoux, 29-May-2019) (Revised by Thierry Arnoux, 11-Jul-2020)

	Ref	Expression
Hypotheses	axtrkge.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
	axtrkge.d	⊢ − = ( dist ‘ 𝐺 )
	axtrkge.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	axtgupdim2.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
	axtgupdim2.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
	axtgupdim2.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
	axtgupdim2.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑃 )
	axtgupdim2.v	⊢ ( 𝜑 → 𝑉 ∈ 𝑃 )
	axtgupdim2.0	⊢ ( 𝜑 → 𝑈 ≠ 𝑉 )
	axtgupdim2.1	⊢ ( 𝜑 → ( 𝑈 − 𝑋 ) = ( 𝑉 − 𝑋 ) )
	axtgupdim2.2	⊢ ( 𝜑 → ( 𝑈 − 𝑌 ) = ( 𝑉 − 𝑌 ) )
	axtgupdim2.3	⊢ ( 𝜑 → ( 𝑈 − 𝑍 ) = ( 𝑉 − 𝑍 ) )
	axtgupdim2.w	⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
	axtgupdim2.g	⊢ ( 𝜑 → ¬ 𝐺 Dim_TarskiG≥ 3 )
Assertion	axtgupdim2	⊢ ( 𝜑 → ( 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑍 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) )

Proof

Step	Hyp	Ref	Expression
1		axtrkge.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		axtrkge.d	⊢ − = ( dist ‘ 𝐺 )
3		axtrkge.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
4		axtgupdim2.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
5		axtgupdim2.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
6		axtgupdim2.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
7		axtgupdim2.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑃 )
8		axtgupdim2.v	⊢ ( 𝜑 → 𝑉 ∈ 𝑃 )
9		axtgupdim2.0	⊢ ( 𝜑 → 𝑈 ≠ 𝑉 )
10		axtgupdim2.1	⊢ ( 𝜑 → ( 𝑈 − 𝑋 ) = ( 𝑉 − 𝑋 ) )
11		axtgupdim2.2	⊢ ( 𝜑 → ( 𝑈 − 𝑌 ) = ( 𝑉 − 𝑌 ) )
12		axtgupdim2.3	⊢ ( 𝜑 → ( 𝑈 − 𝑍 ) = ( 𝑉 − 𝑍 ) )
13		axtgupdim2.w	⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
14		axtgupdim2.g	⊢ ( 𝜑 → ¬ 𝐺 Dim_TarskiG≥ 3 )
15	1 2 3	istrkg3ld	⊢ ( 𝐺 ∈ 𝑉 → ( 𝐺 Dim_TarskiG≥ 3 ↔ ∃ 𝑢 ∈ 𝑃 ∃ 𝑣 ∈ 𝑃 ( 𝑢 ≠ 𝑣 ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ( ( 𝑢 − 𝑥 ) = ( 𝑣 − 𝑥 ) ∧ ( 𝑢 − 𝑦 ) = ( 𝑣 − 𝑦 ) ∧ ( 𝑢 − 𝑧 ) = ( 𝑣 − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) ) )
16	13 15	syl	⊢ ( 𝜑 → ( 𝐺 Dim_TarskiG≥ 3 ↔ ∃ 𝑢 ∈ 𝑃 ∃ 𝑣 ∈ 𝑃 ( 𝑢 ≠ 𝑣 ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ( ( 𝑢 − 𝑥 ) = ( 𝑣 − 𝑥 ) ∧ ( 𝑢 − 𝑦 ) = ( 𝑣 − 𝑦 ) ∧ ( 𝑢 − 𝑧 ) = ( 𝑣 − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) ) )
17	14 16	mtbid	⊢ ( 𝜑 → ¬ ∃ 𝑢 ∈ 𝑃 ∃ 𝑣 ∈ 𝑃 ( 𝑢 ≠ 𝑣 ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ( ( 𝑢 − 𝑥 ) = ( 𝑣 − 𝑥 ) ∧ ( 𝑢 − 𝑦 ) = ( 𝑣 − 𝑦 ) ∧ ( 𝑢 − 𝑧 ) = ( 𝑣 − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) )
18		ralnex2	⊢ ( ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ¬ ( 𝑢 ≠ 𝑣 ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ( ( 𝑢 − 𝑥 ) = ( 𝑣 − 𝑥 ) ∧ ( 𝑢 − 𝑦 ) = ( 𝑣 − 𝑦 ) ∧ ( 𝑢 − 𝑧 ) = ( 𝑣 − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) ↔ ¬ ∃ 𝑢 ∈ 𝑃 ∃ 𝑣 ∈ 𝑃 ( 𝑢 ≠ 𝑣 ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ( ( 𝑢 − 𝑥 ) = ( 𝑣 − 𝑥 ) ∧ ( 𝑢 − 𝑦 ) = ( 𝑣 − 𝑦 ) ∧ ( 𝑢 − 𝑧 ) = ( 𝑣 − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) )
19	17 18	sylibr	⊢ ( 𝜑 → ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ¬ ( 𝑢 ≠ 𝑣 ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ( ( 𝑢 − 𝑥 ) = ( 𝑣 − 𝑥 ) ∧ ( 𝑢 − 𝑦 ) = ( 𝑣 − 𝑦 ) ∧ ( 𝑢 − 𝑧 ) = ( 𝑣 − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) )
20		neeq1	⊢ ( 𝑢 = 𝑈 → ( 𝑢 ≠ 𝑣 ↔ 𝑈 ≠ 𝑣 ) )
21		oveq1	⊢ ( 𝑢 = 𝑈 → ( 𝑢 − 𝑥 ) = ( 𝑈 − 𝑥 ) )
22	21	eqeq1d	⊢ ( 𝑢 = 𝑈 → ( ( 𝑢 − 𝑥 ) = ( 𝑣 − 𝑥 ) ↔ ( 𝑈 − 𝑥 ) = ( 𝑣 − 𝑥 ) ) )
23		oveq1	⊢ ( 𝑢 = 𝑈 → ( 𝑢 − 𝑦 ) = ( 𝑈 − 𝑦 ) )
24	23	eqeq1d	⊢ ( 𝑢 = 𝑈 → ( ( 𝑢 − 𝑦 ) = ( 𝑣 − 𝑦 ) ↔ ( 𝑈 − 𝑦 ) = ( 𝑣 − 𝑦 ) ) )
25		oveq1	⊢ ( 𝑢 = 𝑈 → ( 𝑢 − 𝑧 ) = ( 𝑈 − 𝑧 ) )
26	25	eqeq1d	⊢ ( 𝑢 = 𝑈 → ( ( 𝑢 − 𝑧 ) = ( 𝑣 − 𝑧 ) ↔ ( 𝑈 − 𝑧 ) = ( 𝑣 − 𝑧 ) ) )
27	22 24 26	3anbi123d	⊢ ( 𝑢 = 𝑈 → ( ( ( 𝑢 − 𝑥 ) = ( 𝑣 − 𝑥 ) ∧ ( 𝑢 − 𝑦 ) = ( 𝑣 − 𝑦 ) ∧ ( 𝑢 − 𝑧 ) = ( 𝑣 − 𝑧 ) ) ↔ ( ( 𝑈 − 𝑥 ) = ( 𝑣 − 𝑥 ) ∧ ( 𝑈 − 𝑦 ) = ( 𝑣 − 𝑦 ) ∧ ( 𝑈 − 𝑧 ) = ( 𝑣 − 𝑧 ) ) ) )
28	27	anbi1d	⊢ ( 𝑢 = 𝑈 → ( ( ( ( 𝑢 − 𝑥 ) = ( 𝑣 − 𝑥 ) ∧ ( 𝑢 − 𝑦 ) = ( 𝑣 − 𝑦 ) ∧ ( 𝑢 − 𝑧 ) = ( 𝑣 − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ↔ ( ( ( 𝑈 − 𝑥 ) = ( 𝑣 − 𝑥 ) ∧ ( 𝑈 − 𝑦 ) = ( 𝑣 − 𝑦 ) ∧ ( 𝑈 − 𝑧 ) = ( 𝑣 − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) )
29	28	rexbidv	⊢ ( 𝑢 = 𝑈 → ( ∃ 𝑧 ∈ 𝑃 ( ( ( 𝑢 − 𝑥 ) = ( 𝑣 − 𝑥 ) ∧ ( 𝑢 − 𝑦 ) = ( 𝑣 − 𝑦 ) ∧ ( 𝑢 − 𝑧 ) = ( 𝑣 − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ↔ ∃ 𝑧 ∈ 𝑃 ( ( ( 𝑈 − 𝑥 ) = ( 𝑣 − 𝑥 ) ∧ ( 𝑈 − 𝑦 ) = ( 𝑣 − 𝑦 ) ∧ ( 𝑈 − 𝑧 ) = ( 𝑣 − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) )
30	29	2rexbidv	⊢ ( 𝑢 = 𝑈 → ( ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ( ( 𝑢 − 𝑥 ) = ( 𝑣 − 𝑥 ) ∧ ( 𝑢 − 𝑦 ) = ( 𝑣 − 𝑦 ) ∧ ( 𝑢 − 𝑧 ) = ( 𝑣 − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ↔ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ( ( 𝑈 − 𝑥 ) = ( 𝑣 − 𝑥 ) ∧ ( 𝑈 − 𝑦 ) = ( 𝑣 − 𝑦 ) ∧ ( 𝑈 − 𝑧 ) = ( 𝑣 − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) )
31	20 30	anbi12d	⊢ ( 𝑢 = 𝑈 → ( ( 𝑢 ≠ 𝑣 ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ( ( 𝑢 − 𝑥 ) = ( 𝑣 − 𝑥 ) ∧ ( 𝑢 − 𝑦 ) = ( 𝑣 − 𝑦 ) ∧ ( 𝑢 − 𝑧 ) = ( 𝑣 − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) ↔ ( 𝑈 ≠ 𝑣 ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ( ( 𝑈 − 𝑥 ) = ( 𝑣 − 𝑥 ) ∧ ( 𝑈 − 𝑦 ) = ( 𝑣 − 𝑦 ) ∧ ( 𝑈 − 𝑧 ) = ( 𝑣 − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) ) )
32	31	notbid	⊢ ( 𝑢 = 𝑈 → ( ¬ ( 𝑢 ≠ 𝑣 ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ( ( 𝑢 − 𝑥 ) = ( 𝑣 − 𝑥 ) ∧ ( 𝑢 − 𝑦 ) = ( 𝑣 − 𝑦 ) ∧ ( 𝑢 − 𝑧 ) = ( 𝑣 − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) ↔ ¬ ( 𝑈 ≠ 𝑣 ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ( ( 𝑈 − 𝑥 ) = ( 𝑣 − 𝑥 ) ∧ ( 𝑈 − 𝑦 ) = ( 𝑣 − 𝑦 ) ∧ ( 𝑈 − 𝑧 ) = ( 𝑣 − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) ) )
33		neeq2	⊢ ( 𝑣 = 𝑉 → ( 𝑈 ≠ 𝑣 ↔ 𝑈 ≠ 𝑉 ) )
34		oveq1	⊢ ( 𝑣 = 𝑉 → ( 𝑣 − 𝑥 ) = ( 𝑉 − 𝑥 ) )
35	34	eqeq2d	⊢ ( 𝑣 = 𝑉 → ( ( 𝑈 − 𝑥 ) = ( 𝑣 − 𝑥 ) ↔ ( 𝑈 − 𝑥 ) = ( 𝑉 − 𝑥 ) ) )
36		oveq1	⊢ ( 𝑣 = 𝑉 → ( 𝑣 − 𝑦 ) = ( 𝑉 − 𝑦 ) )
37	36	eqeq2d	⊢ ( 𝑣 = 𝑉 → ( ( 𝑈 − 𝑦 ) = ( 𝑣 − 𝑦 ) ↔ ( 𝑈 − 𝑦 ) = ( 𝑉 − 𝑦 ) ) )
38		oveq1	⊢ ( 𝑣 = 𝑉 → ( 𝑣 − 𝑧 ) = ( 𝑉 − 𝑧 ) )
39	38	eqeq2d	⊢ ( 𝑣 = 𝑉 → ( ( 𝑈 − 𝑧 ) = ( 𝑣 − 𝑧 ) ↔ ( 𝑈 − 𝑧 ) = ( 𝑉 − 𝑧 ) ) )
40	35 37 39	3anbi123d	⊢ ( 𝑣 = 𝑉 → ( ( ( 𝑈 − 𝑥 ) = ( 𝑣 − 𝑥 ) ∧ ( 𝑈 − 𝑦 ) = ( 𝑣 − 𝑦 ) ∧ ( 𝑈 − 𝑧 ) = ( 𝑣 − 𝑧 ) ) ↔ ( ( 𝑈 − 𝑥 ) = ( 𝑉 − 𝑥 ) ∧ ( 𝑈 − 𝑦 ) = ( 𝑉 − 𝑦 ) ∧ ( 𝑈 − 𝑧 ) = ( 𝑉 − 𝑧 ) ) ) )
41	40	anbi1d	⊢ ( 𝑣 = 𝑉 → ( ( ( ( 𝑈 − 𝑥 ) = ( 𝑣 − 𝑥 ) ∧ ( 𝑈 − 𝑦 ) = ( 𝑣 − 𝑦 ) ∧ ( 𝑈 − 𝑧 ) = ( 𝑣 − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ↔ ( ( ( 𝑈 − 𝑥 ) = ( 𝑉 − 𝑥 ) ∧ ( 𝑈 − 𝑦 ) = ( 𝑉 − 𝑦 ) ∧ ( 𝑈 − 𝑧 ) = ( 𝑉 − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) )
42	41	rexbidv	⊢ ( 𝑣 = 𝑉 → ( ∃ 𝑧 ∈ 𝑃 ( ( ( 𝑈 − 𝑥 ) = ( 𝑣 − 𝑥 ) ∧ ( 𝑈 − 𝑦 ) = ( 𝑣 − 𝑦 ) ∧ ( 𝑈 − 𝑧 ) = ( 𝑣 − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ↔ ∃ 𝑧 ∈ 𝑃 ( ( ( 𝑈 − 𝑥 ) = ( 𝑉 − 𝑥 ) ∧ ( 𝑈 − 𝑦 ) = ( 𝑉 − 𝑦 ) ∧ ( 𝑈 − 𝑧 ) = ( 𝑉 − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) )
43	42	2rexbidv	⊢ ( 𝑣 = 𝑉 → ( ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ( ( 𝑈 − 𝑥 ) = ( 𝑣 − 𝑥 ) ∧ ( 𝑈 − 𝑦 ) = ( 𝑣 − 𝑦 ) ∧ ( 𝑈 − 𝑧 ) = ( 𝑣 − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ↔ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ( ( 𝑈 − 𝑥 ) = ( 𝑉 − 𝑥 ) ∧ ( 𝑈 − 𝑦 ) = ( 𝑉 − 𝑦 ) ∧ ( 𝑈 − 𝑧 ) = ( 𝑉 − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) )
44	33 43	anbi12d	⊢ ( 𝑣 = 𝑉 → ( ( 𝑈 ≠ 𝑣 ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ( ( 𝑈 − 𝑥 ) = ( 𝑣 − 𝑥 ) ∧ ( 𝑈 − 𝑦 ) = ( 𝑣 − 𝑦 ) ∧ ( 𝑈 − 𝑧 ) = ( 𝑣 − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) ↔ ( 𝑈 ≠ 𝑉 ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ( ( 𝑈 − 𝑥 ) = ( 𝑉 − 𝑥 ) ∧ ( 𝑈 − 𝑦 ) = ( 𝑉 − 𝑦 ) ∧ ( 𝑈 − 𝑧 ) = ( 𝑉 − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) ) )
45	44	notbid	⊢ ( 𝑣 = 𝑉 → ( ¬ ( 𝑈 ≠ 𝑣 ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ( ( 𝑈 − 𝑥 ) = ( 𝑣 − 𝑥 ) ∧ ( 𝑈 − 𝑦 ) = ( 𝑣 − 𝑦 ) ∧ ( 𝑈 − 𝑧 ) = ( 𝑣 − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) ↔ ¬ ( 𝑈 ≠ 𝑉 ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ( ( 𝑈 − 𝑥 ) = ( 𝑉 − 𝑥 ) ∧ ( 𝑈 − 𝑦 ) = ( 𝑉 − 𝑦 ) ∧ ( 𝑈 − 𝑧 ) = ( 𝑉 − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) ) )
46	32 45	rspc2v	⊢ ( ( 𝑈 ∈ 𝑃 ∧ 𝑉 ∈ 𝑃 ) → ( ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ¬ ( 𝑢 ≠ 𝑣 ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ( ( 𝑢 − 𝑥 ) = ( 𝑣 − 𝑥 ) ∧ ( 𝑢 − 𝑦 ) = ( 𝑣 − 𝑦 ) ∧ ( 𝑢 − 𝑧 ) = ( 𝑣 − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) → ¬ ( 𝑈 ≠ 𝑉 ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ( ( 𝑈 − 𝑥 ) = ( 𝑉 − 𝑥 ) ∧ ( 𝑈 − 𝑦 ) = ( 𝑉 − 𝑦 ) ∧ ( 𝑈 − 𝑧 ) = ( 𝑉 − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) ) )
47	7 8 46	syl2anc	⊢ ( 𝜑 → ( ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ¬ ( 𝑢 ≠ 𝑣 ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ( ( 𝑢 − 𝑥 ) = ( 𝑣 − 𝑥 ) ∧ ( 𝑢 − 𝑦 ) = ( 𝑣 − 𝑦 ) ∧ ( 𝑢 − 𝑧 ) = ( 𝑣 − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) → ¬ ( 𝑈 ≠ 𝑉 ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ( ( 𝑈 − 𝑥 ) = ( 𝑉 − 𝑥 ) ∧ ( 𝑈 − 𝑦 ) = ( 𝑉 − 𝑦 ) ∧ ( 𝑈 − 𝑧 ) = ( 𝑉 − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) ) )
48	19 47	mpd	⊢ ( 𝜑 → ¬ ( 𝑈 ≠ 𝑉 ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ( ( 𝑈 − 𝑥 ) = ( 𝑉 − 𝑥 ) ∧ ( 𝑈 − 𝑦 ) = ( 𝑉 − 𝑦 ) ∧ ( 𝑈 − 𝑧 ) = ( 𝑉 − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) )
49		imnan	⊢ ( ( 𝑈 ≠ 𝑉 → ¬ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ( ( 𝑈 − 𝑥 ) = ( 𝑉 − 𝑥 ) ∧ ( 𝑈 − 𝑦 ) = ( 𝑉 − 𝑦 ) ∧ ( 𝑈 − 𝑧 ) = ( 𝑉 − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) ↔ ¬ ( 𝑈 ≠ 𝑉 ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ( ( 𝑈 − 𝑥 ) = ( 𝑉 − 𝑥 ) ∧ ( 𝑈 − 𝑦 ) = ( 𝑉 − 𝑦 ) ∧ ( 𝑈 − 𝑧 ) = ( 𝑉 − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) )
50	48 49	sylibr	⊢ ( 𝜑 → ( 𝑈 ≠ 𝑉 → ¬ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ( ( 𝑈 − 𝑥 ) = ( 𝑉 − 𝑥 ) ∧ ( 𝑈 − 𝑦 ) = ( 𝑉 − 𝑦 ) ∧ ( 𝑈 − 𝑧 ) = ( 𝑉 − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) )
51	9 50	mpd	⊢ ( 𝜑 → ¬ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ( ( 𝑈 − 𝑥 ) = ( 𝑉 − 𝑥 ) ∧ ( 𝑈 − 𝑦 ) = ( 𝑉 − 𝑦 ) ∧ ( 𝑈 − 𝑧 ) = ( 𝑉 − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) )
52		ralnex3	⊢ ( ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ¬ ( ( ( 𝑈 − 𝑥 ) = ( 𝑉 − 𝑥 ) ∧ ( 𝑈 − 𝑦 ) = ( 𝑉 − 𝑦 ) ∧ ( 𝑈 − 𝑧 ) = ( 𝑉 − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ↔ ¬ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ( ( 𝑈 − 𝑥 ) = ( 𝑉 − 𝑥 ) ∧ ( 𝑈 − 𝑦 ) = ( 𝑉 − 𝑦 ) ∧ ( 𝑈 − 𝑧 ) = ( 𝑉 − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) )
53	51 52	sylibr	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ¬ ( ( ( 𝑈 − 𝑥 ) = ( 𝑉 − 𝑥 ) ∧ ( 𝑈 − 𝑦 ) = ( 𝑉 − 𝑦 ) ∧ ( 𝑈 − 𝑧 ) = ( 𝑉 − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) )
54		oveq2	⊢ ( 𝑥 = 𝑋 → ( 𝑈 − 𝑥 ) = ( 𝑈 − 𝑋 ) )
55		oveq2	⊢ ( 𝑥 = 𝑋 → ( 𝑉 − 𝑥 ) = ( 𝑉 − 𝑋 ) )
56	54 55	eqeq12d	⊢ ( 𝑥 = 𝑋 → ( ( 𝑈 − 𝑥 ) = ( 𝑉 − 𝑥 ) ↔ ( 𝑈 − 𝑋 ) = ( 𝑉 − 𝑋 ) ) )
57	56	3anbi1d	⊢ ( 𝑥 = 𝑋 → ( ( ( 𝑈 − 𝑥 ) = ( 𝑉 − 𝑥 ) ∧ ( 𝑈 − 𝑦 ) = ( 𝑉 − 𝑦 ) ∧ ( 𝑈 − 𝑧 ) = ( 𝑉 − 𝑧 ) ) ↔ ( ( 𝑈 − 𝑋 ) = ( 𝑉 − 𝑋 ) ∧ ( 𝑈 − 𝑦 ) = ( 𝑉 − 𝑦 ) ∧ ( 𝑈 − 𝑧 ) = ( 𝑉 − 𝑧 ) ) ) )
58		oveq1	⊢ ( 𝑥 = 𝑋 → ( 𝑥 𝐼 𝑦 ) = ( 𝑋 𝐼 𝑦 ) )
59	58	eleq2d	⊢ ( 𝑥 = 𝑋 → ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ↔ 𝑧 ∈ ( 𝑋 𝐼 𝑦 ) ) )
60		eleq1	⊢ ( 𝑥 = 𝑋 → ( 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ↔ 𝑋 ∈ ( 𝑧 𝐼 𝑦 ) ) )
61		oveq1	⊢ ( 𝑥 = 𝑋 → ( 𝑥 𝐼 𝑧 ) = ( 𝑋 𝐼 𝑧 ) )
62	61	eleq2d	⊢ ( 𝑥 = 𝑋 → ( 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ↔ 𝑦 ∈ ( 𝑋 𝐼 𝑧 ) ) )
63	59 60 62	3orbi123d	⊢ ( 𝑥 = 𝑋 → ( ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ↔ ( 𝑧 ∈ ( 𝑋 𝐼 𝑦 ) ∨ 𝑋 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑋 𝐼 𝑧 ) ) ) )
64	63	notbid	⊢ ( 𝑥 = 𝑋 → ( ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ↔ ¬ ( 𝑧 ∈ ( 𝑋 𝐼 𝑦 ) ∨ 𝑋 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑋 𝐼 𝑧 ) ) ) )
65	57 64	anbi12d	⊢ ( 𝑥 = 𝑋 → ( ( ( ( 𝑈 − 𝑥 ) = ( 𝑉 − 𝑥 ) ∧ ( 𝑈 − 𝑦 ) = ( 𝑉 − 𝑦 ) ∧ ( 𝑈 − 𝑧 ) = ( 𝑉 − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ↔ ( ( ( 𝑈 − 𝑋 ) = ( 𝑉 − 𝑋 ) ∧ ( 𝑈 − 𝑦 ) = ( 𝑉 − 𝑦 ) ∧ ( 𝑈 − 𝑧 ) = ( 𝑉 − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑋 𝐼 𝑦 ) ∨ 𝑋 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑋 𝐼 𝑧 ) ) ) ) )
66	65	notbid	⊢ ( 𝑥 = 𝑋 → ( ¬ ( ( ( 𝑈 − 𝑥 ) = ( 𝑉 − 𝑥 ) ∧ ( 𝑈 − 𝑦 ) = ( 𝑉 − 𝑦 ) ∧ ( 𝑈 − 𝑧 ) = ( 𝑉 − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ↔ ¬ ( ( ( 𝑈 − 𝑋 ) = ( 𝑉 − 𝑋 ) ∧ ( 𝑈 − 𝑦 ) = ( 𝑉 − 𝑦 ) ∧ ( 𝑈 − 𝑧 ) = ( 𝑉 − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑋 𝐼 𝑦 ) ∨ 𝑋 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑋 𝐼 𝑧 ) ) ) ) )
67		oveq2	⊢ ( 𝑦 = 𝑌 → ( 𝑈 − 𝑦 ) = ( 𝑈 − 𝑌 ) )
68		oveq2	⊢ ( 𝑦 = 𝑌 → ( 𝑉 − 𝑦 ) = ( 𝑉 − 𝑌 ) )
69	67 68	eqeq12d	⊢ ( 𝑦 = 𝑌 → ( ( 𝑈 − 𝑦 ) = ( 𝑉 − 𝑦 ) ↔ ( 𝑈 − 𝑌 ) = ( 𝑉 − 𝑌 ) ) )
70	69	3anbi2d	⊢ ( 𝑦 = 𝑌 → ( ( ( 𝑈 − 𝑋 ) = ( 𝑉 − 𝑋 ) ∧ ( 𝑈 − 𝑦 ) = ( 𝑉 − 𝑦 ) ∧ ( 𝑈 − 𝑧 ) = ( 𝑉 − 𝑧 ) ) ↔ ( ( 𝑈 − 𝑋 ) = ( 𝑉 − 𝑋 ) ∧ ( 𝑈 − 𝑌 ) = ( 𝑉 − 𝑌 ) ∧ ( 𝑈 − 𝑧 ) = ( 𝑉 − 𝑧 ) ) ) )
71		oveq2	⊢ ( 𝑦 = 𝑌 → ( 𝑋 𝐼 𝑦 ) = ( 𝑋 𝐼 𝑌 ) )
72	71	eleq2d	⊢ ( 𝑦 = 𝑌 → ( 𝑧 ∈ ( 𝑋 𝐼 𝑦 ) ↔ 𝑧 ∈ ( 𝑋 𝐼 𝑌 ) ) )
73		oveq2	⊢ ( 𝑦 = 𝑌 → ( 𝑧 𝐼 𝑦 ) = ( 𝑧 𝐼 𝑌 ) )
74	73	eleq2d	⊢ ( 𝑦 = 𝑌 → ( 𝑋 ∈ ( 𝑧 𝐼 𝑦 ) ↔ 𝑋 ∈ ( 𝑧 𝐼 𝑌 ) ) )
75		eleq1	⊢ ( 𝑦 = 𝑌 → ( 𝑦 ∈ ( 𝑋 𝐼 𝑧 ) ↔ 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ) )
76	72 74 75	3orbi123d	⊢ ( 𝑦 = 𝑌 → ( ( 𝑧 ∈ ( 𝑋 𝐼 𝑦 ) ∨ 𝑋 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑋 𝐼 𝑧 ) ) ↔ ( 𝑧 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑧 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ) ) )
77	76	notbid	⊢ ( 𝑦 = 𝑌 → ( ¬ ( 𝑧 ∈ ( 𝑋 𝐼 𝑦 ) ∨ 𝑋 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑋 𝐼 𝑧 ) ) ↔ ¬ ( 𝑧 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑧 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ) ) )
78	70 77	anbi12d	⊢ ( 𝑦 = 𝑌 → ( ( ( ( 𝑈 − 𝑋 ) = ( 𝑉 − 𝑋 ) ∧ ( 𝑈 − 𝑦 ) = ( 𝑉 − 𝑦 ) ∧ ( 𝑈 − 𝑧 ) = ( 𝑉 − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑋 𝐼 𝑦 ) ∨ 𝑋 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑋 𝐼 𝑧 ) ) ) ↔ ( ( ( 𝑈 − 𝑋 ) = ( 𝑉 − 𝑋 ) ∧ ( 𝑈 − 𝑌 ) = ( 𝑉 − 𝑌 ) ∧ ( 𝑈 − 𝑧 ) = ( 𝑉 − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑧 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ) ) ) )
79	78	notbid	⊢ ( 𝑦 = 𝑌 → ( ¬ ( ( ( 𝑈 − 𝑋 ) = ( 𝑉 − 𝑋 ) ∧ ( 𝑈 − 𝑦 ) = ( 𝑉 − 𝑦 ) ∧ ( 𝑈 − 𝑧 ) = ( 𝑉 − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑋 𝐼 𝑦 ) ∨ 𝑋 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑋 𝐼 𝑧 ) ) ) ↔ ¬ ( ( ( 𝑈 − 𝑋 ) = ( 𝑉 − 𝑋 ) ∧ ( 𝑈 − 𝑌 ) = ( 𝑉 − 𝑌 ) ∧ ( 𝑈 − 𝑧 ) = ( 𝑉 − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑧 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ) ) ) )
80		oveq2	⊢ ( 𝑧 = 𝑍 → ( 𝑈 − 𝑧 ) = ( 𝑈 − 𝑍 ) )
81		oveq2	⊢ ( 𝑧 = 𝑍 → ( 𝑉 − 𝑧 ) = ( 𝑉 − 𝑍 ) )
82	80 81	eqeq12d	⊢ ( 𝑧 = 𝑍 → ( ( 𝑈 − 𝑧 ) = ( 𝑉 − 𝑧 ) ↔ ( 𝑈 − 𝑍 ) = ( 𝑉 − 𝑍 ) ) )
83	82	3anbi3d	⊢ ( 𝑧 = 𝑍 → ( ( ( 𝑈 − 𝑋 ) = ( 𝑉 − 𝑋 ) ∧ ( 𝑈 − 𝑌 ) = ( 𝑉 − 𝑌 ) ∧ ( 𝑈 − 𝑧 ) = ( 𝑉 − 𝑧 ) ) ↔ ( ( 𝑈 − 𝑋 ) = ( 𝑉 − 𝑋 ) ∧ ( 𝑈 − 𝑌 ) = ( 𝑉 − 𝑌 ) ∧ ( 𝑈 − 𝑍 ) = ( 𝑉 − 𝑍 ) ) ) )
84		eleq1	⊢ ( 𝑧 = 𝑍 → ( 𝑧 ∈ ( 𝑋 𝐼 𝑌 ) ↔ 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ) )
85		oveq1	⊢ ( 𝑧 = 𝑍 → ( 𝑧 𝐼 𝑌 ) = ( 𝑍 𝐼 𝑌 ) )
86	85	eleq2d	⊢ ( 𝑧 = 𝑍 → ( 𝑋 ∈ ( 𝑧 𝐼 𝑌 ) ↔ 𝑋 ∈ ( 𝑍 𝐼 𝑌 ) ) )
87		oveq2	⊢ ( 𝑧 = 𝑍 → ( 𝑋 𝐼 𝑧 ) = ( 𝑋 𝐼 𝑍 ) )
88	87	eleq2d	⊢ ( 𝑧 = 𝑍 → ( 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ↔ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) )
89	84 86 88	3orbi123d	⊢ ( 𝑧 = 𝑍 → ( ( 𝑧 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑧 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ) ↔ ( 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑍 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ) )
90	89	notbid	⊢ ( 𝑧 = 𝑍 → ( ¬ ( 𝑧 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑧 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ) ↔ ¬ ( 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑍 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ) )
91	83 90	anbi12d	⊢ ( 𝑧 = 𝑍 → ( ( ( ( 𝑈 − 𝑋 ) = ( 𝑉 − 𝑋 ) ∧ ( 𝑈 − 𝑌 ) = ( 𝑉 − 𝑌 ) ∧ ( 𝑈 − 𝑧 ) = ( 𝑉 − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑧 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ) ) ↔ ( ( ( 𝑈 − 𝑋 ) = ( 𝑉 − 𝑋 ) ∧ ( 𝑈 − 𝑌 ) = ( 𝑉 − 𝑌 ) ∧ ( 𝑈 − 𝑍 ) = ( 𝑉 − 𝑍 ) ) ∧ ¬ ( 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑍 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ) ) )
92	91	notbid	⊢ ( 𝑧 = 𝑍 → ( ¬ ( ( ( 𝑈 − 𝑋 ) = ( 𝑉 − 𝑋 ) ∧ ( 𝑈 − 𝑌 ) = ( 𝑉 − 𝑌 ) ∧ ( 𝑈 − 𝑧 ) = ( 𝑉 − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑧 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ) ) ↔ ¬ ( ( ( 𝑈 − 𝑋 ) = ( 𝑉 − 𝑋 ) ∧ ( 𝑈 − 𝑌 ) = ( 𝑉 − 𝑌 ) ∧ ( 𝑈 − 𝑍 ) = ( 𝑉 − 𝑍 ) ) ∧ ¬ ( 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑍 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ) ) )
93	66 79 92	rspc3v	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃 ) → ( ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ¬ ( ( ( 𝑈 − 𝑥 ) = ( 𝑉 − 𝑥 ) ∧ ( 𝑈 − 𝑦 ) = ( 𝑉 − 𝑦 ) ∧ ( 𝑈 − 𝑧 ) = ( 𝑉 − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) → ¬ ( ( ( 𝑈 − 𝑋 ) = ( 𝑉 − 𝑋 ) ∧ ( 𝑈 − 𝑌 ) = ( 𝑉 − 𝑌 ) ∧ ( 𝑈 − 𝑍 ) = ( 𝑉 − 𝑍 ) ) ∧ ¬ ( 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑍 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ) ) )
94	4 5 6 93	syl3anc	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ¬ ( ( ( 𝑈 − 𝑥 ) = ( 𝑉 − 𝑥 ) ∧ ( 𝑈 − 𝑦 ) = ( 𝑉 − 𝑦 ) ∧ ( 𝑈 − 𝑧 ) = ( 𝑉 − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) → ¬ ( ( ( 𝑈 − 𝑋 ) = ( 𝑉 − 𝑋 ) ∧ ( 𝑈 − 𝑌 ) = ( 𝑉 − 𝑌 ) ∧ ( 𝑈 − 𝑍 ) = ( 𝑉 − 𝑍 ) ) ∧ ¬ ( 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑍 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ) ) )
95	53 94	mpd	⊢ ( 𝜑 → ¬ ( ( ( 𝑈 − 𝑋 ) = ( 𝑉 − 𝑋 ) ∧ ( 𝑈 − 𝑌 ) = ( 𝑉 − 𝑌 ) ∧ ( 𝑈 − 𝑍 ) = ( 𝑉 − 𝑍 ) ) ∧ ¬ ( 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑍 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ) )
96		imnan	⊢ ( ( ( ( 𝑈 − 𝑋 ) = ( 𝑉 − 𝑋 ) ∧ ( 𝑈 − 𝑌 ) = ( 𝑉 − 𝑌 ) ∧ ( 𝑈 − 𝑍 ) = ( 𝑉 − 𝑍 ) ) → ¬ ¬ ( 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑍 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ) ↔ ¬ ( ( ( 𝑈 − 𝑋 ) = ( 𝑉 − 𝑋 ) ∧ ( 𝑈 − 𝑌 ) = ( 𝑉 − 𝑌 ) ∧ ( 𝑈 − 𝑍 ) = ( 𝑉 − 𝑍 ) ) ∧ ¬ ( 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑍 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ) )
97	95 96	sylibr	⊢ ( 𝜑 → ( ( ( 𝑈 − 𝑋 ) = ( 𝑉 − 𝑋 ) ∧ ( 𝑈 − 𝑌 ) = ( 𝑉 − 𝑌 ) ∧ ( 𝑈 − 𝑍 ) = ( 𝑉 − 𝑍 ) ) → ¬ ¬ ( 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑍 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ) )
98	10 11 12 97	mp3and	⊢ ( 𝜑 → ¬ ¬ ( 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑍 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) )
99	98	notnotrd	⊢ ( 𝜑 → ( 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑍 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) )

Metamath Proof Explorer

Theorem axtgupdim2

Proof