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∈BxBtwnay→∃b∈𝔼⁡N∀x∈A∀y∈BbBtwnxy

Proof

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