Metamath Proof Explorer

Theorem btwntriv2

Description: Betweenness always holds for the second endpoint. Theorem 3.1 of Schwabhauser p. 30. (Contributed by Scott Fenton, 12-Jun-2013)

Ref Expression
Assertion btwntriv2 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N→BBtwnAB

Proof

Step Hyp Ref Expression
1 simp1 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N→N∈ℕ
2 simp2 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N→A∈𝔼⁡N
3 simp3 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N→B∈𝔼⁡N
4 axsegcon ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧B∈𝔼⁡N∧B∈𝔼⁡N→∃x∈𝔼⁡NBBtwnAx∧BxCgrBB
5 1 2 3 3 3 4 syl122anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N→∃x∈𝔼⁡NBBtwnAx∧BxCgrBB
6 simpl1 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧x∈𝔼⁡N→N∈ℕ
7 simpl3 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧x∈𝔼⁡N→B∈𝔼⁡N
8 simpr ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧x∈𝔼⁡N→x∈𝔼⁡N
9 axcgrid ⊢N∈ℕ∧B∈𝔼⁡N∧x∈𝔼⁡N∧B∈𝔼⁡N→BxCgrBB→B=x
10 6 7 8 7 9 syl13anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧x∈𝔼⁡N→BxCgrBB→B=x
11 opeq2 ⊢B=x→AB=Ax
12 11 breq2d ⊢B=x→BBtwnAB↔BBtwnAx
13 12 biimprd ⊢B=x→BBtwnAx→BBtwnAB
14 10 13 syl6 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧x∈𝔼⁡N→BxCgrBB→BBtwnAx→BBtwnAB
15 14 impd ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧x∈𝔼⁡N→BxCgrBB∧BBtwnAx→BBtwnAB
16 15 ancomsd ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧x∈𝔼⁡N→BBtwnAx∧BxCgrBB→BBtwnAB
17 16 rexlimdva ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N→∃x∈𝔼⁡NBBtwnAx∧BxCgrBB→BBtwnAB
18 5 17 mpd ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N→BBtwnAB