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_≤ ⟨ 𝐸 , 𝐹 ⟩ ) )

Metamath Proof Explorer

Theorem segletr

Proof