Theorem seglerflx

Description: Segment comparison is reflexive. Theorem 5.7 of Schwabhauser p. 42. (Contributed by Scott Fenton, 11-Oct-2013)

	Ref	Expression
Assertion	seglerflx	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → ⟨ 𝐴 , 𝐵 ⟩ Seg≤ ⟨ 𝐴 , 𝐵 ⟩ )

Proof

Step	Hyp	Ref	Expression
1		simp3	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
2		btwntriv2	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐵 Btwn ⟨ 𝐴 , 𝐵 ⟩ )
3		cgrrflx	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ )
4		breq1	⊢ ( 𝑦 = 𝐵 → ( 𝑦 Btwn ⟨ 𝐴 , 𝐵 ⟩ ↔ 𝐵 Btwn ⟨ 𝐴 , 𝐵 ⟩ ) )
5		opeq2	⊢ ( 𝑦 = 𝐵 → ⟨ 𝐴 , 𝑦 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ )
6	5	breq2d	⊢ ( 𝑦 = 𝐵 → ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐴 , 𝑦 ⟩ ↔ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) )
7	4 6	anbi12d	⊢ ( 𝑦 = 𝐵 → ( ( 𝑦 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐴 , 𝑦 ⟩ ) ↔ ( 𝐵 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) )
8	7	rspcev	⊢ ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) → ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐴 , 𝑦 ⟩ ) )
9	1 2 3 8	syl12anc	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐴 , 𝑦 ⟩ ) )
10		simp1	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑁 ∈ ℕ )
11		simp2	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
12		brsegle	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ Seg≤ ⟨ 𝐴 , 𝐵 ⟩ ↔ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐴 , 𝑦 ⟩ ) ) )
13	10 11 1 11 1 12	syl122anc	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ Seg≤ ⟨ 𝐴 , 𝐵 ⟩ ↔ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐴 , 𝑦 ⟩ ) ) )
14	9 13	mpbird	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → ⟨ 𝐴 , 𝐵 ⟩ Seg≤ ⟨ 𝐴 , 𝐵 ⟩ )