Metamath Proof Explorer

Theorem axcontlem11

Description: Lemma for axcont . Eliminate the hypotheses from axcontlem10 . (Contributed by Scott Fenton, 20-Jun-2013)

Ref Expression
Assertion axcontlem11 ⊢ N ∈ ℕ ∧ A ⊆ 𝔼 ⁡ N ∧ B ⊆ 𝔼 ⁡ N ∧ ∀ x ∈ A ∀ y ∈ B x Btwn Z y ∧ Z ∈ 𝔼 ⁡ N ∧ U ∈ A ∧ B ≠ ∅ ∧ Z ≠ U → ∃ b ∈ 𝔼 ⁡ N ∀ x ∈ A ∀ y ∈ B b Btwn x y

Proof

Step Hyp Ref Expression
1 opeq2 ⊢ q = p → Z q = Z p
2 1 breq2d ⊢ q = p → U Btwn Z q ↔ U Btwn Z p
3 breq1 ⊢ q = p → q Btwn Z U ↔ p Btwn Z U
4 2 3 orbi12d ⊢ q = p → U Btwn Z q ∨ q Btwn Z U ↔ U Btwn Z p ∨ p Btwn Z U
5 4 cbvrabv ⊢ q ∈ 𝔼 ⁡ N | U Btwn Z q ∨ q Btwn Z U = p ∈ 𝔼 ⁡ N | U Btwn Z p ∨ p Btwn Z U
6 eqid ⊢ z r | z ∈ q ∈ 𝔼 ⁡ N | U Btwn Z q ∨ q Btwn Z U ∧ r ∈ 0 +∞ ∧ ∀ j ∈ 1 … N z ⁡ j = 1 − r ⁢ Z ⁡ j + r ⁢ U ⁡ j = z r | z ∈ q ∈ 𝔼 ⁡ N | U Btwn Z q ∨ q Btwn Z U ∧ r ∈ 0 +∞ ∧ ∀ j ∈ 1 … N z ⁡ j = 1 − r ⁢ Z ⁡ j + r ⁢ U ⁡ j
7 6 axcontlem1 ⊢ z r | z ∈ q ∈ 𝔼 ⁡ N | U Btwn Z q ∨ q Btwn Z U ∧ r ∈ 0 +∞ ∧ ∀ j ∈ 1 … N z ⁡ j = 1 − r ⁢ Z ⁡ j + r ⁢ U ⁡ j = x t | x ∈ q ∈ 𝔼 ⁡ N | U Btwn Z q ∨ q Btwn Z U ∧ t ∈ 0 +∞ ∧ ∀ i ∈ 1 … N x ⁡ i = 1 − t ⁢ Z ⁡ i + t ⁢ U ⁡ i
8 5 7 axcontlem10 ⊢ N ∈ ℕ ∧ A ⊆ 𝔼 ⁡ N ∧ B ⊆ 𝔼 ⁡ N ∧ ∀ x ∈ A ∀ y ∈ B x Btwn Z y ∧ Z ∈ 𝔼 ⁡ N ∧ U ∈ A ∧ B ≠ ∅ ∧ Z ≠ U → ∃ b ∈ 𝔼 ⁡ N ∀ x ∈ A ∀ y ∈ B b Btwn x y