Metamath Proof Explorer

Theorem axcontlem9

Description: Lemma for axcont . Given the separation assumption, all values of F over A are less than or equal to all values of F over B . (Contributed by Scott Fenton, 20-Jun-2013)

Ref Expression
Hypotheses axcontlem9.1 ${⊢}{D}=\left\{{p}\in 𝔼\left({N}\right)|\left({U}\mathrm{Btwn}⟨{Z},{p}⟩\vee {p}\mathrm{Btwn}⟨{Z},{U}⟩\right)\right\}$
axcontlem9.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 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 {n}\in {F}\left[{A}\right]\phantom{\rule{.4em}{0ex}}\forall {m}\in {F}\left[{B}\right]\phantom{\rule{.4em}{0ex}}{n}\le {m}$

Proof

Step Hyp Ref Expression
1 axcontlem9.1 ${⊢}{D}=\left\{{p}\in 𝔼\left({N}\right)|\left({U}\mathrm{Btwn}⟨{Z},{p}⟩\vee {p}\mathrm{Btwn}⟨{Z},{U}⟩\right)\right\}$
2 axcontlem9.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 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 ℕ$
4 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)$
5 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)$
6 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}$
7 5 6 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)$
8 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}$
9 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)$
10 3 4 7 8 9 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)$
11 f1ofun ${⊢}{F}:{D}\underset{1-1 onto}{⟶}\left[0,\mathrm{+\infty }\right)\to \mathrm{Fun}{F}$
12 fvelima ${⊢}\left(\mathrm{Fun}{F}\wedge {n}\in {F}\left[{A}\right]\right)\to \exists {a}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({a}\right)={n}$
13 12 ex ${⊢}\mathrm{Fun}{F}\to \left({n}\in {F}\left[{A}\right]\to \exists {a}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({a}\right)={n}\right)$
14 10 11 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 \left({n}\in {F}\left[{A}\right]\to \exists {a}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({a}\right)={n}\right)$
15 fvelima ${⊢}\left(\mathrm{Fun}{F}\wedge {m}\in {F}\left[{B}\right]\right)\to \exists {b}\in {B}\phantom{\rule{.4em}{0ex}}{F}\left({b}\right)={m}$
16 15 ex ${⊢}\mathrm{Fun}{F}\to \left({m}\in {F}\left[{B}\right]\to \exists {b}\in {B}\phantom{\rule{.4em}{0ex}}{F}\left({b}\right)={m}\right)$
17 10 11 16 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 \left({m}\in {F}\left[{B}\right]\to \exists {b}\in {B}\phantom{\rule{.4em}{0ex}}{F}\left({b}\right)={m}\right)$
18 reeanv ${⊢}\exists {a}\in {A}\phantom{\rule{.4em}{0ex}}\exists {b}\in {B}\phantom{\rule{.4em}{0ex}}\left({F}\left({a}\right)={n}\wedge {F}\left({b}\right)={m}\right)↔\left(\exists {a}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({a}\right)={n}\wedge \exists {b}\in {B}\phantom{\rule{.4em}{0ex}}{F}\left({b}\right)={m}\right)$
19 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(\left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {B}\ne \varnothing \right)\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}⟩$
20 breq1 ${⊢}{x}={a}\to \left({x}\mathrm{Btwn}⟨{Z},{y}⟩↔{a}\mathrm{Btwn}⟨{Z},{y}⟩\right)$
21 opeq2 ${⊢}{y}={b}\to ⟨{Z},{y}⟩=⟨{Z},{b}⟩$
22 21 breq2d ${⊢}{y}={b}\to \left({a}\mathrm{Btwn}⟨{Z},{y}⟩↔{a}\mathrm{Btwn}⟨{Z},{b}⟩\right)$
23 20 22 rspc2v ${⊢}\left({a}\in {A}\wedge {b}\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 {a}\mathrm{Btwn}⟨{Z},{b}⟩\right)$
24 19 23 mpan9 ${⊢}\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({a}\in {A}\wedge {b}\in {B}\right)\right)\to {a}\mathrm{Btwn}⟨{Z},{b}⟩$
25 simplll ${⊢}\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({a}\in {A}\wedge {b}\in {B}\right)\right)\to {N}\in ℕ$
26 4 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({a}\in {A}\wedge {b}\in {B}\right)\right)\to {Z}\in 𝔼\left({N}\right)$
27 7 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({a}\in {A}\wedge {b}\in {B}\right)\right)\to {U}\in 𝔼\left({N}\right)$
28 25 26 27 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({a}\in {A}\wedge {b}\in {B}\right)\right)\to \left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)$
29 simplrr ${⊢}\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({a}\in {A}\wedge {b}\in {B}\right)\right)\to {Z}\ne {U}$
30 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}$
31 30 sseld ${⊢}\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({a}\in {A}\to {a}\in {D}\right)$
32 simpl ${⊢}\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 \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)$
33 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}$
34 32 4 6 8 33 syl13anc ${⊢}\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}$
35 34 sseld ${⊢}\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({b}\in {B}\to {b}\in {D}\right)$
36 31 35 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({a}\in {A}\wedge {b}\in {B}\right)\to \left({a}\in {D}\wedge {b}\in {D}\right)\right)$
37 36 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({a}\in {A}\wedge {b}\in {B}\right)\right)\to \left({a}\in {D}\wedge {b}\in {D}\right)$
38 1 2 axcontlem7 ${⊢}\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({a}\in {D}\wedge {b}\in {D}\right)\right)\to \left({a}\mathrm{Btwn}⟨{Z},{b}⟩↔{F}\left({a}\right)\le {F}\left({b}\right)\right)$
39 28 29 37 38 syl21anc ${⊢}\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({a}\in {A}\wedge {b}\in {B}\right)\right)\to \left({a}\mathrm{Btwn}⟨{Z},{b}⟩↔{F}\left({a}\right)\le {F}\left({b}\right)\right)$
40 24 39 mpbid ${⊢}\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({a}\in {A}\wedge {b}\in {B}\right)\right)\to {F}\left({a}\right)\le {F}\left({b}\right)$
41 breq12 ${⊢}\left({F}\left({a}\right)={n}\wedge {F}\left({b}\right)={m}\right)\to \left({F}\left({a}\right)\le {F}\left({b}\right)↔{n}\le {m}\right)$
42 40 41 syl5ibcom ${⊢}\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({a}\in {A}\wedge {b}\in {B}\right)\right)\to \left(\left({F}\left({a}\right)={n}\wedge {F}\left({b}\right)={m}\right)\to {n}\le {m}\right)$
43 42 rexlimdvva ${⊢}\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 {a}\in {A}\phantom{\rule{.4em}{0ex}}\exists {b}\in {B}\phantom{\rule{.4em}{0ex}}\left({F}\left({a}\right)={n}\wedge {F}\left({b}\right)={m}\right)\to {n}\le {m}\right)$
44 18 43 syl5bir ${⊢}\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(\exists {a}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({a}\right)={n}\wedge \exists {b}\in {B}\phantom{\rule{.4em}{0ex}}{F}\left({b}\right)={m}\right)\to {n}\le {m}\right)$
45 14 17 44 syl2and ${⊢}\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 {F}\left[{A}\right]\wedge {m}\in {F}\left[{B}\right]\right)\to {n}\le {m}\right)$
46 45 ralrimivv ${⊢}\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 {n}\in {F}\left[{A}\right]\phantom{\rule{.4em}{0ex}}\forall {m}\in {F}\left[{B}\right]\phantom{\rule{.4em}{0ex}}{n}\le {m}$