axcontlem12

Description: Lemma for axcont . Eliminate the trivial cases from the previous lemmas. (Contributed by Scott Fenton, 20-Jun-2013)

		Ref	Expression
	Assertion	axcontlem12	$⊢ ((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)) \to \exists b \in 𝔼 (N) \forall x \in A \forall y \in B b Btwn ⟨x, y⟩$

Proof

Step	Hyp	Ref	Expression
1		rzal	$⊢ B = \emptyset \to \forall y \in B Z Btwn ⟨x, y⟩$
2	1	ralrimivw	$⊢ B = \emptyset \to \forall x \in A \forall y \in B Z Btwn ⟨x, y⟩$
3		breq1	$⊢ b = Z \to (b Btwn ⟨x, y⟩ \leftrightarrow Z Btwn ⟨x, y⟩)$
4	3	2ralbidv	$⊢ b = Z \to (\forall x \in A \forall y \in B b Btwn ⟨x, y⟩ \leftrightarrow \forall x \in A \forall y \in B Z Btwn ⟨x, y⟩)$
5	4	rspcev	$⊢ (Z \in 𝔼 (N) \land \forall x \in A \forall y \in B Z Btwn ⟨x, y⟩) \to \exists b \in 𝔼 (N) \forall x \in A \forall y \in B b Btwn ⟨x, y⟩$
6	5	expcom	$⊢ \forall x \in A \forall y \in B Z Btwn ⟨x, y⟩ \to (Z \in 𝔼 (N) \to \exists b \in 𝔼 (N) \forall x \in A \forall y \in B b Btwn ⟨x, y⟩)$
7	2 6	syl	$⊢ B = \emptyset \to (Z \in 𝔼 (N) \to \exists b \in 𝔼 (N) \forall x \in A \forall y \in B b Btwn ⟨x, y⟩)$
8	7	adantld	$⊢ B = \emptyset \to (((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)) \to \exists b \in 𝔼 (N) \forall x \in A \forall y \in B b Btwn ⟨x, y⟩)$
9	8	adantld	$⊢ B = \emptyset \to (((u \in A \land Z \neq u) \land ((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))) \to \exists b \in 𝔼 (N) \forall x \in A \forall y \in B b Btwn ⟨x, y⟩)$
10		simprrl	$⊢ (B \neq \emptyset \land ((u \in A \land Z \neq u) \land ((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)))) \to (N \in ℕ \land (A \subseteq 𝔼 (N) \land B \subseteq 𝔼 (N) \land \forall x \in A \forall y \in B x Btwn ⟨Z, y⟩))$
11		simprrr	$⊢ (B \neq \emptyset \land ((u \in A \land Z \neq u) \land ((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)))) \to Z \in 𝔼 (N)$
12		simprll	$⊢ (B \neq \emptyset \land ((u \in A \land Z \neq u) \land ((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)))) \to u \in A$
13		simpl	$⊢ (B \neq \emptyset \land ((u \in A \land Z \neq u) \land ((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)))) \to B \neq \emptyset$
14	11 12 13	3jca	$⊢ (B \neq \emptyset \land ((u \in A \land Z \neq u) \land ((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)))) \to (Z \in 𝔼 (N) \land u \in A \land B \neq \emptyset)$
15		simprlr	$⊢ (B \neq \emptyset \land ((u \in A \land Z \neq u) \land ((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)))) \to Z \neq u$
16		axcontlem11	$⊢ ((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⟩$
17	10 14 15 16	syl12anc	$⊢ (B \neq \emptyset \land ((u \in A \land Z \neq u) \land ((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)))) \to \exists b \in 𝔼 (N) \forall x \in A \forall y \in B b Btwn ⟨x, y⟩$
18	17	ex	$⊢ B \neq \emptyset \to (((u \in A \land Z \neq u) \land ((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))) \to \exists b \in 𝔼 (N) \forall x \in A \forall y \in B b Btwn ⟨x, y⟩)$
19	9 18	pm2.61ine	$⊢ ((u \in A \land Z \neq u) \land ((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))) \to \exists b \in 𝔼 (N) \forall x \in A \forall y \in B b Btwn ⟨x, y⟩$
20	19	ex	$⊢ (u \in A \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⟩)) \land Z \in 𝔼 (N)) \to \exists b \in 𝔼 (N) \forall x \in A \forall y \in B b Btwn ⟨x, y⟩)$
21	20	rexlimiva	$⊢ \exists u \in A 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⟩)) \land Z \in 𝔼 (N)) \to \exists b \in 𝔼 (N) \forall x \in A \forall y \in B b Btwn ⟨x, y⟩)$
22		df-ne	$⊢ Z \neq u \leftrightarrow \neg Z = u$
23	22	con2bii	$⊢ Z = u \leftrightarrow \neg Z \neq u$
24	23	ralbii	$⊢ \forall u \in A Z = u \leftrightarrow \forall u \in A \neg Z \neq u$
25		ralnex	$⊢ \forall u \in A \neg Z \neq u \leftrightarrow \neg \exists u \in A Z \neq u$
26	24 25	bitri	$⊢ \forall u \in A Z = u \leftrightarrow \neg \exists u \in A Z \neq u$
27		simpr3	$⊢ (N \in ℕ \land (A \subseteq 𝔼 (N) \land B \subseteq 𝔼 (N) \land \forall x \in A \forall y \in B x Btwn ⟨Z, y⟩)) \to \forall x \in A \forall y \in B x Btwn ⟨Z, y⟩$
28		eqeq2	$⊢ u = x \to (Z = u \leftrightarrow Z = x)$
29	28	rspccva	$⊢ (\forall u \in A Z = u \land x \in A) \to Z = x$
30		opeq1	$⊢ Z = x \to ⟨Z, y⟩ = ⟨x, y⟩$
31	30	breq2d	$⊢ Z = x \to (x Btwn ⟨Z, y⟩ \leftrightarrow x Btwn ⟨x, y⟩)$
32		breq1	$⊢ Z = x \to (Z Btwn ⟨x, y⟩ \leftrightarrow x Btwn ⟨x, y⟩)$
33	31 32	bitr4d	$⊢ Z = x \to (x Btwn ⟨Z, y⟩ \leftrightarrow Z Btwn ⟨x, y⟩)$
34	33	ralbidv	$⊢ Z = x \to (\forall y \in B x Btwn ⟨Z, y⟩ \leftrightarrow \forall y \in B Z Btwn ⟨x, y⟩)$
35	29 34	syl	$⊢ (\forall u \in A Z = u \land x \in A) \to (\forall y \in B x Btwn ⟨Z, y⟩ \leftrightarrow \forall y \in B Z Btwn ⟨x, y⟩)$
36	35	ralbidva	$⊢ \forall u \in A Z = u \to (\forall x \in A \forall y \in B x Btwn ⟨Z, y⟩ \leftrightarrow \forall x \in A \forall y \in B Z Btwn ⟨x, y⟩)$
37	36	biimpa	$⊢ (\forall u \in A Z = u \land \forall x \in A \forall y \in B x Btwn ⟨Z, y⟩) \to \forall x \in A \forall y \in B Z Btwn ⟨x, y⟩$
38	27 37	sylan2	$⊢ (\forall u \in A Z = u \land (N \in ℕ \land (A \subseteq 𝔼 (N) \land B \subseteq 𝔼 (N) \land \forall x \in A \forall y \in B x Btwn ⟨Z, y⟩))) \to \forall x \in A \forall y \in B Z Btwn ⟨x, y⟩$
39	38 5	sylan2	$⊢ (Z \in 𝔼 (N) \land (\forall u \in A Z = u \land (N \in ℕ \land (A \subseteq 𝔼 (N) \land B \subseteq 𝔼 (N) \land \forall x \in A \forall y \in B x Btwn ⟨Z, y⟩)))) \to \exists b \in 𝔼 (N) \forall x \in A \forall y \in B b Btwn ⟨x, y⟩$
40	39	ancoms	$⊢ ((\forall u \in A Z = u \land (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)) \to \exists b \in 𝔼 (N) \forall x \in A \forall y \in B b Btwn ⟨x, y⟩$
41	40	expl	$⊢ \forall u \in A Z = 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⟩)) \land Z \in 𝔼 (N)) \to \exists b \in 𝔼 (N) \forall x \in A \forall y \in B b Btwn ⟨x, y⟩)$
42	26 41	sylbir	$⊢ \neg \exists u \in A 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⟩)) \land Z \in 𝔼 (N)) \to \exists b \in 𝔼 (N) \forall x \in A \forall y \in B b Btwn ⟨x, y⟩)$
43	21 42	pm2.61i	$⊢ ((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)) \to \exists b \in 𝔼 (N) \forall x \in A \forall y \in B b Btwn ⟨x, y⟩$

Metamath Proof Explorer

Theorem axcontlem12

Proof