Metamath Proof Explorer

Theorem segletr

Description: Segment less than is transitive. Theorem 5.8 of Schwabhauser p. 42. (Contributed by Scott Fenton, 11-Oct-2013)

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

Proof

Step Hyp Ref Expression
1 simprll ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ∧ ( 𝑧 Btwn ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝑧 ⟩ ) ) ) → 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ )
2 simprrr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ∧ ( 𝑧 Btwn ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝑧 ⟩ ) ) ) → ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝑧 ⟩ )
3 1 2 jca ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ∧ ( 𝑧 Btwn ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝑧 ⟩ ) ) ) → ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝑧 ⟩ ) )
4 simpl1 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑁 ∈ ℕ )
5 simpl23 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) )
6 simprl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) )
7 simpl31 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) )
8 simpl32 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) )
9 simprr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) )
10 cgrxfr ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝑧 ⟩ ) → ∃ 𝑤 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑤 Btwn ⟨ 𝐸 , 𝑧 ⟩ ∧ ⟨ 𝐶 , ⟨ 𝑦 , 𝐷 ⟩ ⟩ Cgr3 ⟨ 𝐸 , ⟨ 𝑤 , 𝑧 ⟩ ⟩ ) ) )
11 4 5 6 7 8 9 10 syl132anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝑧 ⟩ ) → ∃ 𝑤 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑤 Btwn ⟨ 𝐸 , 𝑧 ⟩ ∧ ⟨ 𝐶 , ⟨ 𝑦 , 𝐷 ⟩ ⟩ Cgr3 ⟨ 𝐸 , ⟨ 𝑤 , 𝑧 ⟩ ⟩ ) ) )
12 11 adantr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ∧ ( 𝑧 Btwn ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝑧 ⟩ ) ) ) → ( ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝑧 ⟩ ) → ∃ 𝑤 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑤 Btwn ⟨ 𝐸 , 𝑧 ⟩ ∧ ⟨ 𝐶 , ⟨ 𝑦 , 𝐷 ⟩ ⟩ Cgr3 ⟨ 𝐸 , ⟨ 𝑤 , 𝑧 ⟩ ⟩ ) ) )
13 3 12 mpd ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ∧ ( 𝑧 Btwn ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝑧 ⟩ ) ) ) → ∃ 𝑤 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑤 Btwn ⟨ 𝐸 , 𝑧 ⟩ ∧ ⟨ 𝐶 , ⟨ 𝑦 , 𝐷 ⟩ ⟩ Cgr3 ⟨ 𝐸 , ⟨ 𝑤 , 𝑧 ⟩ ⟩ ) )
14 anass ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑤 ∈ ( 𝔼 ‘ 𝑁 ) ) ↔ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑤 ∈ ( 𝔼 ‘ 𝑁 ) ) ) )
15 df-3an ⊢ ( ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑤 ∈ ( 𝔼 ‘ 𝑁 ) ) ↔ ( ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑤 ∈ ( 𝔼 ‘ 𝑁 ) ) )
16 15 anbi2i ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑤 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ↔ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑤 ∈ ( 𝔼 ‘ 𝑁 ) ) ) )
17 14 16 bitr4i ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑤 ∈ ( 𝔼 ‘ 𝑁 ) ) ↔ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑤 ∈ ( 𝔼 ‘ 𝑁 ) ) ) )
18 simpl1 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑤 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑁 ∈ ℕ )
19 simpl23 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑤 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) )
20 simpr1 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑤 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) )
21 simpl31 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑤 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) )
22 simpl32 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑤 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) )
23 simpr3 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑤 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑤 ∈ ( 𝔼 ‘ 𝑁 ) )
24 simpr2 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑤 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) )
25 brcgr3 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑤 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐶 , ⟨ 𝑦 , 𝐷 ⟩ ⟩ Cgr3 ⟨ 𝐸 , ⟨ 𝑤 , 𝑧 ⟩ ⟩ ↔ ( ⟨ 𝐶 , 𝑦 ⟩ Cgr ⟨ 𝐸 , 𝑤 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝑧 ⟩ ∧ ⟨ 𝑦 , 𝐷 ⟩ Cgr ⟨ 𝑤 , 𝑧 ⟩ ) ) )
26 18 19 20 21 22 23 24 25 syl133anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑤 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐶 , ⟨ 𝑦 , 𝐷 ⟩ ⟩ Cgr3 ⟨ 𝐸 , ⟨ 𝑤 , 𝑧 ⟩ ⟩ ↔ ( ⟨ 𝐶 , 𝑦 ⟩ Cgr ⟨ 𝐸 , 𝑤 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝑧 ⟩ ∧ ⟨ 𝑦 , 𝐷 ⟩ Cgr ⟨ 𝑤 , 𝑧 ⟩ ) ) )
27 26 anbi2d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑤 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝑤 Btwn ⟨ 𝐸 , 𝑧 ⟩ ∧ ⟨ 𝐶 , ⟨ 𝑦 , 𝐷 ⟩ ⟩ Cgr3 ⟨ 𝐸 , ⟨ 𝑤 , 𝑧 ⟩ ⟩ ) ↔ ( 𝑤 Btwn ⟨ 𝐸 , 𝑧 ⟩ ∧ ( ⟨ 𝐶 , 𝑦 ⟩ Cgr ⟨ 𝐸 , 𝑤 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝑧 ⟩ ∧ ⟨ 𝑦 , 𝐷 ⟩ Cgr ⟨ 𝑤 , 𝑧 ⟩ ) ) ) )
28 27 adantr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑤 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ∧ ( 𝑧 Btwn ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝑧 ⟩ ) ) ) → ( ( 𝑤 Btwn ⟨ 𝐸 , 𝑧 ⟩ ∧ ⟨ 𝐶 , ⟨ 𝑦 , 𝐷 ⟩ ⟩ Cgr3 ⟨ 𝐸 , ⟨ 𝑤 , 𝑧 ⟩ ⟩ ) ↔ ( 𝑤 Btwn ⟨ 𝐸 , 𝑧 ⟩ ∧ ( ⟨ 𝐶 , 𝑦 ⟩ Cgr ⟨ 𝐸 , 𝑤 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝑧 ⟩ ∧ ⟨ 𝑦 , 𝐷 ⟩ Cgr ⟨ 𝑤 , 𝑧 ⟩ ) ) ) )
29 df-3an ⊢ ( ( ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ∧ ( 𝑧 Btwn ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝑧 ⟩ ) ∧ ( 𝑤 Btwn ⟨ 𝐸 , 𝑧 ⟩ ∧ ( ⟨ 𝐶 , 𝑦 ⟩ Cgr ⟨ 𝐸 , 𝑤 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝑧 ⟩ ∧ ⟨ 𝑦 , 𝐷 ⟩ Cgr ⟨ 𝑤 , 𝑧 ⟩ ) ) ) ↔ ( ( ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ∧ ( 𝑧 Btwn ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝑧 ⟩ ) ) ∧ ( 𝑤 Btwn ⟨ 𝐸 , 𝑧 ⟩ ∧ ( ⟨ 𝐶 , 𝑦 ⟩ Cgr ⟨ 𝐸 , 𝑤 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝑧 ⟩ ∧ ⟨ 𝑦 , 𝐷 ⟩ Cgr ⟨ 𝑤 , 𝑧 ⟩ ) ) ) )
30 simpl33 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑤 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) )
31 simpr3l ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑤 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ∧ ( 𝑧 Btwn ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝑧 ⟩ ) ∧ ( 𝑤 Btwn ⟨ 𝐸 , 𝑧 ⟩ ∧ ( ⟨ 𝐶 , 𝑦 ⟩ Cgr ⟨ 𝐸 , 𝑤 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝑧 ⟩ ∧ ⟨ 𝑦 , 𝐷 ⟩ Cgr ⟨ 𝑤 , 𝑧 ⟩ ) ) ) ) → 𝑤 Btwn ⟨ 𝐸 , 𝑧 ⟩ )
32 simpr2l ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑤 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ∧ ( 𝑧 Btwn ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝑧 ⟩ ) ∧ ( 𝑤 Btwn ⟨ 𝐸 , 𝑧 ⟩ ∧ ( ⟨ 𝐶 , 𝑦 ⟩ Cgr ⟨ 𝐸 , 𝑤 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝑧 ⟩ ∧ ⟨ 𝑦 , 𝐷 ⟩ Cgr ⟨ 𝑤 , 𝑧 ⟩ ) ) ) ) → 𝑧 Btwn ⟨ 𝐸 , 𝐹 ⟩ )
33 18 22 23 24 30 31 32 btwnexchand ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑤 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ∧ ( 𝑧 Btwn ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝑧 ⟩ ) ∧ ( 𝑤 Btwn ⟨ 𝐸 , 𝑧 ⟩ ∧ ( ⟨ 𝐶 , 𝑦 ⟩ Cgr ⟨ 𝐸 , 𝑤 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝑧 ⟩ ∧ ⟨ 𝑦 , 𝐷 ⟩ Cgr ⟨ 𝑤 , 𝑧 ⟩ ) ) ) ) → 𝑤 Btwn ⟨ 𝐸 , 𝐹 ⟩ )
34 simpl21 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑤 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
35 simpl22 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑤 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
36 simpr1r ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑤 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ∧ ( 𝑧 Btwn ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝑧 ⟩ ) ∧ ( 𝑤 Btwn ⟨ 𝐸 , 𝑧 ⟩ ∧ ( ⟨ 𝐶 , 𝑦 ⟩ Cgr ⟨ 𝐸 , 𝑤 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝑧 ⟩ ∧ ⟨ 𝑦 , 𝐷 ⟩ Cgr ⟨ 𝑤 , 𝑧 ⟩ ) ) ) ) → ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ )
37 simp3r1 ⊢ ( ( ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ∧ ( 𝑧 Btwn ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝑧 ⟩ ) ∧ ( 𝑤 Btwn ⟨ 𝐸 , 𝑧 ⟩ ∧ ( ⟨ 𝐶 , 𝑦 ⟩ Cgr ⟨ 𝐸 , 𝑤 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝑧 ⟩ ∧ ⟨ 𝑦 , 𝐷 ⟩ Cgr ⟨ 𝑤 , 𝑧 ⟩ ) ) ) → ⟨ 𝐶 , 𝑦 ⟩ Cgr ⟨ 𝐸 , 𝑤 ⟩ )
38 37 adantl ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑤 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ∧ ( 𝑧 Btwn ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝑧 ⟩ ) ∧ ( 𝑤 Btwn ⟨ 𝐸 , 𝑧 ⟩ ∧ ( ⟨ 𝐶 , 𝑦 ⟩ Cgr ⟨ 𝐸 , 𝑤 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝑧 ⟩ ∧ ⟨ 𝑦 , 𝐷 ⟩ Cgr ⟨ 𝑤 , 𝑧 ⟩ ) ) ) ) → ⟨ 𝐶 , 𝑦 ⟩ Cgr ⟨ 𝐸 , 𝑤 ⟩ )
39 18 34 35 19 20 22 23 36 38 cgrtrand ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑤 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ∧ ( 𝑧 Btwn ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝑧 ⟩ ) ∧ ( 𝑤 Btwn ⟨ 𝐸 , 𝑧 ⟩ ∧ ( ⟨ 𝐶 , 𝑦 ⟩ Cgr ⟨ 𝐸 , 𝑤 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝑧 ⟩ ∧ ⟨ 𝑦 , 𝐷 ⟩ Cgr ⟨ 𝑤 , 𝑧 ⟩ ) ) ) ) → ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐸 , 𝑤 ⟩ )
40 33 39 jca ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑤 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ∧ ( 𝑧 Btwn ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝑧 ⟩ ) ∧ ( 𝑤 Btwn ⟨ 𝐸 , 𝑧 ⟩ ∧ ( ⟨ 𝐶 , 𝑦 ⟩ Cgr ⟨ 𝐸 , 𝑤 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝑧 ⟩ ∧ ⟨ 𝑦 , 𝐷 ⟩ Cgr ⟨ 𝑤 , 𝑧 ⟩ ) ) ) ) → ( 𝑤 Btwn ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐸 , 𝑤 ⟩ ) )
41 29 40 sylan2br ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑤 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ∧ ( 𝑧 Btwn ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝑧 ⟩ ) ) ∧ ( 𝑤 Btwn ⟨ 𝐸 , 𝑧 ⟩ ∧ ( ⟨ 𝐶 , 𝑦 ⟩ Cgr ⟨ 𝐸 , 𝑤 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝑧 ⟩ ∧ ⟨ 𝑦 , 𝐷 ⟩ Cgr ⟨ 𝑤 , 𝑧 ⟩ ) ) ) ) → ( 𝑤 Btwn ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐸 , 𝑤 ⟩ ) )
42 41 expr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑤 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ∧ ( 𝑧 Btwn ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝑧 ⟩ ) ) ) → ( ( 𝑤 Btwn ⟨ 𝐸 , 𝑧 ⟩ ∧ ( ⟨ 𝐶 , 𝑦 ⟩ Cgr ⟨ 𝐸 , 𝑤 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝑧 ⟩ ∧ ⟨ 𝑦 , 𝐷 ⟩ Cgr ⟨ 𝑤 , 𝑧 ⟩ ) ) → ( 𝑤 Btwn ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐸 , 𝑤 ⟩ ) ) )
43 28 42 sylbid ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑤 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ∧ ( 𝑧 Btwn ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝑧 ⟩ ) ) ) → ( ( 𝑤 Btwn ⟨ 𝐸 , 𝑧 ⟩ ∧ ⟨ 𝐶 , ⟨ 𝑦 , 𝐷 ⟩ ⟩ Cgr3 ⟨ 𝐸 , ⟨ 𝑤 , 𝑧 ⟩ ⟩ ) → ( 𝑤 Btwn ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐸 , 𝑤 ⟩ ) ) )
44 17 43 sylanb ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑤 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ∧ ( 𝑧 Btwn ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝑧 ⟩ ) ) ) → ( ( 𝑤 Btwn ⟨ 𝐸 , 𝑧 ⟩ ∧ ⟨ 𝐶 , ⟨ 𝑦 , 𝐷 ⟩ ⟩ Cgr3 ⟨ 𝐸 , ⟨ 𝑤 , 𝑧 ⟩ ⟩ ) → ( 𝑤 Btwn ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐸 , 𝑤 ⟩ ) ) )
45 44 an32s ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ∧ ( 𝑧 Btwn ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝑧 ⟩ ) ) ) ∧ 𝑤 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( 𝑤 Btwn ⟨ 𝐸 , 𝑧 ⟩ ∧ ⟨ 𝐶 , ⟨ 𝑦 , 𝐷 ⟩ ⟩ Cgr3 ⟨ 𝐸 , ⟨ 𝑤 , 𝑧 ⟩ ⟩ ) → ( 𝑤 Btwn ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐸 , 𝑤 ⟩ ) ) )
46 45 reximdva ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ∧ ( 𝑧 Btwn ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝑧 ⟩ ) ) ) → ( ∃ 𝑤 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑤 Btwn ⟨ 𝐸 , 𝑧 ⟩ ∧ ⟨ 𝐶 , ⟨ 𝑦 , 𝐷 ⟩ ⟩ Cgr3 ⟨ 𝐸 , ⟨ 𝑤 , 𝑧 ⟩ ⟩ ) → ∃ 𝑤 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑤 Btwn ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐸 , 𝑤 ⟩ ) ) )
47 13 46 mpd ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ∧ ( 𝑧 Btwn ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝑧 ⟩ ) ) ) → ∃ 𝑤 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑤 Btwn ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐸 , 𝑤 ⟩ ) )
48 47 exp31 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ∧ ( 𝑧 Btwn ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝑧 ⟩ ) ) → ∃ 𝑤 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑤 Btwn ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐸 , 𝑤 ⟩ ) ) ) )
49 48 rexlimdvv ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ( ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ∧ ( 𝑧 Btwn ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝑧 ⟩ ) ) → ∃ 𝑤 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑤 Btwn ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐸 , 𝑤 ⟩ ) ) )
50 simp1 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑁 ∈ ℕ )
51 simp21 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
52 simp22 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
53 simp23 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) )
54 simp31 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) )
55 brsegle ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ Seg≤ ⟨ 𝐶 , 𝐷 ⟩ ↔ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ) )
56 50 51 52 53 54 55 syl122anc ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ Seg≤ ⟨ 𝐶 , 𝐷 ⟩ ↔ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ) )
57 simp32 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) )
58 simp33 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) )
59 brsegle ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐶 , 𝐷 ⟩ Seg≤ ⟨ 𝐸 , 𝐹 ⟩ ↔ ∃ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑧 Btwn ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝑧 ⟩ ) ) )
60 50 53 54 57 58 59 syl122anc ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐶 , 𝐷 ⟩ Seg≤ ⟨ 𝐸 , 𝐹 ⟩ ↔ ∃ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑧 Btwn ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝑧 ⟩ ) ) )
61 56 60 anbi12d ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ⟨ 𝐴 , 𝐵 ⟩ Seg≤ ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Seg≤ ⟨ 𝐸 , 𝐹 ⟩ ) ↔ ( ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ∧ ∃ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑧 Btwn ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝑧 ⟩ ) ) ) )
62 reeanv ⊢ ( ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ( ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ∧ ( 𝑧 Btwn ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝑧 ⟩ ) ) ↔ ( ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ∧ ∃ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑧 Btwn ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝑧 ⟩ ) ) )
63 61 62 bitr4di ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ⟨ 𝐴 , 𝐵 ⟩ Seg≤ ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Seg≤ ⟨ 𝐸 , 𝐹 ⟩ ) ↔ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ( ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ∧ ( 𝑧 Btwn ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝑧 ⟩ ) ) ) )
64 brsegle ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ Seg≤ ⟨ 𝐸 , 𝐹 ⟩ ↔ ∃ 𝑤 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑤 Btwn ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐸 , 𝑤 ⟩ ) ) )
65 50 51 52 57 58 64 syl122anc ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ Seg≤ ⟨ 𝐸 , 𝐹 ⟩ ↔ ∃ 𝑤 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑤 Btwn ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐸 , 𝑤 ⟩ ) ) )
66 49 63 65 3imtr4d ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ⟨ 𝐴 , 𝐵 ⟩ Seg≤ ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Seg≤ ⟨ 𝐸 , 𝐹 ⟩ ) → ⟨ 𝐴 , 𝐵 ⟩ Seg≤ ⟨ 𝐸 , 𝐹 ⟩ ) )