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 ${⊢}\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}⟨{Z},{y}⟩\right)\right)\wedge \left(\left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {B}\ne \varnothing \right)\wedge {Z}\ne {U}\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 opeq2 ${⊢}{q}={p}\to ⟨{Z},{q}⟩=⟨{Z},{p}⟩$
2 1 breq2d ${⊢}{q}={p}\to \left({U}\mathrm{Btwn}⟨{Z},{q}⟩↔{U}\mathrm{Btwn}⟨{Z},{p}⟩\right)$
3 breq1 ${⊢}{q}={p}\to \left({q}\mathrm{Btwn}⟨{Z},{U}⟩↔{p}\mathrm{Btwn}⟨{Z},{U}⟩\right)$
4 2 3 orbi12d ${⊢}{q}={p}\to \left(\left({U}\mathrm{Btwn}⟨{Z},{q}⟩\vee {q}\mathrm{Btwn}⟨{Z},{U}⟩\right)↔\left({U}\mathrm{Btwn}⟨{Z},{p}⟩\vee {p}\mathrm{Btwn}⟨{Z},{U}⟩\right)\right)$
5 4 cbvrabv ${⊢}\left\{{q}\in 𝔼\left({N}\right)|\left({U}\mathrm{Btwn}⟨{Z},{q}⟩\vee {q}\mathrm{Btwn}⟨{Z},{U}⟩\right)\right\}=\left\{{p}\in 𝔼\left({N}\right)|\left({U}\mathrm{Btwn}⟨{Z},{p}⟩\vee {p}\mathrm{Btwn}⟨{Z},{U}⟩\right)\right\}$
6 eqid ${⊢}\left\{⟨{z},{r}⟩|\left({z}\in \left\{{q}\in 𝔼\left({N}\right)|\left({U}\mathrm{Btwn}⟨{Z},{q}⟩\vee {q}\mathrm{Btwn}⟨{Z},{U}⟩\right)\right\}\wedge \left({r}\in \left[0,\mathrm{+\infty }\right)\wedge \forall {j}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{z}\left({j}\right)=\left(1-{r}\right){Z}\left({j}\right)+{r}{U}\left({j}\right)\right)\right)\right\}=\left\{⟨{z},{r}⟩|\left({z}\in \left\{{q}\in 𝔼\left({N}\right)|\left({U}\mathrm{Btwn}⟨{Z},{q}⟩\vee {q}\mathrm{Btwn}⟨{Z},{U}⟩\right)\right\}\wedge \left({r}\in \left[0,\mathrm{+\infty }\right)\wedge \forall {j}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{z}\left({j}\right)=\left(1-{r}\right){Z}\left({j}\right)+{r}{U}\left({j}\right)\right)\right)\right\}$
7 6 axcontlem1 ${⊢}\left\{⟨{z},{r}⟩|\left({z}\in \left\{{q}\in 𝔼\left({N}\right)|\left({U}\mathrm{Btwn}⟨{Z},{q}⟩\vee {q}\mathrm{Btwn}⟨{Z},{U}⟩\right)\right\}\wedge \left({r}\in \left[0,\mathrm{+\infty }\right)\wedge \forall {j}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{z}\left({j}\right)=\left(1-{r}\right){Z}\left({j}\right)+{r}{U}\left({j}\right)\right)\right)\right\}=\left\{⟨{x},{t}⟩|\left({x}\in \left\{{q}\in 𝔼\left({N}\right)|\left({U}\mathrm{Btwn}⟨{Z},{q}⟩\vee {q}\mathrm{Btwn}⟨{Z},{U}⟩\right)\right\}\wedge \left({t}\in \left[0,\mathrm{+\infty }\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\right)\right)\right\}$
8 5 7 axcontlem10 ${⊢}\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}⟨{Z},{y}⟩\right)\right)\wedge \left(\left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {B}\ne \varnothing \right)\wedge {Z}\ne {U}\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}⟩$