unblem1

Description: Lemma for unbnn . After removing the successor of an element from an unbounded set of natural numbers, the intersection of the result belongs to the original unbounded set. (Contributed by NM, 3-Dec-2003)

		Ref	Expression
	Assertion	unblem1	$⊢ ((B \subseteq ω \land \forall x \in ω \exists y \in B x \in y) \land A \in B) \to ⋂ (B ∖ suc A) \in B$

Proof

Step	Hyp	Ref	Expression
1		omsson	$⊢ ω \subseteq On$
2		sstr	$⊢ (B \subseteq ω \land ω \subseteq On) \to B \subseteq On$
3	1 2	mpan2	$⊢ B \subseteq ω \to B \subseteq On$
4	3	ssdifssd	$⊢ B \subseteq ω \to B ∖ suc A \subseteq On$
5	4	ad2antrr	$⊢ ((B \subseteq ω \land \forall x \in ω \exists y \in B x \in y) \land A \in B) \to B ∖ suc A \subseteq On$
6		ssel	$⊢ B \subseteq ω \to (A \in B \to A \in ω)$
7		peano2b	$⊢ A \in ω \leftrightarrow suc A \in ω$
8	6 7	syl6ib	$⊢ B \subseteq ω \to (A \in B \to suc A \in ω)$
9		eleq1	$⊢ x = suc A \to (x \in y \leftrightarrow suc A \in y)$
10	9	rexbidv	$⊢ x = suc A \to (\exists y \in B x \in y \leftrightarrow \exists y \in B suc A \in y)$
11	10	rspccva	$⊢ (\forall x \in ω \exists y \in B x \in y \land suc A \in ω) \to \exists y \in B suc A \in y$
12		ssel	$⊢ B \subseteq ω \to (y \in B \to y \in ω)$
13		nnord	$⊢ y \in ω \to Ord y$
14		ordn2lp	$⊢ Ord y \to \neg (y \in suc A \land suc A \in y)$
15		imnan	$⊢ (y \in suc A \to \neg suc A \in y) \leftrightarrow \neg (y \in suc A \land suc A \in y)$
16	14 15	sylibr	$⊢ Ord y \to (y \in suc A \to \neg suc A \in y)$
17	16	con2d	$⊢ Ord y \to (suc A \in y \to \neg y \in suc A)$
18	13 17	syl	$⊢ y \in ω \to (suc A \in y \to \neg y \in suc A)$
19	12 18	syl6	$⊢ B \subseteq ω \to (y \in B \to (suc A \in y \to \neg y \in suc A))$
20	19	imdistand	$⊢ B \subseteq ω \to ((y \in B \land suc A \in y) \to (y \in B \land \neg y \in suc A))$
21		eldif	$⊢ y \in (B ∖ suc A) \leftrightarrow (y \in B \land \neg y \in suc A)$
22		ne0i	$⊢ y \in (B ∖ suc A) \to B ∖ suc A \neq \emptyset$
23	21 22	sylbir	$⊢ (y \in B \land \neg y \in suc A) \to B ∖ suc A \neq \emptyset$
24	20 23	syl6	$⊢ B \subseteq ω \to ((y \in B \land suc A \in y) \to B ∖ suc A \neq \emptyset)$
25	24	expd	$⊢ B \subseteq ω \to (y \in B \to (suc A \in y \to B ∖ suc A \neq \emptyset))$
26	25	rexlimdv	$⊢ B \subseteq ω \to (\exists y \in B suc A \in y \to B ∖ suc A \neq \emptyset)$
27	11 26	syl5	$⊢ B \subseteq ω \to ((\forall x \in ω \exists y \in B x \in y \land suc A \in ω) \to B ∖ suc A \neq \emptyset)$
28	8 27	sylan2d	$⊢ B \subseteq ω \to ((\forall x \in ω \exists y \in B x \in y \land A \in B) \to B ∖ suc A \neq \emptyset)$
29	28	impl	$⊢ ((B \subseteq ω \land \forall x \in ω \exists y \in B x \in y) \land A \in B) \to B ∖ suc A \neq \emptyset$
30		onint	$⊢ (B ∖ suc A \subseteq On \land B ∖ suc A \neq \emptyset) \to ⋂ (B ∖ suc A) \in (B ∖ suc A)$
31	5 29 30	syl2anc	$⊢ ((B \subseteq ω \land \forall x \in ω \exists y \in B x \in y) \land A \in B) \to ⋂ (B ∖ suc A) \in (B ∖ suc A)$
32	31	eldifad	$⊢ ((B \subseteq ω \land \forall x \in ω \exists y \in B x \in y) \land A \in B) \to ⋂ (B ∖ suc A) \in B$

Metamath Proof Explorer

Theorem unblem1

Proof