Metamath Proof Explorer

Theorem segleantisym

Description: Antisymmetry law for segment comparison. Theorem 5.9 of Schwabhauser p. 42. (Contributed by Scott Fenton, 14-Oct-2013)

Ref Expression
Assertion segleantisym ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ⟨ 𝐴 , 𝐵 ⟩ Seg≤ ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Seg≤ ⟨ 𝐴 , 𝐵 ⟩ ) → ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) )

Proof

Step Hyp Ref Expression
1 brsegle ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ Seg≤ ⟨ 𝐶 , 𝐷 ⟩ ↔ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ) )
2 brsegle2 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐶 , 𝐷 ⟩ Seg≤ ⟨ 𝐴 , 𝐵 ⟩ ↔ ∃ 𝑡 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐷 Btwn ⟨ 𝐶 , 𝑡 ⟩ ∧ ⟨ 𝐶 , 𝑡 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) )
3 2 3com23 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐶 , 𝐷 ⟩ Seg≤ ⟨ 𝐴 , 𝐵 ⟩ ↔ ∃ 𝑡 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐷 Btwn ⟨ 𝐶 , 𝑡 ⟩ ∧ ⟨ 𝐶 , 𝑡 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) )
4 1 3 anbi12d ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ⟨ 𝐴 , 𝐵 ⟩ Seg≤ ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Seg≤ ⟨ 𝐴 , 𝐵 ⟩ ) ↔ ( ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ∧ ∃ 𝑡 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐷 Btwn ⟨ 𝐶 , 𝑡 ⟩ ∧ ⟨ 𝐶 , 𝑡 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ) )
5 reeanv ⊢ ( ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑡 ∈ ( 𝔼 ‘ 𝑁 ) ( ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐶 , 𝑡 ⟩ ∧ ⟨ 𝐶 , 𝑡 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ↔ ( ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ∧ ∃ 𝑡 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐷 Btwn ⟨ 𝐶 , 𝑡 ⟩ ∧ ⟨ 𝐶 , 𝑡 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) )
6 4 5 bitr4di ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ⟨ 𝐴 , 𝐵 ⟩ Seg≤ ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Seg≤ ⟨ 𝐴 , 𝐵 ⟩ ) ↔ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑡 ∈ ( 𝔼 ‘ 𝑁 ) ( ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐶 , 𝑡 ⟩ ∧ ⟨ 𝐶 , 𝑡 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ) )
7 simpl1 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑡 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑁 ∈ ℕ )
8 simpl3l ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑡 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) )
9 simprr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑡 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑡 ∈ ( 𝔼 ‘ 𝑁 ) )
10 simprl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑡 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) )
11 simpl3r ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑡 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) )
12 simprll ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑡 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐶 , 𝑡 ⟩ ∧ ⟨ 𝐶 , 𝑡 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ) → 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ )
13 simprrl ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑡 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐶 , 𝑡 ⟩ ∧ ⟨ 𝐶 , 𝑡 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ) → 𝐷 Btwn ⟨ 𝐶 , 𝑡 ⟩ )
14 7 8 10 11 9 12 13 btwnexchand ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑡 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐶 , 𝑡 ⟩ ∧ ⟨ 𝐶 , 𝑡 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ) → 𝑦 Btwn ⟨ 𝐶 , 𝑡 ⟩ )
15 simpl2l ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑡 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
16 simpl2r ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑡 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
17 simprrr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑡 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐶 , 𝑡 ⟩ ∧ ⟨ 𝐶 , 𝑡 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ) → ⟨ 𝐶 , 𝑡 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ )
18 simprlr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑡 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐶 , 𝑡 ⟩ ∧ ⟨ 𝐶 , 𝑡 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ) → ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ )
19 7 8 9 15 16 8 10 17 18 cgrtrand ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑡 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐶 , 𝑡 ⟩ ∧ ⟨ 𝐶 , 𝑡 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ) → ⟨ 𝐶 , 𝑡 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ )
20 7 8 9 10 14 19 endofsegidand ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑡 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐶 , 𝑡 ⟩ ∧ ⟨ 𝐶 , 𝑡 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ) → 𝑡 = 𝑦 )
21 opeq2 ⊢ ( 𝑡 = 𝑦 → ⟨ 𝐶 , 𝑡 ⟩ = ⟨ 𝐶 , 𝑦 ⟩ )
22 21 breq2d ⊢ ( 𝑡 = 𝑦 → ( 𝐷 Btwn ⟨ 𝐶 , 𝑡 ⟩ ↔ 𝐷 Btwn ⟨ 𝐶 , 𝑦 ⟩ ) )
23 21 breq1d ⊢ ( 𝑡 = 𝑦 → ( ⟨ 𝐶 , 𝑡 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ↔ ⟨ 𝐶 , 𝑦 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) )
24 22 23 anbi12d ⊢ ( 𝑡 = 𝑦 → ( ( 𝐷 Btwn ⟨ 𝐶 , 𝑡 ⟩ ∧ ⟨ 𝐶 , 𝑡 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ↔ ( 𝐷 Btwn ⟨ 𝐶 , 𝑦 ⟩ ∧ ⟨ 𝐶 , 𝑦 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) )
25 24 anbi2d ⊢ ( 𝑡 = 𝑦 → ( ( ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐶 , 𝑡 ⟩ ∧ ⟨ 𝐶 , 𝑡 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ↔ ( ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐶 , 𝑦 ⟩ ∧ ⟨ 𝐶 , 𝑦 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ) )
26 25 anbi2d ⊢ ( 𝑡 = 𝑦 → ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑡 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐶 , 𝑡 ⟩ ∧ ⟨ 𝐶 , 𝑡 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ) ↔ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑡 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐶 , 𝑦 ⟩ ∧ ⟨ 𝐶 , 𝑦 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ) ) )
27 simprrl ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑡 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐶 , 𝑦 ⟩ ∧ ⟨ 𝐶 , 𝑦 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ) → 𝐷 Btwn ⟨ 𝐶 , 𝑦 ⟩ )
28 7 11 8 10 27 btwncomand ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑡 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐶 , 𝑦 ⟩ ∧ ⟨ 𝐶 , 𝑦 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ) → 𝐷 Btwn ⟨ 𝑦 , 𝐶 ⟩ )
29 simprll ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑡 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐶 , 𝑦 ⟩ ∧ ⟨ 𝐶 , 𝑦 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ) → 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ )
30 7 10 8 11 29 btwncomand ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑡 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐶 , 𝑦 ⟩ ∧ ⟨ 𝐶 , 𝑦 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ) → 𝑦 Btwn ⟨ 𝐷 , 𝐶 ⟩ )
31 btwnswapid ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐷 Btwn ⟨ 𝑦 , 𝐶 ⟩ ∧ 𝑦 Btwn ⟨ 𝐷 , 𝐶 ⟩ ) → 𝐷 = 𝑦 ) )
32 7 11 10 8 31 syl13anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑡 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐷 Btwn ⟨ 𝑦 , 𝐶 ⟩ ∧ 𝑦 Btwn ⟨ 𝐷 , 𝐶 ⟩ ) → 𝐷 = 𝑦 ) )
33 32 adantr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑡 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐶 , 𝑦 ⟩ ∧ ⟨ 𝐶 , 𝑦 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ) → ( ( 𝐷 Btwn ⟨ 𝑦 , 𝐶 ⟩ ∧ 𝑦 Btwn ⟨ 𝐷 , 𝐶 ⟩ ) → 𝐷 = 𝑦 ) )
34 28 30 33 mp2and ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑡 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐶 , 𝑦 ⟩ ∧ ⟨ 𝐶 , 𝑦 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ) → 𝐷 = 𝑦 )
35 simprlr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑡 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐶 , 𝑦 ⟩ ∧ ⟨ 𝐶 , 𝑦 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ) → ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ )
36 opeq2 ⊢ ( 𝐷 = 𝑦 → ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝐶 , 𝑦 ⟩ )
37 36 breq2d ⊢ ( 𝐷 = 𝑦 → ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ↔ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) )
38 35 37 syl5ibrcom ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑡 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐶 , 𝑦 ⟩ ∧ ⟨ 𝐶 , 𝑦 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ) → ( 𝐷 = 𝑦 → ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) )
39 34 38 mpd ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑡 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐶 , 𝑦 ⟩ ∧ ⟨ 𝐶 , 𝑦 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ) → ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ )
40 26 39 syl6bi ⊢ ( 𝑡 = 𝑦 → ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑡 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐶 , 𝑡 ⟩ ∧ ⟨ 𝐶 , 𝑡 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ) → ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) )
41 20 40 mpcom ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑡 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐶 , 𝑡 ⟩ ∧ ⟨ 𝐶 , 𝑡 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ) → ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ )
42 41 exp31 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑡 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐶 , 𝑡 ⟩ ∧ ⟨ 𝐶 , 𝑡 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) → ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) )
43 42 rexlimdvv ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑡 ∈ ( 𝔼 ‘ 𝑁 ) ( ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐶 , 𝑡 ⟩ ∧ ⟨ 𝐶 , 𝑡 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) → ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) )
44 6 43 sylbid ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ⟨ 𝐴 , 𝐵 ⟩ Seg≤ ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Seg≤ ⟨ 𝐴 , 𝐵 ⟩ ) → ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) )