# Metamath Proof Explorer

## Theorem axcontlem10

Description: Lemma for axcont . Given a handful of assumptions, derive the conclusion of the final theorem. (Contributed by Scott Fenton, 20-Jun-2013)

Ref Expression
Hypotheses axcontlem10.1 ${⊢}{D}=\left\{{p}\in 𝔼\left({N}\right)|\left({U}\mathrm{Btwn}⟨{Z},{p}⟩\vee {p}\mathrm{Btwn}⟨{Z},{U}⟩\right)\right\}$
axcontlem10.2 ${⊢}{F}=\left\{⟨{x},{t}⟩|\left({x}\in {D}\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\}$
Assertion 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}⟩$

### Proof

Step Hyp Ref Expression
1 axcontlem10.1 ${⊢}{D}=\left\{{p}\in 𝔼\left({N}\right)|\left({U}\mathrm{Btwn}⟨{Z},{p}⟩\vee {p}\mathrm{Btwn}⟨{Z},{U}⟩\right)\right\}$
2 axcontlem10.2 ${⊢}{F}=\left\{⟨{x},{t}⟩|\left({x}\in {D}\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\}$
3 imassrn ${⊢}{F}\left[{A}\right]\subseteq \mathrm{ran}{F}$
4 simpll ${⊢}\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 {N}\in ℕ$
5 simprl1 ${⊢}\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 {Z}\in 𝔼\left({N}\right)$
6 simplr1 ${⊢}\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 {A}\subseteq 𝔼\left({N}\right)$
7 simprl2 ${⊢}\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 {U}\in {A}$
8 6 7 sseldd ${⊢}\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 {U}\in 𝔼\left({N}\right)$
9 simprr ${⊢}\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 {Z}\ne {U}$
10 1 2 axcontlem2 ${⊢}\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\to {F}:{D}\underset{1-1 onto}{⟶}\left[0,\mathrm{+\infty }\right)$
11 4 5 8 9 10 syl31anc ${⊢}\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 {F}:{D}\underset{1-1 onto}{⟶}\left[0,\mathrm{+\infty }\right)$
12 f1ofo ${⊢}{F}:{D}\underset{1-1 onto}{⟶}\left[0,\mathrm{+\infty }\right)\to {F}:{D}\underset{onto}{⟶}\left[0,\mathrm{+\infty }\right)$
13 forn ${⊢}{F}:{D}\underset{onto}{⟶}\left[0,\mathrm{+\infty }\right)\to \mathrm{ran}{F}=\left[0,\mathrm{+\infty }\right)$
14 11 12 13 3syl ${⊢}\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 \mathrm{ran}{F}=\left[0,\mathrm{+\infty }\right)$
15 3 14 sseqtrid ${⊢}\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 {F}\left[{A}\right]\subseteq \left[0,\mathrm{+\infty }\right)$
16 rge0ssre ${⊢}\left[0,\mathrm{+\infty }\right)\subseteq ℝ$
17 15 16 sstrdi ${⊢}\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 {F}\left[{A}\right]\subseteq ℝ$
18 imassrn ${⊢}{F}\left[{B}\right]\subseteq \mathrm{ran}{F}$
19 18 14 sseqtrid ${⊢}\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 {F}\left[{B}\right]\subseteq \left[0,\mathrm{+\infty }\right)$
20 19 16 sstrdi ${⊢}\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 {F}\left[{B}\right]\subseteq ℝ$
21 1 2 axcontlem9 ${⊢}\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 \forall {m}\in {F}\left[{A}\right]\phantom{\rule{.4em}{0ex}}\forall {n}\in {F}\left[{B}\right]\phantom{\rule{.4em}{0ex}}{m}\le {n}$
22 dedekindle ${⊢}\left({F}\left[{A}\right]\subseteq ℝ\wedge {F}\left[{B}\right]\subseteq ℝ\wedge \forall {m}\in {F}\left[{A}\right]\phantom{\rule{.4em}{0ex}}\forall {n}\in {F}\left[{B}\right]\phantom{\rule{.4em}{0ex}}{m}\le {n}\right)\to \exists {k}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {m}\in {F}\left[{A}\right]\phantom{\rule{.4em}{0ex}}\forall {n}\in {F}\left[{B}\right]\phantom{\rule{.4em}{0ex}}\left({m}\le {k}\wedge {k}\le {n}\right)$
23 17 20 21 22 syl3anc ${⊢}\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 {k}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {m}\in {F}\left[{A}\right]\phantom{\rule{.4em}{0ex}}\forall {n}\in {F}\left[{B}\right]\phantom{\rule{.4em}{0ex}}\left({m}\le {k}\wedge {k}\le {n}\right)$
24 simpr ${⊢}\left(\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(\left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {B}\ne \varnothing \right)\wedge {Z}\ne {U}\right)\right)\wedge \forall {m}\in {F}\left[{A}\right]\phantom{\rule{.4em}{0ex}}\forall {n}\in {F}\left[{B}\right]\phantom{\rule{.4em}{0ex}}\left({m}\le {k}\wedge {k}\le {n}\right)\right)\wedge {k}\in ℝ\right)\to {k}\in ℝ$
25 simprl3 ${⊢}\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 {B}\ne \varnothing$
26 25 ad2antrr ${⊢}\left(\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(\left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {B}\ne \varnothing \right)\wedge {Z}\ne {U}\right)\right)\wedge \forall {m}\in {F}\left[{A}\right]\phantom{\rule{.4em}{0ex}}\forall {n}\in {F}\left[{B}\right]\phantom{\rule{.4em}{0ex}}\left({m}\le {k}\wedge {k}\le {n}\right)\right)\wedge {k}\in ℝ\right)\to {B}\ne \varnothing$
27 n0 ${⊢}{B}\ne \varnothing ↔\exists {b}\phantom{\rule{.4em}{0ex}}{b}\in {B}$
28 26 27 sylib ${⊢}\left(\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(\left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {B}\ne \varnothing \right)\wedge {Z}\ne {U}\right)\right)\wedge \forall {m}\in {F}\left[{A}\right]\phantom{\rule{.4em}{0ex}}\forall {n}\in {F}\left[{B}\right]\phantom{\rule{.4em}{0ex}}\left({m}\le {k}\wedge {k}\le {n}\right)\right)\wedge {k}\in ℝ\right)\to \exists {b}\phantom{\rule{.4em}{0ex}}{b}\in {B}$
29 0red ${⊢}\left(\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(\left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {B}\ne \varnothing \right)\wedge {Z}\ne {U}\right)\right)\wedge \forall {m}\in {F}\left[{A}\right]\phantom{\rule{.4em}{0ex}}\forall {n}\in {F}\left[{B}\right]\phantom{\rule{.4em}{0ex}}\left({m}\le {k}\wedge {k}\le {n}\right)\right)\wedge \left({k}\in ℝ\wedge {b}\in {B}\right)\right)\to 0\in ℝ$
30 f1of ${⊢}{F}:{D}\underset{1-1 onto}{⟶}\left[0,\mathrm{+\infty }\right)\to {F}:{D}⟶\left[0,\mathrm{+\infty }\right)$
31 11 30 syl ${⊢}\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 {F}:{D}⟶\left[0,\mathrm{+\infty }\right)$
32 1 axcontlem4 ${⊢}\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 {A}\subseteq {D}$
33 32 7 sseldd ${⊢}\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 {U}\in {D}$
34 31 33 ffvelrnd ${⊢}\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 {F}\left({U}\right)\in \left[0,\mathrm{+\infty }\right)$
35 16 34 sseldi ${⊢}\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 {F}\left({U}\right)\in ℝ$
36 35 ad2antrr ${⊢}\left(\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(\left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {B}\ne \varnothing \right)\wedge {Z}\ne {U}\right)\right)\wedge \forall {m}\in {F}\left[{A}\right]\phantom{\rule{.4em}{0ex}}\forall {n}\in {F}\left[{B}\right]\phantom{\rule{.4em}{0ex}}\left({m}\le {k}\wedge {k}\le {n}\right)\right)\wedge \left({k}\in ℝ\wedge {b}\in {B}\right)\right)\to {F}\left({U}\right)\in ℝ$
37 simprl ${⊢}\left(\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(\left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {B}\ne \varnothing \right)\wedge {Z}\ne {U}\right)\right)\wedge \forall {m}\in {F}\left[{A}\right]\phantom{\rule{.4em}{0ex}}\forall {n}\in {F}\left[{B}\right]\phantom{\rule{.4em}{0ex}}\left({m}\le {k}\wedge {k}\le {n}\right)\right)\wedge \left({k}\in ℝ\wedge {b}\in {B}\right)\right)\to {k}\in ℝ$
38 elrege0 ${⊢}{F}\left({U}\right)\in \left[0,\mathrm{+\infty }\right)↔\left({F}\left({U}\right)\in ℝ\wedge 0\le {F}\left({U}\right)\right)$
39 38 simprbi ${⊢}{F}\left({U}\right)\in \left[0,\mathrm{+\infty }\right)\to 0\le {F}\left({U}\right)$
40 34 39 syl ${⊢}\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 0\le {F}\left({U}\right)$
41 40 ad2antrr ${⊢}\left(\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(\left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {B}\ne \varnothing \right)\wedge {Z}\ne {U}\right)\right)\wedge \forall {m}\in {F}\left[{A}\right]\phantom{\rule{.4em}{0ex}}\forall {n}\in {F}\left[{B}\right]\phantom{\rule{.4em}{0ex}}\left({m}\le {k}\wedge {k}\le {n}\right)\right)\wedge \left({k}\in ℝ\wedge {b}\in {B}\right)\right)\to 0\le {F}\left({U}\right)$
42 f1of1 ${⊢}{F}:{D}\underset{1-1 onto}{⟶}\left[0,\mathrm{+\infty }\right)\to {F}:{D}\underset{1-1}{⟶}\left[0,\mathrm{+\infty }\right)$
43 11 42 syl ${⊢}\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 {F}:{D}\underset{1-1}{⟶}\left[0,\mathrm{+\infty }\right)$
44 f1elima ${⊢}\left({F}:{D}\underset{1-1}{⟶}\left[0,\mathrm{+\infty }\right)\wedge {U}\in {D}\wedge {A}\subseteq {D}\right)\to \left({F}\left({U}\right)\in {F}\left[{A}\right]↔{U}\in {A}\right)$
45 43 33 32 44 syl3anc ${⊢}\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 \left({F}\left({U}\right)\in {F}\left[{A}\right]↔{U}\in {A}\right)$
46 7 45 mpbird ${⊢}\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 {F}\left({U}\right)\in {F}\left[{A}\right]$
47 46 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(\left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {B}\ne \varnothing \right)\wedge {Z}\ne {U}\right)\right)\wedge \left({k}\in ℝ\wedge {b}\in {B}\right)\right)\to {F}\left({U}\right)\in {F}\left[{A}\right]$
48 simpr ${⊢}\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(\left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {B}\ne \varnothing \right)\wedge {Z}\ne {U}\right)\right)\wedge {b}\in {B}\right)\to {b}\in {B}$
49 43 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(\left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {B}\ne \varnothing \right)\wedge {Z}\ne {U}\right)\right)\wedge {b}\in {B}\right)\to {F}:{D}\underset{1-1}{⟶}\left[0,\mathrm{+\infty }\right)$
50 simpl1 ${⊢}\left(\left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {B}\ne \varnothing \right)\wedge {Z}\ne {U}\right)\to {Z}\in 𝔼\left({N}\right)$
51 simpl2 ${⊢}\left(\left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {B}\ne \varnothing \right)\wedge {Z}\ne {U}\right)\to {U}\in {A}$
52 simpr ${⊢}\left(\left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {B}\ne \varnothing \right)\wedge {Z}\ne {U}\right)\to {Z}\ne {U}$
53 50 51 52 3jca ${⊢}\left(\left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {B}\ne \varnothing \right)\wedge {Z}\ne {U}\right)\to \left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {Z}\ne {U}\right)$
54 1 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}$
55 53 54 sylan2 ${⊢}\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 {B}\subseteq {D}$
56 55 sselda ${⊢}\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(\left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {B}\ne \varnothing \right)\wedge {Z}\ne {U}\right)\right)\wedge {b}\in {B}\right)\to {b}\in {D}$
57 55 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(\left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {B}\ne \varnothing \right)\wedge {Z}\ne {U}\right)\right)\wedge {b}\in {B}\right)\to {B}\subseteq {D}$
58 f1elima ${⊢}\left({F}:{D}\underset{1-1}{⟶}\left[0,\mathrm{+\infty }\right)\wedge {b}\in {D}\wedge {B}\subseteq {D}\right)\to \left({F}\left({b}\right)\in {F}\left[{B}\right]↔{b}\in {B}\right)$
59 49 56 57 58 syl3anc ${⊢}\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(\left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {B}\ne \varnothing \right)\wedge {Z}\ne {U}\right)\right)\wedge {b}\in {B}\right)\to \left({F}\left({b}\right)\in {F}\left[{B}\right]↔{b}\in {B}\right)$
60 48 59 mpbird ${⊢}\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(\left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {B}\ne \varnothing \right)\wedge {Z}\ne {U}\right)\right)\wedge {b}\in {B}\right)\to {F}\left({b}\right)\in {F}\left[{B}\right]$
61 60 adantrl ${⊢}\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(\left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {B}\ne \varnothing \right)\wedge {Z}\ne {U}\right)\right)\wedge \left({k}\in ℝ\wedge {b}\in {B}\right)\right)\to {F}\left({b}\right)\in {F}\left[{B}\right]$
62 47 61 jca ${⊢}\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(\left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {B}\ne \varnothing \right)\wedge {Z}\ne {U}\right)\right)\wedge \left({k}\in ℝ\wedge {b}\in {B}\right)\right)\to \left({F}\left({U}\right)\in {F}\left[{A}\right]\wedge {F}\left({b}\right)\in {F}\left[{B}\right]\right)$
63 breq1 ${⊢}{m}={F}\left({U}\right)\to \left({m}\le {k}↔{F}\left({U}\right)\le {k}\right)$
64 63 anbi1d ${⊢}{m}={F}\left({U}\right)\to \left(\left({m}\le {k}\wedge {k}\le {n}\right)↔\left({F}\left({U}\right)\le {k}\wedge {k}\le {n}\right)\right)$
65 breq2 ${⊢}{n}={F}\left({b}\right)\to \left({k}\le {n}↔{k}\le {F}\left({b}\right)\right)$
66 65 anbi2d ${⊢}{n}={F}\left({b}\right)\to \left(\left({F}\left({U}\right)\le {k}\wedge {k}\le {n}\right)↔\left({F}\left({U}\right)\le {k}\wedge {k}\le {F}\left({b}\right)\right)\right)$
67 64 66 rspc2va ${⊢}\left(\left({F}\left({U}\right)\in {F}\left[{A}\right]\wedge {F}\left({b}\right)\in {F}\left[{B}\right]\right)\wedge \forall {m}\in {F}\left[{A}\right]\phantom{\rule{.4em}{0ex}}\forall {n}\in {F}\left[{B}\right]\phantom{\rule{.4em}{0ex}}\left({m}\le {k}\wedge {k}\le {n}\right)\right)\to \left({F}\left({U}\right)\le {k}\wedge {k}\le {F}\left({b}\right)\right)$
68 62 67 sylan ${⊢}\left(\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(\left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {B}\ne \varnothing \right)\wedge {Z}\ne {U}\right)\right)\wedge \left({k}\in ℝ\wedge {b}\in {B}\right)\right)\wedge \forall {m}\in {F}\left[{A}\right]\phantom{\rule{.4em}{0ex}}\forall {n}\in {F}\left[{B}\right]\phantom{\rule{.4em}{0ex}}\left({m}\le {k}\wedge {k}\le {n}\right)\right)\to \left({F}\left({U}\right)\le {k}\wedge {k}\le {F}\left({b}\right)\right)$
69 68 an32s ${⊢}\left(\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(\left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {B}\ne \varnothing \right)\wedge {Z}\ne {U}\right)\right)\wedge \forall {m}\in {F}\left[{A}\right]\phantom{\rule{.4em}{0ex}}\forall {n}\in {F}\left[{B}\right]\phantom{\rule{.4em}{0ex}}\left({m}\le {k}\wedge {k}\le {n}\right)\right)\wedge \left({k}\in ℝ\wedge {b}\in {B}\right)\right)\to \left({F}\left({U}\right)\le {k}\wedge {k}\le {F}\left({b}\right)\right)$
70 69 simpld ${⊢}\left(\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(\left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {B}\ne \varnothing \right)\wedge {Z}\ne {U}\right)\right)\wedge \forall {m}\in {F}\left[{A}\right]\phantom{\rule{.4em}{0ex}}\forall {n}\in {F}\left[{B}\right]\phantom{\rule{.4em}{0ex}}\left({m}\le {k}\wedge {k}\le {n}\right)\right)\wedge \left({k}\in ℝ\wedge {b}\in {B}\right)\right)\to {F}\left({U}\right)\le {k}$
71 29 36 37 41 70 letrd ${⊢}\left(\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(\left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {B}\ne \varnothing \right)\wedge {Z}\ne {U}\right)\right)\wedge \forall {m}\in {F}\left[{A}\right]\phantom{\rule{.4em}{0ex}}\forall {n}\in {F}\left[{B}\right]\phantom{\rule{.4em}{0ex}}\left({m}\le {k}\wedge {k}\le {n}\right)\right)\wedge \left({k}\in ℝ\wedge {b}\in {B}\right)\right)\to 0\le {k}$
72 71 expr ${⊢}\left(\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(\left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {B}\ne \varnothing \right)\wedge {Z}\ne {U}\right)\right)\wedge \forall {m}\in {F}\left[{A}\right]\phantom{\rule{.4em}{0ex}}\forall {n}\in {F}\left[{B}\right]\phantom{\rule{.4em}{0ex}}\left({m}\le {k}\wedge {k}\le {n}\right)\right)\wedge {k}\in ℝ\right)\to \left({b}\in {B}\to 0\le {k}\right)$
73 72 exlimdv ${⊢}\left(\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(\left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {B}\ne \varnothing \right)\wedge {Z}\ne {U}\right)\right)\wedge \forall {m}\in {F}\left[{A}\right]\phantom{\rule{.4em}{0ex}}\forall {n}\in {F}\left[{B}\right]\phantom{\rule{.4em}{0ex}}\left({m}\le {k}\wedge {k}\le {n}\right)\right)\wedge {k}\in ℝ\right)\to \left(\exists {b}\phantom{\rule{.4em}{0ex}}{b}\in {B}\to 0\le {k}\right)$
74 28 73 mpd ${⊢}\left(\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(\left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {B}\ne \varnothing \right)\wedge {Z}\ne {U}\right)\right)\wedge \forall {m}\in {F}\left[{A}\right]\phantom{\rule{.4em}{0ex}}\forall {n}\in {F}\left[{B}\right]\phantom{\rule{.4em}{0ex}}\left({m}\le {k}\wedge {k}\le {n}\right)\right)\wedge {k}\in ℝ\right)\to 0\le {k}$
75 elrege0 ${⊢}{k}\in \left[0,\mathrm{+\infty }\right)↔\left({k}\in ℝ\wedge 0\le {k}\right)$
76 24 74 75 sylanbrc ${⊢}\left(\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(\left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {B}\ne \varnothing \right)\wedge {Z}\ne {U}\right)\right)\wedge \forall {m}\in {F}\left[{A}\right]\phantom{\rule{.4em}{0ex}}\forall {n}\in {F}\left[{B}\right]\phantom{\rule{.4em}{0ex}}\left({m}\le {k}\wedge {k}\le {n}\right)\right)\wedge {k}\in ℝ\right)\to {k}\in \left[0,\mathrm{+\infty }\right)$
77 76 ex ${⊢}\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(\left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {B}\ne \varnothing \right)\wedge {Z}\ne {U}\right)\right)\wedge \forall {m}\in {F}\left[{A}\right]\phantom{\rule{.4em}{0ex}}\forall {n}\in {F}\left[{B}\right]\phantom{\rule{.4em}{0ex}}\left({m}\le {k}\wedge {k}\le {n}\right)\right)\to \left({k}\in ℝ\to {k}\in \left[0,\mathrm{+\infty }\right)\right)$
78 1 ssrab3 ${⊢}{D}\subseteq 𝔼\left({N}\right)$
79 simpr ${⊢}\left(\forall {m}\in {F}\left[{A}\right]\phantom{\rule{.4em}{0ex}}\forall {n}\in {F}\left[{B}\right]\phantom{\rule{.4em}{0ex}}\left({m}\le {k}\wedge {k}\le {n}\right)\wedge {k}\in \left[0,\mathrm{+\infty }\right)\right)\to {k}\in \left[0,\mathrm{+\infty }\right)$
80 f1ocnvdm ${⊢}\left({F}:{D}\underset{1-1 onto}{⟶}\left[0,\mathrm{+\infty }\right)\wedge {k}\in \left[0,\mathrm{+\infty }\right)\right)\to {{F}}^{-1}\left({k}\right)\in {D}$
81 11 79 80 syl2an ${⊢}\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(\left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {B}\ne \varnothing \right)\wedge {Z}\ne {U}\right)\right)\wedge \left(\forall {m}\in {F}\left[{A}\right]\phantom{\rule{.4em}{0ex}}\forall {n}\in {F}\left[{B}\right]\phantom{\rule{.4em}{0ex}}\left({m}\le {k}\wedge {k}\le {n}\right)\wedge {k}\in \left[0,\mathrm{+\infty }\right)\right)\right)\to {{F}}^{-1}\left({k}\right)\in {D}$
82 78 81 sseldi ${⊢}\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(\left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {B}\ne \varnothing \right)\wedge {Z}\ne {U}\right)\right)\wedge \left(\forall {m}\in {F}\left[{A}\right]\phantom{\rule{.4em}{0ex}}\forall {n}\in {F}\left[{B}\right]\phantom{\rule{.4em}{0ex}}\left({m}\le {k}\wedge {k}\le {n}\right)\wedge {k}\in \left[0,\mathrm{+\infty }\right)\right)\right)\to {{F}}^{-1}\left({k}\right)\in 𝔼\left({N}\right)$
83 4 5 8 3jca ${⊢}\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 \left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)$
84 83 9 jca ${⊢}\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 \left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)$
85 84 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(\left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {B}\ne \varnothing \right)\wedge {Z}\ne {U}\right)\right)\wedge \left(\left(\forall {m}\in {F}\left[{A}\right]\phantom{\rule{.4em}{0ex}}\forall {n}\in {F}\left[{B}\right]\phantom{\rule{.4em}{0ex}}\left({m}\le {k}\wedge {k}\le {n}\right)\wedge {k}\in \left[0,\mathrm{+\infty }\right)\right)\wedge \left({q}\in {A}\wedge {r}\in {B}\right)\right)\right)\to \left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)$
86 32 sselda ${⊢}\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(\left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {B}\ne \varnothing \right)\wedge {Z}\ne {U}\right)\right)\wedge {q}\in {A}\right)\to {q}\in {D}$
87 86 adantrr ${⊢}\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(\left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {B}\ne \varnothing \right)\wedge {Z}\ne {U}\right)\right)\wedge \left({q}\in {A}\wedge {r}\in {B}\right)\right)\to {q}\in {D}$
88 87 adantrl ${⊢}\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(\left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {B}\ne \varnothing \right)\wedge {Z}\ne {U}\right)\right)\wedge \left(\left(\forall {m}\in {F}\left[{A}\right]\phantom{\rule{.4em}{0ex}}\forall {n}\in {F}\left[{B}\right]\phantom{\rule{.4em}{0ex}}\left({m}\le {k}\wedge {k}\le {n}\right)\wedge {k}\in \left[0,\mathrm{+\infty }\right)\right)\wedge \left({q}\in {A}\wedge {r}\in {B}\right)\right)\right)\to {q}\in {D}$
89 simplr ${⊢}\left(\left(\forall {m}\in {F}\left[{A}\right]\phantom{\rule{.4em}{0ex}}\forall {n}\in {F}\left[{B}\right]\phantom{\rule{.4em}{0ex}}\left({m}\le {k}\wedge {k}\le {n}\right)\wedge {k}\in \left[0,\mathrm{+\infty }\right)\right)\wedge \left({q}\in {A}\wedge {r}\in {B}\right)\right)\to {k}\in \left[0,\mathrm{+\infty }\right)$
90 11 89 80 syl2an ${⊢}\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(\left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {B}\ne \varnothing \right)\wedge {Z}\ne {U}\right)\right)\wedge \left(\left(\forall {m}\in {F}\left[{A}\right]\phantom{\rule{.4em}{0ex}}\forall {n}\in {F}\left[{B}\right]\phantom{\rule{.4em}{0ex}}\left({m}\le {k}\wedge {k}\le {n}\right)\wedge {k}\in \left[0,\mathrm{+\infty }\right)\right)\wedge \left({q}\in {A}\wedge {r}\in {B}\right)\right)\right)\to {{F}}^{-1}\left({k}\right)\in {D}$
91 55 sselda ${⊢}\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(\left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {B}\ne \varnothing \right)\wedge {Z}\ne {U}\right)\right)\wedge {r}\in {B}\right)\to {r}\in {D}$
92 91 adantrl ${⊢}\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(\left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {B}\ne \varnothing \right)\wedge {Z}\ne {U}\right)\right)\wedge \left({q}\in {A}\wedge {r}\in {B}\right)\right)\to {r}\in {D}$
93 92 adantrl ${⊢}\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(\left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {B}\ne \varnothing \right)\wedge {Z}\ne {U}\right)\right)\wedge \left(\left(\forall {m}\in {F}\left[{A}\right]\phantom{\rule{.4em}{0ex}}\forall {n}\in {F}\left[{B}\right]\phantom{\rule{.4em}{0ex}}\left({m}\le {k}\wedge {k}\le {n}\right)\wedge {k}\in \left[0,\mathrm{+\infty }\right)\right)\wedge \left({q}\in {A}\wedge {r}\in {B}\right)\right)\right)\to {r}\in {D}$
94 88 90 93 3jca ${⊢}\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(\left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {B}\ne \varnothing \right)\wedge {Z}\ne {U}\right)\right)\wedge \left(\left(\forall {m}\in {F}\left[{A}\right]\phantom{\rule{.4em}{0ex}}\forall {n}\in {F}\left[{B}\right]\phantom{\rule{.4em}{0ex}}\left({m}\le {k}\wedge {k}\le {n}\right)\wedge {k}\in \left[0,\mathrm{+\infty }\right)\right)\wedge \left({q}\in {A}\wedge {r}\in {B}\right)\right)\right)\to \left({q}\in {D}\wedge {{F}}^{-1}\left({k}\right)\in {D}\wedge {r}\in {D}\right)$
95 85 94 jca ${⊢}\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(\left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {B}\ne \varnothing \right)\wedge {Z}\ne {U}\right)\right)\wedge \left(\left(\forall {m}\in {F}\left[{A}\right]\phantom{\rule{.4em}{0ex}}\forall {n}\in {F}\left[{B}\right]\phantom{\rule{.4em}{0ex}}\left({m}\le {k}\wedge {k}\le {n}\right)\wedge {k}\in \left[0,\mathrm{+\infty }\right)\right)\wedge \left({q}\in {A}\wedge {r}\in {B}\right)\right)\right)\to \left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({q}\in {D}\wedge {{F}}^{-1}\left({k}\right)\in {D}\wedge {r}\in {D}\right)\right)$
96 f1ofun ${⊢}{F}:{D}\underset{1-1 onto}{⟶}\left[0,\mathrm{+\infty }\right)\to \mathrm{Fun}{F}$
97 11 96 syl ${⊢}\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 \mathrm{Fun}{F}$
98 fdm ${⊢}{F}:{D}⟶\left[0,\mathrm{+\infty }\right)\to \mathrm{dom}{F}={D}$
99 11 30 98 3syl ${⊢}\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 \mathrm{dom}{F}={D}$
100 32 99 sseqtrrd ${⊢}\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 {A}\subseteq \mathrm{dom}{F}$
101 funfvima2 ${⊢}\left(\mathrm{Fun}{F}\wedge {A}\subseteq \mathrm{dom}{F}\right)\to \left({q}\in {A}\to {F}\left({q}\right)\in {F}\left[{A}\right]\right)$
102 97 100 101 syl2anc ${⊢}\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 \left({q}\in {A}\to {F}\left({q}\right)\in {F}\left[{A}\right]\right)$
103 55 99 sseqtrrd ${⊢}\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 {B}\subseteq \mathrm{dom}{F}$
104 funfvima2 ${⊢}\left(\mathrm{Fun}{F}\wedge {B}\subseteq \mathrm{dom}{F}\right)\to \left({r}\in {B}\to {F}\left({r}\right)\in {F}\left[{B}\right]\right)$
105 97 103 104 syl2anc ${⊢}\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 \left({r}\in {B}\to {F}\left({r}\right)\in {F}\left[{B}\right]\right)$
106 102 105 anim12d ${⊢}\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 \left(\left({q}\in {A}\wedge {r}\in {B}\right)\to \left({F}\left({q}\right)\in {F}\left[{A}\right]\wedge {F}\left({r}\right)\in {F}\left[{B}\right]\right)\right)$
107 106 imp ${⊢}\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(\left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {B}\ne \varnothing \right)\wedge {Z}\ne {U}\right)\right)\wedge \left({q}\in {A}\wedge {r}\in {B}\right)\right)\to \left({F}\left({q}\right)\in {F}\left[{A}\right]\wedge {F}\left({r}\right)\in {F}\left[{B}\right]\right)$
108 107 adantrl ${⊢}\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(\left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {B}\ne \varnothing \right)\wedge {Z}\ne {U}\right)\right)\wedge \left(\left(\forall {m}\in {F}\left[{A}\right]\phantom{\rule{.4em}{0ex}}\forall {n}\in {F}\left[{B}\right]\phantom{\rule{.4em}{0ex}}\left({m}\le {k}\wedge {k}\le {n}\right)\wedge {k}\in \left[0,\mathrm{+\infty }\right)\right)\wedge \left({q}\in {A}\wedge {r}\in {B}\right)\right)\right)\to \left({F}\left({q}\right)\in {F}\left[{A}\right]\wedge {F}\left({r}\right)\in {F}\left[{B}\right]\right)$
109 simprll ${⊢}\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(\left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {B}\ne \varnothing \right)\wedge {Z}\ne {U}\right)\right)\wedge \left(\left(\forall {m}\in {F}\left[{A}\right]\phantom{\rule{.4em}{0ex}}\forall {n}\in {F}\left[{B}\right]\phantom{\rule{.4em}{0ex}}\left({m}\le {k}\wedge {k}\le {n}\right)\wedge {k}\in \left[0,\mathrm{+\infty }\right)\right)\wedge \left({q}\in {A}\wedge {r}\in {B}\right)\right)\right)\to \forall {m}\in {F}\left[{A}\right]\phantom{\rule{.4em}{0ex}}\forall {n}\in {F}\left[{B}\right]\phantom{\rule{.4em}{0ex}}\left({m}\le {k}\wedge {k}\le {n}\right)$
110 breq1 ${⊢}{m}={F}\left({q}\right)\to \left({m}\le {k}↔{F}\left({q}\right)\le {k}\right)$
111 110 anbi1d ${⊢}{m}={F}\left({q}\right)\to \left(\left({m}\le {k}\wedge {k}\le {n}\right)↔\left({F}\left({q}\right)\le {k}\wedge {k}\le {n}\right)\right)$
112 breq2 ${⊢}{n}={F}\left({r}\right)\to \left({k}\le {n}↔{k}\le {F}\left({r}\right)\right)$
113 112 anbi2d ${⊢}{n}={F}\left({r}\right)\to \left(\left({F}\left({q}\right)\le {k}\wedge {k}\le {n}\right)↔\left({F}\left({q}\right)\le {k}\wedge {k}\le {F}\left({r}\right)\right)\right)$
114 111 113 rspc2v ${⊢}\left({F}\left({q}\right)\in {F}\left[{A}\right]\wedge {F}\left({r}\right)\in {F}\left[{B}\right]\right)\to \left(\forall {m}\in {F}\left[{A}\right]\phantom{\rule{.4em}{0ex}}\forall {n}\in {F}\left[{B}\right]\phantom{\rule{.4em}{0ex}}\left({m}\le {k}\wedge {k}\le {n}\right)\to \left({F}\left({q}\right)\le {k}\wedge {k}\le {F}\left({r}\right)\right)\right)$
115 108 109 114 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(\left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {B}\ne \varnothing \right)\wedge {Z}\ne {U}\right)\right)\wedge \left(\left(\forall {m}\in {F}\left[{A}\right]\phantom{\rule{.4em}{0ex}}\forall {n}\in {F}\left[{B}\right]\phantom{\rule{.4em}{0ex}}\left({m}\le {k}\wedge {k}\le {n}\right)\wedge {k}\in \left[0,\mathrm{+\infty }\right)\right)\wedge \left({q}\in {A}\wedge {r}\in {B}\right)\right)\right)\to \left({F}\left({q}\right)\le {k}\wedge {k}\le {F}\left({r}\right)\right)$
116 f1ocnvfv2 ${⊢}\left({F}:{D}\underset{1-1 onto}{⟶}\left[0,\mathrm{+\infty }\right)\wedge {k}\in \left[0,\mathrm{+\infty }\right)\right)\to {F}\left({{F}}^{-1}\left({k}\right)\right)={k}$
117 11 89 116 syl2an ${⊢}\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(\left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {B}\ne \varnothing \right)\wedge {Z}\ne {U}\right)\right)\wedge \left(\left(\forall {m}\in {F}\left[{A}\right]\phantom{\rule{.4em}{0ex}}\forall {n}\in {F}\left[{B}\right]\phantom{\rule{.4em}{0ex}}\left({m}\le {k}\wedge {k}\le {n}\right)\wedge {k}\in \left[0,\mathrm{+\infty }\right)\right)\wedge \left({q}\in {A}\wedge {r}\in {B}\right)\right)\right)\to {F}\left({{F}}^{-1}\left({k}\right)\right)={k}$
118 117 breq2d ${⊢}\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(\left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {B}\ne \varnothing \right)\wedge {Z}\ne {U}\right)\right)\wedge \left(\left(\forall {m}\in {F}\left[{A}\right]\phantom{\rule{.4em}{0ex}}\forall {n}\in {F}\left[{B}\right]\phantom{\rule{.4em}{0ex}}\left({m}\le {k}\wedge {k}\le {n}\right)\wedge {k}\in \left[0,\mathrm{+\infty }\right)\right)\wedge \left({q}\in {A}\wedge {r}\in {B}\right)\right)\right)\to \left({F}\left({q}\right)\le {F}\left({{F}}^{-1}\left({k}\right)\right)↔{F}\left({q}\right)\le {k}\right)$
119 117 breq1d ${⊢}\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(\left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {B}\ne \varnothing \right)\wedge {Z}\ne {U}\right)\right)\wedge \left(\left(\forall {m}\in {F}\left[{A}\right]\phantom{\rule{.4em}{0ex}}\forall {n}\in {F}\left[{B}\right]\phantom{\rule{.4em}{0ex}}\left({m}\le {k}\wedge {k}\le {n}\right)\wedge {k}\in \left[0,\mathrm{+\infty }\right)\right)\wedge \left({q}\in {A}\wedge {r}\in {B}\right)\right)\right)\to \left({F}\left({{F}}^{-1}\left({k}\right)\right)\le {F}\left({r}\right)↔{k}\le {F}\left({r}\right)\right)$
120 118 119 anbi12d ${⊢}\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(\left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {B}\ne \varnothing \right)\wedge {Z}\ne {U}\right)\right)\wedge \left(\left(\forall {m}\in {F}\left[{A}\right]\phantom{\rule{.4em}{0ex}}\forall {n}\in {F}\left[{B}\right]\phantom{\rule{.4em}{0ex}}\left({m}\le {k}\wedge {k}\le {n}\right)\wedge {k}\in \left[0,\mathrm{+\infty }\right)\right)\wedge \left({q}\in {A}\wedge {r}\in {B}\right)\right)\right)\to \left(\left({F}\left({q}\right)\le {F}\left({{F}}^{-1}\left({k}\right)\right)\wedge {F}\left({{F}}^{-1}\left({k}\right)\right)\le {F}\left({r}\right)\right)↔\left({F}\left({q}\right)\le {k}\wedge {k}\le {F}\left({r}\right)\right)\right)$
121 115 120 mpbird ${⊢}\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(\left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {B}\ne \varnothing \right)\wedge {Z}\ne {U}\right)\right)\wedge \left(\left(\forall {m}\in {F}\left[{A}\right]\phantom{\rule{.4em}{0ex}}\forall {n}\in {F}\left[{B}\right]\phantom{\rule{.4em}{0ex}}\left({m}\le {k}\wedge {k}\le {n}\right)\wedge {k}\in \left[0,\mathrm{+\infty }\right)\right)\wedge \left({q}\in {A}\wedge {r}\in {B}\right)\right)\right)\to \left({F}\left({q}\right)\le {F}\left({{F}}^{-1}\left({k}\right)\right)\wedge {F}\left({{F}}^{-1}\left({k}\right)\right)\le {F}\left({r}\right)\right)$
122 1 2 axcontlem8 ${⊢}\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({q}\in {D}\wedge {{F}}^{-1}\left({k}\right)\in {D}\wedge {r}\in {D}\right)\right)\to \left(\left({F}\left({q}\right)\le {F}\left({{F}}^{-1}\left({k}\right)\right)\wedge {F}\left({{F}}^{-1}\left({k}\right)\right)\le {F}\left({r}\right)\right)\to {{F}}^{-1}\left({k}\right)\mathrm{Btwn}⟨{q},{r}⟩\right)$
123 95 121 122 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(\left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {B}\ne \varnothing \right)\wedge {Z}\ne {U}\right)\right)\wedge \left(\left(\forall {m}\in {F}\left[{A}\right]\phantom{\rule{.4em}{0ex}}\forall {n}\in {F}\left[{B}\right]\phantom{\rule{.4em}{0ex}}\left({m}\le {k}\wedge {k}\le {n}\right)\wedge {k}\in \left[0,\mathrm{+\infty }\right)\right)\wedge \left({q}\in {A}\wedge {r}\in {B}\right)\right)\right)\to {{F}}^{-1}\left({k}\right)\mathrm{Btwn}⟨{q},{r}⟩$
124 123 anassrs ${⊢}\left(\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(\left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {B}\ne \varnothing \right)\wedge {Z}\ne {U}\right)\right)\wedge \left(\forall {m}\in {F}\left[{A}\right]\phantom{\rule{.4em}{0ex}}\forall {n}\in {F}\left[{B}\right]\phantom{\rule{.4em}{0ex}}\left({m}\le {k}\wedge {k}\le {n}\right)\wedge {k}\in \left[0,\mathrm{+\infty }\right)\right)\right)\wedge \left({q}\in {A}\wedge {r}\in {B}\right)\right)\to {{F}}^{-1}\left({k}\right)\mathrm{Btwn}⟨{q},{r}⟩$
125 124 ralrimivva ${⊢}\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(\left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {B}\ne \varnothing \right)\wedge {Z}\ne {U}\right)\right)\wedge \left(\forall {m}\in {F}\left[{A}\right]\phantom{\rule{.4em}{0ex}}\forall {n}\in {F}\left[{B}\right]\phantom{\rule{.4em}{0ex}}\left({m}\le {k}\wedge {k}\le {n}\right)\wedge {k}\in \left[0,\mathrm{+\infty }\right)\right)\right)\to \forall {q}\in {A}\phantom{\rule{.4em}{0ex}}\forall {r}\in {B}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left({k}\right)\mathrm{Btwn}⟨{q},{r}⟩$
126 opeq1 ${⊢}{q}={x}\to ⟨{q},{r}⟩=⟨{x},{r}⟩$
127 126 breq2d ${⊢}{q}={x}\to \left({{F}}^{-1}\left({k}\right)\mathrm{Btwn}⟨{q},{r}⟩↔{{F}}^{-1}\left({k}\right)\mathrm{Btwn}⟨{x},{r}⟩\right)$
128 opeq2 ${⊢}{r}={y}\to ⟨{x},{r}⟩=⟨{x},{y}⟩$
129 128 breq2d ${⊢}{r}={y}\to \left({{F}}^{-1}\left({k}\right)\mathrm{Btwn}⟨{x},{r}⟩↔{{F}}^{-1}\left({k}\right)\mathrm{Btwn}⟨{x},{y}⟩\right)$
130 127 129 cbvral2vw ${⊢}\forall {q}\in {A}\phantom{\rule{.4em}{0ex}}\forall {r}\in {B}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left({k}\right)\mathrm{Btwn}⟨{q},{r}⟩↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left({k}\right)\mathrm{Btwn}⟨{x},{y}⟩$
131 125 130 sylib ${⊢}\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(\left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {B}\ne \varnothing \right)\wedge {Z}\ne {U}\right)\right)\wedge \left(\forall {m}\in {F}\left[{A}\right]\phantom{\rule{.4em}{0ex}}\forall {n}\in {F}\left[{B}\right]\phantom{\rule{.4em}{0ex}}\left({m}\le {k}\wedge {k}\le {n}\right)\wedge {k}\in \left[0,\mathrm{+\infty }\right)\right)\right)\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left({k}\right)\mathrm{Btwn}⟨{x},{y}⟩$
132 breq1 ${⊢}{b}={{F}}^{-1}\left({k}\right)\to \left({b}\mathrm{Btwn}⟨{x},{y}⟩↔{{F}}^{-1}\left({k}\right)\mathrm{Btwn}⟨{x},{y}⟩\right)$
133 132 2ralbidv ${⊢}{b}={{F}}^{-1}\left({k}\right)\to \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{b}\mathrm{Btwn}⟨{x},{y}⟩↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left({k}\right)\mathrm{Btwn}⟨{x},{y}⟩\right)$
134 133 rspcev ${⊢}\left({{F}}^{-1}\left({k}\right)\in 𝔼\left({N}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left({k}\right)\mathrm{Btwn}⟨{x},{y}⟩\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}⟩$
135 82 131 134 syl2anc ${⊢}\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(\left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {B}\ne \varnothing \right)\wedge {Z}\ne {U}\right)\right)\wedge \left(\forall {m}\in {F}\left[{A}\right]\phantom{\rule{.4em}{0ex}}\forall {n}\in {F}\left[{B}\right]\phantom{\rule{.4em}{0ex}}\left({m}\le {k}\wedge {k}\le {n}\right)\wedge {k}\in \left[0,\mathrm{+\infty }\right)\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}⟩$
136 135 expr ${⊢}\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(\left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {B}\ne \varnothing \right)\wedge {Z}\ne {U}\right)\right)\wedge \forall {m}\in {F}\left[{A}\right]\phantom{\rule{.4em}{0ex}}\forall {n}\in {F}\left[{B}\right]\phantom{\rule{.4em}{0ex}}\left({m}\le {k}\wedge {k}\le {n}\right)\right)\to \left({k}\in \left[0,\mathrm{+\infty }\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}⟩\right)$
137 77 136 syld ${⊢}\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(\left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {B}\ne \varnothing \right)\wedge {Z}\ne {U}\right)\right)\wedge \forall {m}\in {F}\left[{A}\right]\phantom{\rule{.4em}{0ex}}\forall {n}\in {F}\left[{B}\right]\phantom{\rule{.4em}{0ex}}\left({m}\le {k}\wedge {k}\le {n}\right)\right)\to \left({k}\in ℝ\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}⟩\right)$
138 137 ex ${⊢}\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 \left(\forall {m}\in {F}\left[{A}\right]\phantom{\rule{.4em}{0ex}}\forall {n}\in {F}\left[{B}\right]\phantom{\rule{.4em}{0ex}}\left({m}\le {k}\wedge {k}\le {n}\right)\to \left({k}\in ℝ\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}⟩\right)\right)$
139 138 com23 ${⊢}\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 \left({k}\in ℝ\to \left(\forall {m}\in {F}\left[{A}\right]\phantom{\rule{.4em}{0ex}}\forall {n}\in {F}\left[{B}\right]\phantom{\rule{.4em}{0ex}}\left({m}\le {k}\wedge {k}\le {n}\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}⟩\right)\right)$
140 139 rexlimdv ${⊢}\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 \left(\exists {k}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {m}\in {F}\left[{A}\right]\phantom{\rule{.4em}{0ex}}\forall {n}\in {F}\left[{B}\right]\phantom{\rule{.4em}{0ex}}\left({m}\le {k}\wedge {k}\le {n}\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}⟩\right)$
141 23 140 mpd ${⊢}\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}⟩$