Metamath Proof Explorer

Theorem legso

Description: The "shorter than" relation induces an order on pairs. Remark 5.13 of Schwabhauser p. 42. (Contributed by Thierry Arnoux, 27-Jun-2019)

Ref Expression
Hypotheses legval.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
legval.d ⊢ − = ( dist ‘ 𝐺 )
legval.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
legval.l ⊢ ≤ = ( ≤G ‘ 𝐺 )
legval.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
legso.a ⊢ 𝐸 = ( − “ ( 𝑃 × 𝑃 ) )
legso.f ⊢ ( 𝜑 → Fun − )
legso.l ⊢ < = ( ( ≤ ↾ 𝐸 ) ∖ I )
legso.d ⊢ ( 𝜑 → ( 𝑃 × 𝑃 ) ⊆ dom − )
Assertion legso ( 𝜑 → < Or 𝐸 )

Proof

Step Hyp Ref Expression
1 legval.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 legval.d ⊢ − = ( dist ‘ 𝐺 )
3 legval.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
4 legval.l ⊢ ≤ = ( ≤G ‘ 𝐺 )
5 legval.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
6 legso.a ⊢ 𝐸 = ( − “ ( 𝑃 × 𝑃 ) )
7 legso.f ⊢ ( 𝜑 → Fun − )
8 legso.l ⊢ < = ( ( ≤ ↾ 𝐸 ) ∖ I )
9 legso.d ⊢ ( 𝜑 → ( 𝑃 × 𝑃 ) ⊆ dom − )
10 neirr ⊢ ¬ ( 𝑥 − 𝑦 ) ≠ ( 𝑥 − 𝑦 )
11 10 intnan ⊢ ¬ ( ( 𝑥 − 𝑦 ) ≤ ( 𝑥 − 𝑦 ) ∧ ( 𝑥 − 𝑦 ) ≠ ( 𝑥 − 𝑦 ) )
12 5 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) → 𝐺 ∈ TarskiG )
13 12 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) → 𝐺 ∈ TarskiG )
14 7 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) → Fun − )
15 14 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) → Fun − )
16 9 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) → ( 𝑃 × 𝑃 ) ⊆ dom − )
17 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) → 𝑥 ∈ 𝑃 )
18 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) → 𝑦 ∈ 𝑃 )
19 1 2 3 4 13 6 15 8 16 17 18 ltgov ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) → ( ( 𝑥 − 𝑦 ) < ( 𝑥 − 𝑦 ) ↔ ( ( 𝑥 − 𝑦 ) ≤ ( 𝑥 − 𝑦 ) ∧ ( 𝑥 − 𝑦 ) ≠ ( 𝑥 − 𝑦 ) ) ) )
20 11 19 mtbiri ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) → ¬ ( 𝑥 − 𝑦 ) < ( 𝑥 − 𝑦 ) )
21 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) → 𝑎 = ( 𝑥 − 𝑦 ) )
22 21 21 breq12d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) → ( 𝑎 < 𝑎 ↔ ( 𝑥 − 𝑦 ) < ( 𝑥 − 𝑦 ) ) )
23 20 22 mtbird ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) → ¬ 𝑎 < 𝑎 )
24 simpr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) → 𝑎 ∈ 𝐸 )
25 1 2 3 4 12 6 14 24 ltgseg ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) → ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 𝑎 = ( 𝑥 − 𝑦 ) )
26 23 25 r19.29vva ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) → ¬ 𝑎 < 𝑎 )
27 5 ad8antr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) ∧ ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑏 = ( 𝑧 − 𝑡 ) ) → 𝐺 ∈ TarskiG )
28 27 ad3antrrr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) ∧ ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑏 = ( 𝑧 − 𝑡 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑐 = ( 𝑢 − 𝑣 ) ) → 𝐺 ∈ TarskiG )
29 simp-9r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) ∧ ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑏 = ( 𝑧 − 𝑡 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑐 = ( 𝑢 − 𝑣 ) ) → 𝑥 ∈ 𝑃 )
30 simp-8r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) ∧ ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑏 = ( 𝑧 − 𝑡 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑐 = ( 𝑢 − 𝑣 ) ) → 𝑦 ∈ 𝑃 )
31 simp-6r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) ∧ ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑏 = ( 𝑧 − 𝑡 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑐 = ( 𝑢 − 𝑣 ) ) → 𝑧 ∈ 𝑃 )
32 simp-5r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) ∧ ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑏 = ( 𝑧 − 𝑡 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑐 = ( 𝑢 − 𝑣 ) ) → 𝑡 ∈ 𝑃 )
33 simpllr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) ∧ ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑏 = ( 𝑧 − 𝑡 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑐 = ( 𝑢 − 𝑣 ) ) → 𝑢 ∈ 𝑃 )
34 simplr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) ∧ ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑏 = ( 𝑧 − 𝑡 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑐 = ( 𝑢 − 𝑣 ) ) → 𝑣 ∈ 𝑃 )
35 simp-10r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) ∧ ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑏 = ( 𝑧 − 𝑡 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑐 = ( 𝑢 − 𝑣 ) ) → ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ) )
36 35 simpld ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) ∧ ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑏 = ( 𝑧 − 𝑡 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑐 = ( 𝑢 − 𝑣 ) ) → 𝑎 < 𝑏 )
37 simp-7r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) ∧ ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑏 = ( 𝑧 − 𝑡 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑐 = ( 𝑢 − 𝑣 ) ) → 𝑎 = ( 𝑥 − 𝑦 ) )
38 simp-4r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) ∧ ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑏 = ( 𝑧 − 𝑡 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑐 = ( 𝑢 − 𝑣 ) ) → 𝑏 = ( 𝑧 − 𝑡 ) )
39 36 37 38 3brtr3d ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) ∧ ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑏 = ( 𝑧 − 𝑡 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑐 = ( 𝑢 − 𝑣 ) ) → ( 𝑥 − 𝑦 ) < ( 𝑧 − 𝑡 ) )
40 7 ad8antr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) ∧ ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑏 = ( 𝑧 − 𝑡 ) ) → Fun − )
41 40 ad3antrrr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) ∧ ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑏 = ( 𝑧 − 𝑡 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑐 = ( 𝑢 − 𝑣 ) ) → Fun − )
42 9 ad8antr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) ∧ ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑏 = ( 𝑧 − 𝑡 ) ) → ( 𝑃 × 𝑃 ) ⊆ dom − )
43 42 ad3antrrr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) ∧ ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑏 = ( 𝑧 − 𝑡 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑐 = ( 𝑢 − 𝑣 ) ) → ( 𝑃 × 𝑃 ) ⊆ dom − )
44 1 2 3 4 28 6 41 8 43 29 30 ltgov ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) ∧ ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑏 = ( 𝑧 − 𝑡 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑐 = ( 𝑢 − 𝑣 ) ) → ( ( 𝑥 − 𝑦 ) < ( 𝑧 − 𝑡 ) ↔ ( ( 𝑥 − 𝑦 ) ≤ ( 𝑧 − 𝑡 ) ∧ ( 𝑥 − 𝑦 ) ≠ ( 𝑧 − 𝑡 ) ) ) )
45 39 44 mpbid ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) ∧ ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑏 = ( 𝑧 − 𝑡 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑐 = ( 𝑢 − 𝑣 ) ) → ( ( 𝑥 − 𝑦 ) ≤ ( 𝑧 − 𝑡 ) ∧ ( 𝑥 − 𝑦 ) ≠ ( 𝑧 − 𝑡 ) ) )
46 45 simpld ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) ∧ ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑏 = ( 𝑧 − 𝑡 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑐 = ( 𝑢 − 𝑣 ) ) → ( 𝑥 − 𝑦 ) ≤ ( 𝑧 − 𝑡 ) )
47 35 simprd ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) ∧ ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑏 = ( 𝑧 − 𝑡 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑐 = ( 𝑢 − 𝑣 ) ) → 𝑏 < 𝑐 )
48 simpr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) ∧ ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑏 = ( 𝑧 − 𝑡 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑐 = ( 𝑢 − 𝑣 ) ) → 𝑐 = ( 𝑢 − 𝑣 ) )
49 47 38 48 3brtr3d ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) ∧ ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑏 = ( 𝑧 − 𝑡 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑐 = ( 𝑢 − 𝑣 ) ) → ( 𝑧 − 𝑡 ) < ( 𝑢 − 𝑣 ) )
50 1 2 3 4 28 6 41 8 43 31 32 ltgov ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) ∧ ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑏 = ( 𝑧 − 𝑡 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑐 = ( 𝑢 − 𝑣 ) ) → ( ( 𝑧 − 𝑡 ) < ( 𝑢 − 𝑣 ) ↔ ( ( 𝑧 − 𝑡 ) ≤ ( 𝑢 − 𝑣 ) ∧ ( 𝑧 − 𝑡 ) ≠ ( 𝑢 − 𝑣 ) ) ) )
51 49 50 mpbid ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) ∧ ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑏 = ( 𝑧 − 𝑡 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑐 = ( 𝑢 − 𝑣 ) ) → ( ( 𝑧 − 𝑡 ) ≤ ( 𝑢 − 𝑣 ) ∧ ( 𝑧 − 𝑡 ) ≠ ( 𝑢 − 𝑣 ) ) )
52 51 simpld ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) ∧ ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑏 = ( 𝑧 − 𝑡 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑐 = ( 𝑢 − 𝑣 ) ) → ( 𝑧 − 𝑡 ) ≤ ( 𝑢 − 𝑣 ) )
53 1 2 3 4 28 29 30 31 32 33 34 46 52 legtrd ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) ∧ ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑏 = ( 𝑧 − 𝑡 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑐 = ( 𝑢 − 𝑣 ) ) → ( 𝑥 − 𝑦 ) ≤ ( 𝑢 − 𝑣 ) )
54 28 adantr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) ∧ ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑏 = ( 𝑧 − 𝑡 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑐 = ( 𝑢 − 𝑣 ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑢 − 𝑣 ) ) → 𝐺 ∈ TarskiG )
55 29 adantr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) ∧ ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑏 = ( 𝑧 − 𝑡 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑐 = ( 𝑢 − 𝑣 ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑢 − 𝑣 ) ) → 𝑥 ∈ 𝑃 )
56 30 adantr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) ∧ ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑏 = ( 𝑧 − 𝑡 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑐 = ( 𝑢 − 𝑣 ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑢 − 𝑣 ) ) → 𝑦 ∈ 𝑃 )
57 31 adantr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) ∧ ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑏 = ( 𝑧 − 𝑡 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑐 = ( 𝑢 − 𝑣 ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑢 − 𝑣 ) ) → 𝑧 ∈ 𝑃 )
58 32 adantr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) ∧ ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑏 = ( 𝑧 − 𝑡 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑐 = ( 𝑢 − 𝑣 ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑢 − 𝑣 ) ) → 𝑡 ∈ 𝑃 )
59 46 adantr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) ∧ ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑏 = ( 𝑧 − 𝑡 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑐 = ( 𝑢 − 𝑣 ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑢 − 𝑣 ) ) → ( 𝑥 − 𝑦 ) ≤ ( 𝑧 − 𝑡 ) )
60 52 adantr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) ∧ ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑏 = ( 𝑧 − 𝑡 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑐 = ( 𝑢 − 𝑣 ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑢 − 𝑣 ) ) → ( 𝑧 − 𝑡 ) ≤ ( 𝑢 − 𝑣 ) )
61 simpr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) ∧ ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑏 = ( 𝑧 − 𝑡 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑐 = ( 𝑢 − 𝑣 ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑢 − 𝑣 ) ) → ( 𝑥 − 𝑦 ) = ( 𝑢 − 𝑣 ) )
62 60 61 breqtrrd ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) ∧ ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑏 = ( 𝑧 − 𝑡 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑐 = ( 𝑢 − 𝑣 ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑢 − 𝑣 ) ) → ( 𝑧 − 𝑡 ) ≤ ( 𝑥 − 𝑦 ) )
63 1 2 3 4 54 55 56 57 58 59 62 legtri3 ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) ∧ ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑏 = ( 𝑧 − 𝑡 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑐 = ( 𝑢 − 𝑣 ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑢 − 𝑣 ) ) → ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) )
64 45 simprd ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) ∧ ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑏 = ( 𝑧 − 𝑡 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑐 = ( 𝑢 − 𝑣 ) ) → ( 𝑥 − 𝑦 ) ≠ ( 𝑧 − 𝑡 ) )
65 64 adantr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) ∧ ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑏 = ( 𝑧 − 𝑡 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑐 = ( 𝑢 − 𝑣 ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑢 − 𝑣 ) ) → ( 𝑥 − 𝑦 ) ≠ ( 𝑧 − 𝑡 ) )
66 65 neneqd ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) ∧ ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑏 = ( 𝑧 − 𝑡 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑐 = ( 𝑢 − 𝑣 ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑢 − 𝑣 ) ) → ¬ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) )
67 63 66 pm2.65da ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) ∧ ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑏 = ( 𝑧 − 𝑡 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑐 = ( 𝑢 − 𝑣 ) ) → ¬ ( 𝑥 − 𝑦 ) = ( 𝑢 − 𝑣 ) )
68 67 neqned ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) ∧ ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑏 = ( 𝑧 − 𝑡 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑐 = ( 𝑢 − 𝑣 ) ) → ( 𝑥 − 𝑦 ) ≠ ( 𝑢 − 𝑣 ) )
69 1 2 3 4 28 6 41 8 43 29 30 ltgov ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) ∧ ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑏 = ( 𝑧 − 𝑡 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑐 = ( 𝑢 − 𝑣 ) ) → ( ( 𝑥 − 𝑦 ) < ( 𝑢 − 𝑣 ) ↔ ( ( 𝑥 − 𝑦 ) ≤ ( 𝑢 − 𝑣 ) ∧ ( 𝑥 − 𝑦 ) ≠ ( 𝑢 − 𝑣 ) ) ) )
70 53 68 69 mpbir2and ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) ∧ ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑏 = ( 𝑧 − 𝑡 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑐 = ( 𝑢 − 𝑣 ) ) → ( 𝑥 − 𝑦 ) < ( 𝑢 − 𝑣 ) )
71 70 37 48 3brtr4d ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) ∧ ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑏 = ( 𝑧 − 𝑡 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑐 = ( 𝑢 − 𝑣 ) ) → 𝑎 < 𝑐 )
72 simp-5r ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) ∧ ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) → ( 𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) )
73 72 simp3d ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) ∧ ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) → 𝑐 ∈ 𝐸 )
74 73 ad3antrrr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) ∧ ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑏 = ( 𝑧 − 𝑡 ) ) → 𝑐 ∈ 𝐸 )
75 1 2 3 4 27 6 40 74 ltgseg ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) ∧ ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑏 = ( 𝑧 − 𝑡 ) ) → ∃ 𝑢 ∈ 𝑃 ∃ 𝑣 ∈ 𝑃 𝑐 = ( 𝑢 − 𝑣 ) )
76 71 75 r19.29vva ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) ∧ ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑏 = ( 𝑧 − 𝑡 ) ) → 𝑎 < 𝑐 )
77 5 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) ∧ ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) → 𝐺 ∈ TarskiG )
78 7 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) ∧ ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) → Fun − )
79 72 simp2d ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) ∧ ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) → 𝑏 ∈ 𝐸 )
80 1 2 3 4 77 6 78 79 ltgseg ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) ∧ ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) → ∃ 𝑧 ∈ 𝑃 ∃ 𝑡 ∈ 𝑃 𝑏 = ( 𝑧 − 𝑡 ) )
81 76 80 r19.29vva ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) ∧ ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) → 𝑎 < 𝑐 )
82 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) ∧ ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ) ) → 𝐺 ∈ TarskiG )
83 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) ∧ ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ) ) → Fun − )
84 simplr1 ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) ∧ ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ) ) → 𝑎 ∈ 𝐸 )
85 1 2 3 4 82 6 83 84 ltgseg ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) ∧ ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ) ) → ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 𝑎 = ( 𝑥 − 𝑦 ) )
86 81 85 r19.29vva ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) ∧ ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ) ) → 𝑎 < 𝑐 )
87 86 ex ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) → ( ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ) → 𝑎 < 𝑐 ) )
88 26 87 ispod ⊢ ( 𝜑 → < Po 𝐸 )
89 5 ad8antr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) ∧ 𝑏 ∈ 𝐸 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑏 = ( 𝑧 − 𝑡 ) ) → 𝐺 ∈ TarskiG )
90 simp-6r ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) ∧ 𝑏 ∈ 𝐸 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑏 = ( 𝑧 − 𝑡 ) ) → 𝑥 ∈ 𝑃 )
91 simp-5r ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) ∧ 𝑏 ∈ 𝐸 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑏 = ( 𝑧 − 𝑡 ) ) → 𝑦 ∈ 𝑃 )
92 simpllr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) ∧ 𝑏 ∈ 𝐸 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑏 = ( 𝑧 − 𝑡 ) ) → 𝑧 ∈ 𝑃 )
93 simplr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) ∧ 𝑏 ∈ 𝐸 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑏 = ( 𝑧 − 𝑡 ) ) → 𝑡 ∈ 𝑃 )
94 1 2 3 4 89 90 91 92 93 legtrid ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) ∧ 𝑏 ∈ 𝐸 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑏 = ( 𝑧 − 𝑡 ) ) → ( ( 𝑥 − 𝑦 ) ≤ ( 𝑧 − 𝑡 ) ∨ ( 𝑧 − 𝑡 ) ≤ ( 𝑥 − 𝑦 ) ) )
95 7 ad8antr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) ∧ 𝑏 ∈ 𝐸 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑏 = ( 𝑧 − 𝑡 ) ) → Fun − )
96 9 ad8antr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) ∧ 𝑏 ∈ 𝐸 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑏 = ( 𝑧 − 𝑡 ) ) → ( 𝑃 × 𝑃 ) ⊆ dom − )
97 1 2 3 4 89 6 95 8 96 90 91 legov3 ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) ∧ 𝑏 ∈ 𝐸 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑏 = ( 𝑧 − 𝑡 ) ) → ( ( 𝑥 − 𝑦 ) ≤ ( 𝑧 − 𝑡 ) ↔ ( ( 𝑥 − 𝑦 ) < ( 𝑧 − 𝑡 ) ∨ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) )
98 1 2 3 4 89 6 95 8 96 92 93 legov3 ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) ∧ 𝑏 ∈ 𝐸 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑏 = ( 𝑧 − 𝑡 ) ) → ( ( 𝑧 − 𝑡 ) ≤ ( 𝑥 − 𝑦 ) ↔ ( ( 𝑧 − 𝑡 ) < ( 𝑥 − 𝑦 ) ∨ ( 𝑧 − 𝑡 ) = ( 𝑥 − 𝑦 ) ) ) )
99 97 98 orbi12d ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) ∧ 𝑏 ∈ 𝐸 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑏 = ( 𝑧 − 𝑡 ) ) → ( ( ( 𝑥 − 𝑦 ) ≤ ( 𝑧 − 𝑡 ) ∨ ( 𝑧 − 𝑡 ) ≤ ( 𝑥 − 𝑦 ) ) ↔ ( ( ( 𝑥 − 𝑦 ) < ( 𝑧 − 𝑡 ) ∨ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ∨ ( ( 𝑧 − 𝑡 ) < ( 𝑥 − 𝑦 ) ∨ ( 𝑧 − 𝑡 ) = ( 𝑥 − 𝑦 ) ) ) ) )
100 94 99 mpbid ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) ∧ 𝑏 ∈ 𝐸 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑏 = ( 𝑧 − 𝑡 ) ) → ( ( ( 𝑥 − 𝑦 ) < ( 𝑧 − 𝑡 ) ∨ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ∨ ( ( 𝑧 − 𝑡 ) < ( 𝑥 − 𝑦 ) ∨ ( 𝑧 − 𝑡 ) = ( 𝑥 − 𝑦 ) ) ) )
101 eqcom ⊢ ( ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ↔ ( 𝑧 − 𝑡 ) = ( 𝑥 − 𝑦 ) )
102 101 orbi2i ⊢ ( ( ( 𝑧 − 𝑡 ) < ( 𝑥 − 𝑦 ) ∨ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ↔ ( ( 𝑧 − 𝑡 ) < ( 𝑥 − 𝑦 ) ∨ ( 𝑧 − 𝑡 ) = ( 𝑥 − 𝑦 ) ) )
103 102 orbi2i ⊢ ( ( ( ( 𝑥 − 𝑦 ) < ( 𝑧 − 𝑡 ) ∨ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ∨ ( ( 𝑧 − 𝑡 ) < ( 𝑥 − 𝑦 ) ∨ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) ↔ ( ( ( 𝑥 − 𝑦 ) < ( 𝑧 − 𝑡 ) ∨ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ∨ ( ( 𝑧 − 𝑡 ) < ( 𝑥 − 𝑦 ) ∨ ( 𝑧 − 𝑡 ) = ( 𝑥 − 𝑦 ) ) ) )
104 df-3or ⊢ ( ( ( 𝑥 − 𝑦 ) < ( 𝑧 − 𝑡 ) ∨ ( 𝑧 − 𝑡 ) < ( 𝑥 − 𝑦 ) ∨ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ↔ ( ( ( 𝑥 − 𝑦 ) < ( 𝑧 − 𝑡 ) ∨ ( 𝑧 − 𝑡 ) < ( 𝑥 − 𝑦 ) ) ∨ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) )
105 3orcomb ⊢ ( ( ( 𝑥 − 𝑦 ) < ( 𝑧 − 𝑡 ) ∨ ( 𝑧 − 𝑡 ) < ( 𝑥 − 𝑦 ) ∨ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ↔ ( ( 𝑥 − 𝑦 ) < ( 𝑧 − 𝑡 ) ∨ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ∨ ( 𝑧 − 𝑡 ) < ( 𝑥 − 𝑦 ) ) )
106 orordir ⊢ ( ( ( ( 𝑥 − 𝑦 ) < ( 𝑧 − 𝑡 ) ∨ ( 𝑧 − 𝑡 ) < ( 𝑥 − 𝑦 ) ) ∨ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ↔ ( ( ( 𝑥 − 𝑦 ) < ( 𝑧 − 𝑡 ) ∨ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ∨ ( ( 𝑧 − 𝑡 ) < ( 𝑥 − 𝑦 ) ∨ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) )
107 104 105 106 3bitr3ri ⊢ ( ( ( ( 𝑥 − 𝑦 ) < ( 𝑧 − 𝑡 ) ∨ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ∨ ( ( 𝑧 − 𝑡 ) < ( 𝑥 − 𝑦 ) ∨ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) ↔ ( ( 𝑥 − 𝑦 ) < ( 𝑧 − 𝑡 ) ∨ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ∨ ( 𝑧 − 𝑡 ) < ( 𝑥 − 𝑦 ) ) )
108 103 107 bitr3i ⊢ ( ( ( ( 𝑥 − 𝑦 ) < ( 𝑧 − 𝑡 ) ∨ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ∨ ( ( 𝑧 − 𝑡 ) < ( 𝑥 − 𝑦 ) ∨ ( 𝑧 − 𝑡 ) = ( 𝑥 − 𝑦 ) ) ) ↔ ( ( 𝑥 − 𝑦 ) < ( 𝑧 − 𝑡 ) ∨ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ∨ ( 𝑧 − 𝑡 ) < ( 𝑥 − 𝑦 ) ) )
109 100 108 sylib ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) ∧ 𝑏 ∈ 𝐸 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑏 = ( 𝑧 − 𝑡 ) ) → ( ( 𝑥 − 𝑦 ) < ( 𝑧 − 𝑡 ) ∨ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ∨ ( 𝑧 − 𝑡 ) < ( 𝑥 − 𝑦 ) ) )
110 simp-4r ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) ∧ 𝑏 ∈ 𝐸 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑏 = ( 𝑧 − 𝑡 ) ) → 𝑎 = ( 𝑥 − 𝑦 ) )
111 simpr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) ∧ 𝑏 ∈ 𝐸 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑏 = ( 𝑧 − 𝑡 ) ) → 𝑏 = ( 𝑧 − 𝑡 ) )
112 110 111 breq12d ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) ∧ 𝑏 ∈ 𝐸 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑏 = ( 𝑧 − 𝑡 ) ) → ( 𝑎 < 𝑏 ↔ ( 𝑥 − 𝑦 ) < ( 𝑧 − 𝑡 ) ) )
113 110 111 eqeq12d ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) ∧ 𝑏 ∈ 𝐸 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑏 = ( 𝑧 − 𝑡 ) ) → ( 𝑎 = 𝑏 ↔ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) )
114 111 110 breq12d ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) ∧ 𝑏 ∈ 𝐸 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑏 = ( 𝑧 − 𝑡 ) ) → ( 𝑏 < 𝑎 ↔ ( 𝑧 − 𝑡 ) < ( 𝑥 − 𝑦 ) ) )
115 112 113 114 3orbi123d ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) ∧ 𝑏 ∈ 𝐸 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑏 = ( 𝑧 − 𝑡 ) ) → ( ( 𝑎 < 𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏 < 𝑎 ) ↔ ( ( 𝑥 − 𝑦 ) < ( 𝑧 − 𝑡 ) ∨ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ∨ ( 𝑧 − 𝑡 ) < ( 𝑥 − 𝑦 ) ) ) )
116 109 115 mpbird ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) ∧ 𝑏 ∈ 𝐸 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑏 = ( 𝑧 − 𝑡 ) ) → ( 𝑎 < 𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏 < 𝑎 ) )
117 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) ∧ 𝑏 ∈ 𝐸 ) → 𝐺 ∈ TarskiG )
118 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) ∧ 𝑏 ∈ 𝐸 ) → Fun − )
119 simpr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) ∧ 𝑏 ∈ 𝐸 ) → 𝑏 ∈ 𝐸 )
120 1 2 3 4 117 6 118 119 ltgseg ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) ∧ 𝑏 ∈ 𝐸 ) → ∃ 𝑧 ∈ 𝑃 ∃ 𝑡 ∈ 𝑃 𝑏 = ( 𝑧 − 𝑡 ) )
121 120 ad3antrrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) ∧ 𝑏 ∈ 𝐸 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) → ∃ 𝑧 ∈ 𝑃 ∃ 𝑡 ∈ 𝑃 𝑏 = ( 𝑧 − 𝑡 ) )
122 116 121 r19.29vva ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) ∧ 𝑏 ∈ 𝐸 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ( 𝑥 − 𝑦 ) ) → ( 𝑎 < 𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏 < 𝑎 ) )
123 25 adantr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) ∧ 𝑏 ∈ 𝐸 ) → ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 𝑎 = ( 𝑥 − 𝑦 ) )
124 122 123 r19.29vva ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) ∧ 𝑏 ∈ 𝐸 ) → ( 𝑎 < 𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏 < 𝑎 ) )
125 124 anasss ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸 ) ) → ( 𝑎 < 𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏 < 𝑎 ) )
126 88 125 issod ⊢ ( 𝜑 → < Or 𝐸 )