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 ⊢ N ∈ ℕ ∧ A ⊆ 𝔼 ⁡ N ∧ B ⊆ 𝔼 ⁡ N ∧ ∃ a ∈ 𝔼 ⁡ N ∀ x ∈ A ∀ y ∈ B x Btwn a y → ∃ b ∈ 𝔼 ⁡ N ∀ x ∈ A ∀ y ∈ B b Btwn x y

Proof

Step Hyp Ref Expression
1 simpr ⊢ a ∈ 𝔼 ⁡ N ∧ ∀ x ∈ A ∀ y ∈ B x Btwn a y → ∀ x ∈ A ∀ y ∈ B x Btwn a y
2 1 3anim3i ⊢ A ⊆ 𝔼 ⁡ N ∧ B ⊆ 𝔼 ⁡ N ∧ a ∈ 𝔼 ⁡ N ∧ ∀ x ∈ A ∀ y ∈ B x Btwn a y → A ⊆ 𝔼 ⁡ N ∧ B ⊆ 𝔼 ⁡ N ∧ ∀ x ∈ A ∀ y ∈ B x Btwn a y
3 2 anim2i ⊢ N ∈ ℕ ∧ A ⊆ 𝔼 ⁡ N ∧ B ⊆ 𝔼 ⁡ N ∧ a ∈ 𝔼 ⁡ N ∧ ∀ x ∈ A ∀ y ∈ B x Btwn a y → N ∈ ℕ ∧ A ⊆ 𝔼 ⁡ N ∧ B ⊆ 𝔼 ⁡ N ∧ ∀ x ∈ A ∀ y ∈ B x Btwn a y
4 simpr3l ⊢ N ∈ ℕ ∧ A ⊆ 𝔼 ⁡ N ∧ B ⊆ 𝔼 ⁡ N ∧ a ∈ 𝔼 ⁡ N ∧ ∀ x ∈ A ∀ y ∈ B x Btwn a y → a ∈ 𝔼 ⁡ N
5 axcontlem12 ⊢ N ∈ ℕ ∧ A ⊆ 𝔼 ⁡ N ∧ B ⊆ 𝔼 ⁡ N ∧ ∀ x ∈ A ∀ y ∈ B x Btwn a y ∧ a ∈ 𝔼 ⁡ N → ∃ b ∈ 𝔼 ⁡ N ∀ x ∈ A ∀ y ∈ B b Btwn x y
6 3 4 5 syl2anc ⊢ N ∈ ℕ ∧ A ⊆ 𝔼 ⁡ N ∧ B ⊆ 𝔼 ⁡ N ∧ a ∈ 𝔼 ⁡ N ∧ ∀ x ∈ A ∀ y ∈ B x Btwn a y → ∃ b ∈ 𝔼 ⁡ N ∀ x ∈ A ∀ y ∈ B b Btwn x y
7 6 3exp2 ⊢ N ∈ ℕ → A ⊆ 𝔼 ⁡ N → B ⊆ 𝔼 ⁡ N → a ∈ 𝔼 ⁡ N ∧ ∀ x ∈ A ∀ y ∈ B x Btwn a y → ∃ b ∈ 𝔼 ⁡ N ∀ x ∈ A ∀ y ∈ B b Btwn x y
8 7 com4r ⊢ a ∈ 𝔼 ⁡ N ∧ ∀ x ∈ A ∀ y ∈ B x Btwn a y → N ∈ ℕ → A ⊆ 𝔼 ⁡ N → B ⊆ 𝔼 ⁡ N → ∃ b ∈ 𝔼 ⁡ N ∀ x ∈ A ∀ y ∈ B b Btwn x y
9 8 rexlimiva ⊢ ∃ a ∈ 𝔼 ⁡ N ∀ x ∈ A ∀ y ∈ B x Btwn a y → N ∈ ℕ → A ⊆ 𝔼 ⁡ N → B ⊆ 𝔼 ⁡ N → ∃ b ∈ 𝔼 ⁡ N ∀ x ∈ A ∀ y ∈ B b Btwn x y
10 9 com4l ⊢ N ∈ ℕ → A ⊆ 𝔼 ⁡ N → B ⊆ 𝔼 ⁡ N → ∃ a ∈ 𝔼 ⁡ N ∀ x ∈ A ∀ y ∈ B x Btwn a y → ∃ b ∈ 𝔼 ⁡ N ∀ x ∈ A ∀ y ∈ B b Btwn x y
11 10 3imp2 ⊢ N ∈ ℕ ∧ A ⊆ 𝔼 ⁡ N ∧ B ⊆ 𝔼 ⁡ N ∧ ∃ a ∈ 𝔼 ⁡ N ∀ x ∈ A ∀ y ∈ B x Btwn a y → ∃ b ∈ 𝔼 ⁡ N ∀ x ∈ A ∀ y ∈ B b Btwn x y