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 = \{p \in 𝔼 (N) \| (U Btwn ⟨Z, p⟩ \lor p Btwn ⟨Z, U⟩)\}$
	axcontlem9.2	$⊢ F = \{⟨x, t⟩ \| (x \in D \land (t \in [0, +∞) \land \forall i \in (1 \dots N) x (i) = (1 - t) Z (i) + t U (i)))\}$
Assertion	axcontlem9	$⊢ ((N \in ℕ \land (A \subseteq 𝔼 (N) \land B \subseteq 𝔼 (N) \land \forall x \in A \forall y \in B x Btwn ⟨Z, y⟩)) \land ((Z \in 𝔼 (N) \land U \in A \land B \neq \emptyset) \land Z \neq U)) \to \forall n \in F [A] \forall m \in F [B] n \leq m$

Proof

Step	Hyp	Ref	Expression
1		axcontlem9.1	$⊢ D = \{p \in 𝔼 (N) \| (U Btwn ⟨Z, p⟩ \lor p Btwn ⟨Z, U⟩)\}$
2		axcontlem9.2	$⊢ F = \{⟨x, t⟩ \| (x \in D \land (t \in [0, +∞) \land \forall i \in (1 \dots N) x (i) = (1 - t) Z (i) + t U (i)))\}$
3		simpll	$⊢ ((N \in ℕ \land (A \subseteq 𝔼 (N) \land B \subseteq 𝔼 (N) \land \forall x \in A \forall y \in B x Btwn ⟨Z, y⟩)) \land ((Z \in 𝔼 (N) \land U \in A \land B \neq \emptyset) \land Z \neq U)) \to N \in ℕ$
4		simprl1	$⊢ ((N \in ℕ \land (A \subseteq 𝔼 (N) \land B \subseteq 𝔼 (N) \land \forall x \in A \forall y \in B x Btwn ⟨Z, y⟩)) \land ((Z \in 𝔼 (N) \land U \in A \land B \neq \emptyset) \land Z \neq U)) \to Z \in 𝔼 (N)$
5		simplr1	$⊢ ((N \in ℕ \land (A \subseteq 𝔼 (N) \land B \subseteq 𝔼 (N) \land \forall x \in A \forall y \in B x Btwn ⟨Z, y⟩)) \land ((Z \in 𝔼 (N) \land U \in A \land B \neq \emptyset) \land Z \neq U)) \to A \subseteq 𝔼 (N)$
6		simprl2	$⊢ ((N \in ℕ \land (A \subseteq 𝔼 (N) \land B \subseteq 𝔼 (N) \land \forall x \in A \forall y \in B x Btwn ⟨Z, y⟩)) \land ((Z \in 𝔼 (N) \land U \in A \land B \neq \emptyset) \land Z \neq U)) \to U \in A$
7	5 6	sseldd	$⊢ ((N \in ℕ \land (A \subseteq 𝔼 (N) \land B \subseteq 𝔼 (N) \land \forall x \in A \forall y \in B x Btwn ⟨Z, y⟩)) \land ((Z \in 𝔼 (N) \land U \in A \land B \neq \emptyset) \land Z \neq U)) \to U \in 𝔼 (N)$
8		simprr	$⊢ ((N \in ℕ \land (A \subseteq 𝔼 (N) \land B \subseteq 𝔼 (N) \land \forall x \in A \forall y \in B x Btwn ⟨Z, y⟩)) \land ((Z \in 𝔼 (N) \land U \in A \land B \neq \emptyset) \land Z \neq U)) \to Z \neq U$
9	1 2	axcontlem2	$⊢ ((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \to F : D \underset{1-1 onto}{⟶} [0, +∞)$
10	3 4 7 8 9	syl31anc	$⊢ ((N \in ℕ \land (A \subseteq 𝔼 (N) \land B \subseteq 𝔼 (N) \land \forall x \in A \forall y \in B x Btwn ⟨Z, y⟩)) \land ((Z \in 𝔼 (N) \land U \in A \land B \neq \emptyset) \land Z \neq U)) \to F : D \underset{1-1 onto}{⟶} [0, +∞)$
11		f1ofun	$⊢ F : D \underset{1-1 onto}{⟶} [0, +∞) \to Fun F$
12		fvelima	$⊢ (Fun F \land n \in F [A]) \to \exists a \in A F (a) = n$
13	12	ex	$⊢ Fun F \to (n \in F [A] \to \exists a \in A F (a) = n)$
14	10 11 13	3syl	$⊢ ((N \in ℕ \land (A \subseteq 𝔼 (N) \land B \subseteq 𝔼 (N) \land \forall x \in A \forall y \in B x Btwn ⟨Z, y⟩)) \land ((Z \in 𝔼 (N) \land U \in A \land B \neq \emptyset) \land Z \neq U)) \to (n \in F [A] \to \exists a \in A F (a) = n)$
15		fvelima	$⊢ (Fun F \land m \in F [B]) \to \exists b \in B F (b) = m$
16	15	ex	$⊢ Fun F \to (m \in F [B] \to \exists b \in B F (b) = m)$
17	10 11 16	3syl	$⊢ ((N \in ℕ \land (A \subseteq 𝔼 (N) \land B \subseteq 𝔼 (N) \land \forall x \in A \forall y \in B x Btwn ⟨Z, y⟩)) \land ((Z \in 𝔼 (N) \land U \in A \land B \neq \emptyset) \land Z \neq U)) \to (m \in F [B] \to \exists b \in B F (b) = m)$
18		reeanv	$⊢ \exists a \in A \exists b \in B (F (a) = n \land F (b) = m) \leftrightarrow (\exists a \in A F (a) = n \land \exists b \in B F (b) = m)$
19		simplr3	$⊢ ((N \in ℕ \land (A \subseteq 𝔼 (N) \land B \subseteq 𝔼 (N) \land \forall x \in A \forall y \in B x Btwn ⟨Z, y⟩)) \land ((Z \in 𝔼 (N) \land U \in A \land B \neq \emptyset) \land Z \neq U)) \to \forall x \in A \forall y \in B x Btwn ⟨Z, y⟩$
20		breq1	$⊢ x = a \to (x Btwn ⟨Z, y⟩ \leftrightarrow a Btwn ⟨Z, y⟩)$
21		opeq2	$⊢ y = b \to ⟨Z, y⟩ = ⟨Z, b⟩$
22	21	breq2d	$⊢ y = b \to (a Btwn ⟨Z, y⟩ \leftrightarrow a Btwn ⟨Z, b⟩)$
23	20 22	rspc2v	$⊢ (a \in A \land b \in B) \to (\forall x \in A \forall y \in B x Btwn ⟨Z, y⟩ \to a Btwn ⟨Z, b⟩)$
24	19 23	mpan9	$⊢ (((N \in ℕ \land (A \subseteq 𝔼 (N) \land B \subseteq 𝔼 (N) \land \forall x \in A \forall y \in B x Btwn ⟨Z, y⟩)) \land ((Z \in 𝔼 (N) \land U \in A \land B \neq \emptyset) \land Z \neq U)) \land (a \in A \land b \in B)) \to a Btwn ⟨Z, b⟩$
25		simplll	$⊢ (((N \in ℕ \land (A \subseteq 𝔼 (N) \land B \subseteq 𝔼 (N) \land \forall x \in A \forall y \in B x Btwn ⟨Z, y⟩)) \land ((Z \in 𝔼 (N) \land U \in A \land B \neq \emptyset) \land Z \neq U)) \land (a \in A \land b \in B)) \to N \in ℕ$
26	4	adantr	$⊢ (((N \in ℕ \land (A \subseteq 𝔼 (N) \land B \subseteq 𝔼 (N) \land \forall x \in A \forall y \in B x Btwn ⟨Z, y⟩)) \land ((Z \in 𝔼 (N) \land U \in A \land B \neq \emptyset) \land Z \neq U)) \land (a \in A \land b \in B)) \to Z \in 𝔼 (N)$
27	7	adantr	$⊢ (((N \in ℕ \land (A \subseteq 𝔼 (N) \land B \subseteq 𝔼 (N) \land \forall x \in A \forall y \in B x Btwn ⟨Z, y⟩)) \land ((Z \in 𝔼 (N) \land U \in A \land B \neq \emptyset) \land Z \neq U)) \land (a \in A \land b \in B)) \to U \in 𝔼 (N)$
28	25 26 27	3jca	$⊢ (((N \in ℕ \land (A \subseteq 𝔼 (N) \land B \subseteq 𝔼 (N) \land \forall x \in A \forall y \in B x Btwn ⟨Z, y⟩)) \land ((Z \in 𝔼 (N) \land U \in A \land B \neq \emptyset) \land Z \neq U)) \land (a \in A \land b \in B)) \to (N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N))$
29		simplrr	$⊢ (((N \in ℕ \land (A \subseteq 𝔼 (N) \land B \subseteq 𝔼 (N) \land \forall x \in A \forall y \in B x Btwn ⟨Z, y⟩)) \land ((Z \in 𝔼 (N) \land U \in A \land B \neq \emptyset) \land Z \neq U)) \land (a \in A \land b \in B)) \to Z \neq U$
30	1	axcontlem4	$⊢ ((N \in ℕ \land (A \subseteq 𝔼 (N) \land B \subseteq 𝔼 (N) \land \forall x \in A \forall y \in B x Btwn ⟨Z, y⟩)) \land ((Z \in 𝔼 (N) \land U \in A \land B \neq \emptyset) \land Z \neq U)) \to A \subseteq D$
31	30	sseld	$⊢ ((N \in ℕ \land (A \subseteq 𝔼 (N) \land B \subseteq 𝔼 (N) \land \forall x \in A \forall y \in B x Btwn ⟨Z, y⟩)) \land ((Z \in 𝔼 (N) \land U \in A \land B \neq \emptyset) \land Z \neq U)) \to (a \in A \to a \in D)$
32		simpl	$⊢ ((N \in ℕ \land (A \subseteq 𝔼 (N) \land B \subseteq 𝔼 (N) \land \forall x \in A \forall y \in B x Btwn ⟨Z, y⟩)) \land ((Z \in 𝔼 (N) \land U \in A \land B \neq \emptyset) \land Z \neq U)) \to (N \in ℕ \land (A \subseteq 𝔼 (N) \land B \subseteq 𝔼 (N) \land \forall x \in A \forall y \in B x Btwn ⟨Z, y⟩))$
33	1	axcontlem3	$⊢ ((N \in ℕ \land (A \subseteq 𝔼 (N) \land B \subseteq 𝔼 (N) \land \forall x \in A \forall y \in B x Btwn ⟨Z, y⟩)) \land (Z \in 𝔼 (N) \land U \in A \land Z \neq U)) \to B \subseteq D$
34	32 4 6 8 33	syl13anc	$⊢ ((N \in ℕ \land (A \subseteq 𝔼 (N) \land B \subseteq 𝔼 (N) \land \forall x \in A \forall y \in B x Btwn ⟨Z, y⟩)) \land ((Z \in 𝔼 (N) \land U \in A \land B \neq \emptyset) \land Z \neq U)) \to B \subseteq D$
35	34	sseld	$⊢ ((N \in ℕ \land (A \subseteq 𝔼 (N) \land B \subseteq 𝔼 (N) \land \forall x \in A \forall y \in B x Btwn ⟨Z, y⟩)) \land ((Z \in 𝔼 (N) \land U \in A \land B \neq \emptyset) \land Z \neq U)) \to (b \in B \to b \in D)$
36	31 35	anim12d	$⊢ ((N \in ℕ \land (A \subseteq 𝔼 (N) \land B \subseteq 𝔼 (N) \land \forall x \in A \forall y \in B x Btwn ⟨Z, y⟩)) \land ((Z \in 𝔼 (N) \land U \in A \land B \neq \emptyset) \land Z \neq U)) \to ((a \in A \land b \in B) \to (a \in D \land b \in D))$
37	36	imp	$⊢ (((N \in ℕ \land (A \subseteq 𝔼 (N) \land B \subseteq 𝔼 (N) \land \forall x \in A \forall y \in B x Btwn ⟨Z, y⟩)) \land ((Z \in 𝔼 (N) \land U \in A \land B \neq \emptyset) \land Z \neq U)) \land (a \in A \land b \in B)) \to (a \in D \land b \in D)$
38	1 2	axcontlem7	$⊢ (((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (a \in D \land b \in D)) \to (a Btwn ⟨Z, b⟩ \leftrightarrow F (a) \leq F (b))$
39	28 29 37 38	syl21anc	$⊢ (((N \in ℕ \land (A \subseteq 𝔼 (N) \land B \subseteq 𝔼 (N) \land \forall x \in A \forall y \in B x Btwn ⟨Z, y⟩)) \land ((Z \in 𝔼 (N) \land U \in A \land B \neq \emptyset) \land Z \neq U)) \land (a \in A \land b \in B)) \to (a Btwn ⟨Z, b⟩ \leftrightarrow F (a) \leq F (b))$
40	24 39	mpbid	$⊢ (((N \in ℕ \land (A \subseteq 𝔼 (N) \land B \subseteq 𝔼 (N) \land \forall x \in A \forall y \in B x Btwn ⟨Z, y⟩)) \land ((Z \in 𝔼 (N) \land U \in A \land B \neq \emptyset) \land Z \neq U)) \land (a \in A \land b \in B)) \to F (a) \leq F (b)$
41		breq12	$⊢ (F (a) = n \land F (b) = m) \to (F (a) \leq F (b) \leftrightarrow n \leq m)$
42	40 41	syl5ibcom	$⊢ (((N \in ℕ \land (A \subseteq 𝔼 (N) \land B \subseteq 𝔼 (N) \land \forall x \in A \forall y \in B x Btwn ⟨Z, y⟩)) \land ((Z \in 𝔼 (N) \land U \in A \land B \neq \emptyset) \land Z \neq U)) \land (a \in A \land b \in B)) \to ((F (a) = n \land F (b) = m) \to n \leq m)$
43	42	rexlimdvva	$⊢ ((N \in ℕ \land (A \subseteq 𝔼 (N) \land B \subseteq 𝔼 (N) \land \forall x \in A \forall y \in B x Btwn ⟨Z, y⟩)) \land ((Z \in 𝔼 (N) \land U \in A \land B \neq \emptyset) \land Z \neq U)) \to (\exists a \in A \exists b \in B (F (a) = n \land F (b) = m) \to n \leq m)$
44	18 43	syl5bir	$⊢ ((N \in ℕ \land (A \subseteq 𝔼 (N) \land B \subseteq 𝔼 (N) \land \forall x \in A \forall y \in B x Btwn ⟨Z, y⟩)) \land ((Z \in 𝔼 (N) \land U \in A \land B \neq \emptyset) \land Z \neq U)) \to ((\exists a \in A F (a) = n \land \exists b \in B F (b) = m) \to n \leq m)$
45	14 17 44	syl2and	$⊢ ((N \in ℕ \land (A \subseteq 𝔼 (N) \land B \subseteq 𝔼 (N) \land \forall x \in A \forall y \in B x Btwn ⟨Z, y⟩)) \land ((Z \in 𝔼 (N) \land U \in A \land B \neq \emptyset) \land Z \neq U)) \to ((n \in F [A] \land m \in F [B]) \to n \leq m)$
46	45	ralrimivv	$⊢ ((N \in ℕ \land (A \subseteq 𝔼 (N) \land B \subseteq 𝔼 (N) \land \forall x \in A \forall y \in B x Btwn ⟨Z, y⟩)) \land ((Z \in 𝔼 (N) \land U \in A \land B \neq \emptyset) \land Z \neq U)) \to \forall n \in F [A] \forall m \in F [B] n \leq m$

Metamath Proof Explorer

Theorem axcontlem9

Proof