Metamath Proof Explorer

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	$⊢ (N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \to ⟨A, B⟩ {Seg}_{\leq} ⟨A, B⟩$

Proof

Step	Hyp	Ref	Expression
1		simp3	$⊢ (N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \to B \in 𝔼 (N)$
2		btwntriv2	$⊢ (N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \to B Btwn ⟨A, B⟩$
3		cgrrflx	$⊢ (N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \to ⟨A, B⟩ Cgr ⟨A, B⟩$
4		breq1	$⊢ y = B \to (y Btwn ⟨A, B⟩ \leftrightarrow B Btwn ⟨A, B⟩)$
5		opeq2	$⊢ y = B \to ⟨A, y⟩ = ⟨A, B⟩$
6	5	breq2d	$⊢ y = B \to (⟨A, B⟩ Cgr ⟨A, y⟩ \leftrightarrow ⟨A, B⟩ Cgr ⟨A, B⟩)$
7	4 6	anbi12d	$⊢ y = B \to ((y Btwn ⟨A, B⟩ \land ⟨A, B⟩ Cgr ⟨A, y⟩) \leftrightarrow (B Btwn ⟨A, B⟩ \land ⟨A, B⟩ Cgr ⟨A, B⟩))$
8	7	rspcev	$⊢ (B \in 𝔼 (N) \land (B Btwn ⟨A, B⟩ \land ⟨A, B⟩ Cgr ⟨A, B⟩)) \to \exists y \in 𝔼 (N) (y Btwn ⟨A, B⟩ \land ⟨A, B⟩ Cgr ⟨A, y⟩)$
9	1 2 3 8	syl12anc	$⊢ (N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \to \exists y \in 𝔼 (N) (y Btwn ⟨A, B⟩ \land ⟨A, B⟩ Cgr ⟨A, y⟩)$
10		simp1	$⊢ (N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \to N \in ℕ$
11		simp2	$⊢ (N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \to A \in 𝔼 (N)$
12		brsegle	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (A \in 𝔼 (N) \land B \in 𝔼 (N))) \to (⟨A, B⟩ {Seg}_{\leq} ⟨A, B⟩ \leftrightarrow \exists y \in 𝔼 (N) (y Btwn ⟨A, B⟩ \land ⟨A, B⟩ Cgr ⟨A, y⟩))$
13	10 11 1 11 1 12	syl122anc	$⊢ (N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \to (⟨A, B⟩ {Seg}_{\leq} ⟨A, B⟩ \leftrightarrow \exists y \in 𝔼 (N) (y Btwn ⟨A, B⟩ \land ⟨A, B⟩ Cgr ⟨A, y⟩))$
14	9 13	mpbird	$⊢ (N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \to ⟨A, B⟩ {Seg}_{\leq} ⟨A, B⟩$