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 = \{p \in 𝔼 (N) \| (U Btwn ⟨Z, p⟩ \lor p Btwn ⟨Z, U⟩)\}$
	axcontlem10.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	axcontlem10	$⊢ ((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 b \in 𝔼 (N) \forall x \in A \forall y \in B b Btwn ⟨x, y⟩$

Proof

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

Metamath Proof Explorer

Theorem axcontlem10

Proof