Metamath Proof Explorer

Theorem axcontlem3

Description: Lemma for axcont . Given the separation assumption, B is a subset of D . (Contributed by Scott Fenton, 18-Jun-2013)

		Ref	Expression
	Hypothesis	axcontlem3.1	$⊢ D = \{p \in 𝔼 (N) \| (U Btwn ⟨Z, p⟩ \lor p Btwn ⟨Z, U⟩)\}$
	Assertion	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$

Proof

Step	Hyp	Ref	Expression
1		axcontlem3.1	$⊢ D = \{p \in 𝔼 (N) \| (U Btwn ⟨Z, p⟩ \lor p Btwn ⟨Z, U⟩)\}$
2		simplr2	$⊢ ((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 𝔼 (N)$
3		simpr2	$⊢ ((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 U \in A$
4	3	anim1i	$⊢ (((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)) \land p \in B) \to (U \in A \land p \in B)$
5		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 Z \neq U)) \to \forall x \in A \forall y \in B x Btwn ⟨Z, y⟩$
6	5	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 Z \neq U)) \land p \in B) \to \forall x \in A \forall y \in B x Btwn ⟨Z, y⟩$
7		breq1	$⊢ x = U \to (x Btwn ⟨Z, y⟩ \leftrightarrow U Btwn ⟨Z, y⟩)$
8		opeq2	$⊢ y = p \to ⟨Z, y⟩ = ⟨Z, p⟩$
9	8	breq2d	$⊢ y = p \to (U Btwn ⟨Z, y⟩ \leftrightarrow U Btwn ⟨Z, p⟩)$
10	7 9	rspc2v	$⊢ (U \in A \land p \in B) \to (\forall x \in A \forall y \in B x Btwn ⟨Z, y⟩ \to U Btwn ⟨Z, p⟩)$
11	4 6 10	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 Z \neq U)) \land p \in B) \to U Btwn ⟨Z, p⟩$
12	11	orcd	$⊢ (((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)) \land p \in B) \to (U Btwn ⟨Z, p⟩ \lor p Btwn ⟨Z, U⟩)$
13	12	ralrimiva	$⊢ ((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 \forall p \in B (U Btwn ⟨Z, p⟩ \lor p Btwn ⟨Z, U⟩)$
14	1	sseq2i	$⊢ B \subseteq D \leftrightarrow B \subseteq \{p \in 𝔼 (N) \| (U Btwn ⟨Z, p⟩ \lor p Btwn ⟨Z, U⟩)\}$
15		ssrab	$⊢ B \subseteq \{p \in 𝔼 (N) \| (U Btwn ⟨Z, p⟩ \lor p Btwn ⟨Z, U⟩)\} \leftrightarrow (B \subseteq 𝔼 (N) \land \forall p \in B (U Btwn ⟨Z, p⟩ \lor p Btwn ⟨Z, U⟩))$
16	14 15	bitri	$⊢ B \subseteq D \leftrightarrow (B \subseteq 𝔼 (N) \land \forall p \in B (U Btwn ⟨Z, p⟩ \lor p Btwn ⟨Z, U⟩))$
17	2 13 16	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 Z \neq U)) \to B \subseteq D$