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 ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∃ 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑎 , 𝑦 ⟩ ) ) → ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑏 Btwn ⟨ 𝑥 , 𝑦 ⟩ )

Proof

Step Hyp Ref Expression
1 simpr ⊢ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑎 , 𝑦 ⟩ ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑎 , 𝑦 ⟩ )
2 1 3anim3i ⊢ ( ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ( 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑎 , 𝑦 ⟩ ) ) → ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑎 , 𝑦 ⟩ ) )
3 2 anim2i ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ( 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑎 , 𝑦 ⟩ ) ) ) → ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑎 , 𝑦 ⟩ ) ) )
4 simpr3l ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ( 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑎 , 𝑦 ⟩ ) ) ) → 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) )
5 axcontlem12 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑎 , 𝑦 ⟩ ) ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) ) → ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑏 Btwn ⟨ 𝑥 , 𝑦 ⟩ )
6 3 4 5 syl2anc ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ( 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑎 , 𝑦 ⟩ ) ) ) → ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑏 Btwn ⟨ 𝑥 , 𝑦 ⟩ )
7 6 3exp2 ⊢ ( 𝑁 ∈ ℕ → ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) → ( 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) → ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑎 , 𝑦 ⟩ ) → ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑏 Btwn ⟨ 𝑥 , 𝑦 ⟩ ) ) ) )
8 7 com4r ⊢ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑎 , 𝑦 ⟩ ) → ( 𝑁 ∈ ℕ → ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) → ( 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) → ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑏 Btwn ⟨ 𝑥 , 𝑦 ⟩ ) ) ) )
9 8 rexlimiva ⊢ ( ∃ 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑎 , 𝑦 ⟩ → ( 𝑁 ∈ ℕ → ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) → ( 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) → ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑏 Btwn ⟨ 𝑥 , 𝑦 ⟩ ) ) ) )
10 9 com4l ⊢ ( 𝑁 ∈ ℕ → ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) → ( 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) → ( ∃ 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑎 , 𝑦 ⟩ → ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑏 Btwn ⟨ 𝑥 , 𝑦 ⟩ ) ) ) )
11 10 3imp2 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∃ 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑎 , 𝑦 ⟩ ) ) → ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑏 Btwn ⟨ 𝑥 , 𝑦 ⟩ )