Metamath Proof Explorer


Theorem 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 ( 𝜑 → ¬ 𝐺 DimTarskiG≥ 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 ( 𝜑 → ¬ 𝐺 DimTarskiG≥ 3 )
15 1 2 3 istrkg3ld ( 𝐺𝑉 → ( 𝐺 DimTarskiG≥ 3 ↔ ∃ 𝑢𝑃𝑣𝑃 ( 𝑢𝑣 ∧ ∃ 𝑥𝑃𝑦𝑃𝑧𝑃 ( ( ( 𝑢 𝑥 ) = ( 𝑣 𝑥 ) ∧ ( 𝑢 𝑦 ) = ( 𝑣 𝑦 ) ∧ ( 𝑢 𝑧 ) = ( 𝑣 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) ) )
16 13 15 syl ( 𝜑 → ( 𝐺 DimTarskiG≥ 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 ( 𝜑 → ( 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑍 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) )