# Metamath Proof Explorer

## Theorem axcont

Description: The axiom of continuity. Take two sets of points A and B . If all the points in A come before the points of B on a line, then there is a point separating the two. Axiom A11 of Schwabhauser p. 13. (Contributed by Scott Fenton, 20-Jun-2013)

Ref Expression
Assertion axcont ${⊢}\left({N}\in ℕ\wedge \left({A}\subseteq 𝔼\left({N}\right)\wedge {B}\subseteq 𝔼\left({N}\right)\wedge \exists {a}\in 𝔼\left({N}\right)\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\mathrm{Btwn}⟨{a},{y}⟩\right)\right)\to \exists {b}\in 𝔼\left({N}\right)\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{b}\mathrm{Btwn}⟨{x},{y}⟩$

### Proof

Step Hyp Ref Expression
1 simpr ${⊢}\left({a}\in 𝔼\left({N}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\mathrm{Btwn}⟨{a},{y}⟩\right)\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\mathrm{Btwn}⟨{a},{y}⟩$
2 1 3anim3i ${⊢}\left({A}\subseteq 𝔼\left({N}\right)\wedge {B}\subseteq 𝔼\left({N}\right)\wedge \left({a}\in 𝔼\left({N}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\mathrm{Btwn}⟨{a},{y}⟩\right)\right)\to \left({A}\subseteq 𝔼\left({N}\right)\wedge {B}\subseteq 𝔼\left({N}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\mathrm{Btwn}⟨{a},{y}⟩\right)$
3 2 anim2i ${⊢}\left({N}\in ℕ\wedge \left({A}\subseteq 𝔼\left({N}\right)\wedge {B}\subseteq 𝔼\left({N}\right)\wedge \left({a}\in 𝔼\left({N}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\mathrm{Btwn}⟨{a},{y}⟩\right)\right)\right)\to \left({N}\in ℕ\wedge \left({A}\subseteq 𝔼\left({N}\right)\wedge {B}\subseteq 𝔼\left({N}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\mathrm{Btwn}⟨{a},{y}⟩\right)\right)$
4 simpr3l ${⊢}\left({N}\in ℕ\wedge \left({A}\subseteq 𝔼\left({N}\right)\wedge {B}\subseteq 𝔼\left({N}\right)\wedge \left({a}\in 𝔼\left({N}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\mathrm{Btwn}⟨{a},{y}⟩\right)\right)\right)\to {a}\in 𝔼\left({N}\right)$
5 axcontlem12 ${⊢}\left(\left({N}\in ℕ\wedge \left({A}\subseteq 𝔼\left({N}\right)\wedge {B}\subseteq 𝔼\left({N}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\mathrm{Btwn}⟨{a},{y}⟩\right)\right)\wedge {a}\in 𝔼\left({N}\right)\right)\to \exists {b}\in 𝔼\left({N}\right)\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{b}\mathrm{Btwn}⟨{x},{y}⟩$
6 3 4 5 syl2anc ${⊢}\left({N}\in ℕ\wedge \left({A}\subseteq 𝔼\left({N}\right)\wedge {B}\subseteq 𝔼\left({N}\right)\wedge \left({a}\in 𝔼\left({N}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\mathrm{Btwn}⟨{a},{y}⟩\right)\right)\right)\to \exists {b}\in 𝔼\left({N}\right)\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{b}\mathrm{Btwn}⟨{x},{y}⟩$
7 6 3exp2 ${⊢}{N}\in ℕ\to \left({A}\subseteq 𝔼\left({N}\right)\to \left({B}\subseteq 𝔼\left({N}\right)\to \left(\left({a}\in 𝔼\left({N}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\mathrm{Btwn}⟨{a},{y}⟩\right)\to \exists {b}\in 𝔼\left({N}\right)\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{b}\mathrm{Btwn}⟨{x},{y}⟩\right)\right)\right)$
8 7 com4r ${⊢}\left({a}\in 𝔼\left({N}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\mathrm{Btwn}⟨{a},{y}⟩\right)\to \left({N}\in ℕ\to \left({A}\subseteq 𝔼\left({N}\right)\to \left({B}\subseteq 𝔼\left({N}\right)\to \exists {b}\in 𝔼\left({N}\right)\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{b}\mathrm{Btwn}⟨{x},{y}⟩\right)\right)\right)$
9 8 rexlimiva ${⊢}\exists {a}\in 𝔼\left({N}\right)\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\mathrm{Btwn}⟨{a},{y}⟩\to \left({N}\in ℕ\to \left({A}\subseteq 𝔼\left({N}\right)\to \left({B}\subseteq 𝔼\left({N}\right)\to \exists {b}\in 𝔼\left({N}\right)\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{b}\mathrm{Btwn}⟨{x},{y}⟩\right)\right)\right)$
10 9 com4l ${⊢}{N}\in ℕ\to \left({A}\subseteq 𝔼\left({N}\right)\to \left({B}\subseteq 𝔼\left({N}\right)\to \left(\exists {a}\in 𝔼\left({N}\right)\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\mathrm{Btwn}⟨{a},{y}⟩\to \exists {b}\in 𝔼\left({N}\right)\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{b}\mathrm{Btwn}⟨{x},{y}⟩\right)\right)\right)$
11 10 3imp2 ${⊢}\left({N}\in ℕ\wedge \left({A}\subseteq 𝔼\left({N}\right)\wedge {B}\subseteq 𝔼\left({N}\right)\wedge \exists {a}\in 𝔼\left({N}\right)\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\mathrm{Btwn}⟨{a},{y}⟩\right)\right)\to \exists {b}\in 𝔼\left({N}\right)\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{b}\mathrm{Btwn}⟨{x},{y}⟩$