# Metamath Proof Explorer

## Theorem axcontlem3

Description: Lemma for axcont . Given the separation assumption, B is a subset of D . (Contributed by Scott Fenton, 18-Jun-2013)

Ref Expression
Hypothesis axcontlem3.1 ${⊢}{D}=\left\{{p}\in 𝔼\left({N}\right)|\left({U}\mathrm{Btwn}⟨{Z},{p}⟩\vee {p}\mathrm{Btwn}⟨{Z},{U}⟩\right)\right\}$
Assertion axcontlem3 ${⊢}\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({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {Z}\ne {U}\right)\right)\to {B}\subseteq {D}$

### Proof

Step Hyp Ref Expression
1 axcontlem3.1 ${⊢}{D}=\left\{{p}\in 𝔼\left({N}\right)|\left({U}\mathrm{Btwn}⟨{Z},{p}⟩\vee {p}\mathrm{Btwn}⟨{Z},{U}⟩\right)\right\}$
2 simplr2 ${⊢}\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({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {Z}\ne {U}\right)\right)\to {B}\subseteq 𝔼\left({N}\right)$
3 simpr2 ${⊢}\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({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {Z}\ne {U}\right)\right)\to {U}\in {A}$
4 3 anim1i ${⊢}\left(\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({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {Z}\ne {U}\right)\right)\wedge {p}\in {B}\right)\to \left({U}\in {A}\wedge {p}\in {B}\right)$
5 simplr3 ${⊢}\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({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {Z}\ne {U}\right)\right)\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\mathrm{Btwn}⟨{Z},{y}⟩$
6 5 adantr ${⊢}\left(\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({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {Z}\ne {U}\right)\right)\wedge {p}\in {B}\right)\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\mathrm{Btwn}⟨{Z},{y}⟩$
7 breq1 ${⊢}{x}={U}\to \left({x}\mathrm{Btwn}⟨{Z},{y}⟩↔{U}\mathrm{Btwn}⟨{Z},{y}⟩\right)$
8 opeq2 ${⊢}{y}={p}\to ⟨{Z},{y}⟩=⟨{Z},{p}⟩$
9 8 breq2d ${⊢}{y}={p}\to \left({U}\mathrm{Btwn}⟨{Z},{y}⟩↔{U}\mathrm{Btwn}⟨{Z},{p}⟩\right)$
10 7 9 rspc2v ${⊢}\left({U}\in {A}\wedge {p}\in {B}\right)\to \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\mathrm{Btwn}⟨{Z},{y}⟩\to {U}\mathrm{Btwn}⟨{Z},{p}⟩\right)$
11 4 6 10 sylc ${⊢}\left(\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({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {Z}\ne {U}\right)\right)\wedge {p}\in {B}\right)\to {U}\mathrm{Btwn}⟨{Z},{p}⟩$
12 11 orcd ${⊢}\left(\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({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {Z}\ne {U}\right)\right)\wedge {p}\in {B}\right)\to \left({U}\mathrm{Btwn}⟨{Z},{p}⟩\vee {p}\mathrm{Btwn}⟨{Z},{U}⟩\right)$
13 12 ralrimiva ${⊢}\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({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {Z}\ne {U}\right)\right)\to \forall {p}\in {B}\phantom{\rule{.4em}{0ex}}\left({U}\mathrm{Btwn}⟨{Z},{p}⟩\vee {p}\mathrm{Btwn}⟨{Z},{U}⟩\right)$
14 1 sseq2i ${⊢}{B}\subseteq {D}↔{B}\subseteq \left\{{p}\in 𝔼\left({N}\right)|\left({U}\mathrm{Btwn}⟨{Z},{p}⟩\vee {p}\mathrm{Btwn}⟨{Z},{U}⟩\right)\right\}$
15 ssrab ${⊢}{B}\subseteq \left\{{p}\in 𝔼\left({N}\right)|\left({U}\mathrm{Btwn}⟨{Z},{p}⟩\vee {p}\mathrm{Btwn}⟨{Z},{U}⟩\right)\right\}↔\left({B}\subseteq 𝔼\left({N}\right)\wedge \forall {p}\in {B}\phantom{\rule{.4em}{0ex}}\left({U}\mathrm{Btwn}⟨{Z},{p}⟩\vee {p}\mathrm{Btwn}⟨{Z},{U}⟩\right)\right)$
16 14 15 bitri ${⊢}{B}\subseteq {D}↔\left({B}\subseteq 𝔼\left({N}\right)\wedge \forall {p}\in {B}\phantom{\rule{.4em}{0ex}}\left({U}\mathrm{Btwn}⟨{Z},{p}⟩\vee {p}\mathrm{Btwn}⟨{Z},{U}⟩\right)\right)$
17 2 13 16 sylanbrc ${⊢}\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({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {Z}\ne {U}\right)\right)\to {B}\subseteq {D}$