unblem2

Description: Lemma for unbnn . The value of the function F belongs to the unbounded set of natural numbers A . (Contributed by NM, 3-Dec-2003)

		Ref	Expression
	Hypothesis	unblem.2	$⊢ F = {rec ((x \in V ⟼ ⋂ (A ∖ suc x)), ⋂ A) ↾}_{ω}$
	Assertion	unblem2	$⊢ (A \subseteq ω \land \forall w \in ω \exists v \in A w \in v) \to (z \in ω \to F (z) \in A)$

Proof

Step	Hyp	Ref	Expression
1		unblem.2	$⊢ F = {rec ((x \in V ⟼ ⋂ (A ∖ suc x)), ⋂ A) ↾}_{ω}$
2		fveq2	$⊢ z = \emptyset \to F (z) = F (\emptyset)$
3	2	eleq1d	$⊢ z = \emptyset \to (F (z) \in A \leftrightarrow F (\emptyset) \in A)$
4		fveq2	$⊢ z = u \to F (z) = F (u)$
5	4	eleq1d	$⊢ z = u \to (F (z) \in A \leftrightarrow F (u) \in A)$
6		fveq2	$⊢ z = suc u \to F (z) = F (suc u)$
7	6	eleq1d	$⊢ z = suc u \to (F (z) \in A \leftrightarrow F (suc u) \in A)$
8		omsson	$⊢ ω \subseteq On$
9		sstr	$⊢ (A \subseteq ω \land ω \subseteq On) \to A \subseteq On$
10	8 9	mpan2	$⊢ A \subseteq ω \to A \subseteq On$
11		peano1	$⊢ \emptyset \in ω$
12		eleq1	$⊢ w = \emptyset \to (w \in v \leftrightarrow \emptyset \in v)$
13	12	rexbidv	$⊢ w = \emptyset \to (\exists v \in A w \in v \leftrightarrow \exists v \in A \emptyset \in v)$
14	13	rspcv	$⊢ \emptyset \in ω \to (\forall w \in ω \exists v \in A w \in v \to \exists v \in A \emptyset \in v)$
15	11 14	ax-mp	$⊢ \forall w \in ω \exists v \in A w \in v \to \exists v \in A \emptyset \in v$
16		df-rex	$⊢ \exists v \in A \emptyset \in v \leftrightarrow \exists v (v \in A \land \emptyset \in v)$
17	15 16	sylib	$⊢ \forall w \in ω \exists v \in A w \in v \to \exists v (v \in A \land \emptyset \in v)$
18		exsimpl	$⊢ \exists v (v \in A \land \emptyset \in v) \to \exists v v \in A$
19	17 18	syl	$⊢ \forall w \in ω \exists v \in A w \in v \to \exists v v \in A$
20		n0	$⊢ A \neq \emptyset \leftrightarrow \exists v v \in A$
21	19 20	sylibr	$⊢ \forall w \in ω \exists v \in A w \in v \to A \neq \emptyset$
22		onint	$⊢ (A \subseteq On \land A \neq \emptyset) \to ⋂ A \in A$
23	10 21 22	syl2an	$⊢ (A \subseteq ω \land \forall w \in ω \exists v \in A w \in v) \to ⋂ A \in A$
24	1	fveq1i	$⊢ F (\emptyset) = ({rec ((x \in V ⟼ ⋂ (A ∖ suc x)), ⋂ A) ↾}_{ω}) (\emptyset)$
25		fr0g	$⊢ ⋂ A \in A \to ({rec ((x \in V ⟼ ⋂ (A ∖ suc x)), ⋂ A) ↾}_{ω}) (\emptyset) = ⋂ A$
26	24 25	eqtr2id	$⊢ ⋂ A \in A \to ⋂ A = F (\emptyset)$
27	26	eleq1d	$⊢ ⋂ A \in A \to (⋂ A \in A \leftrightarrow F (\emptyset) \in A)$
28	27	ibi	$⊢ ⋂ A \in A \to F (\emptyset) \in A$
29	23 28	syl	$⊢ (A \subseteq ω \land \forall w \in ω \exists v \in A w \in v) \to F (\emptyset) \in A$
30		unblem1	$⊢ ((A \subseteq ω \land \forall w \in ω \exists v \in A w \in v) \land F (u) \in A) \to ⋂ (A ∖ suc F (u)) \in A$
31		suceq	$⊢ y = x \to suc y = suc x$
32	31	difeq2d	$⊢ y = x \to A ∖ suc y = A ∖ suc x$
33	32	inteqd	$⊢ y = x \to ⋂ (A ∖ suc y) = ⋂ (A ∖ suc x)$
34		suceq	$⊢ y = F (u) \to suc y = suc F (u)$
35	34	difeq2d	$⊢ y = F (u) \to A ∖ suc y = A ∖ suc F (u)$
36	35	inteqd	$⊢ y = F (u) \to ⋂ (A ∖ suc y) = ⋂ (A ∖ suc F (u))$
37	1 33 36	frsucmpt2	$⊢ (u \in ω \land ⋂ (A ∖ suc F (u)) \in A) \to F (suc u) = ⋂ (A ∖ suc F (u))$
38	37	eqcomd	$⊢ (u \in ω \land ⋂ (A ∖ suc F (u)) \in A) \to ⋂ (A ∖ suc F (u)) = F (suc u)$
39	38	eleq1d	$⊢ (u \in ω \land ⋂ (A ∖ suc F (u)) \in A) \to (⋂ (A ∖ suc F (u)) \in A \leftrightarrow F (suc u) \in A)$
40	39	ex	$⊢ u \in ω \to (⋂ (A ∖ suc F (u)) \in A \to (⋂ (A ∖ suc F (u)) \in A \leftrightarrow F (suc u) \in A))$
41	40	ibd	$⊢ u \in ω \to (⋂ (A ∖ suc F (u)) \in A \to F (suc u) \in A)$
42	30 41	syl5	$⊢ u \in ω \to (((A \subseteq ω \land \forall w \in ω \exists v \in A w \in v) \land F (u) \in A) \to F (suc u) \in A)$
43	42	expd	$⊢ u \in ω \to ((A \subseteq ω \land \forall w \in ω \exists v \in A w \in v) \to (F (u) \in A \to F (suc u) \in A))$
44	3 5 7 29 43	finds2	$⊢ z \in ω \to ((A \subseteq ω \land \forall w \in ω \exists v \in A w \in v) \to F (z) \in A)$
45	44	com12	$⊢ (A \subseteq ω \land \forall w \in ω \exists v \in A w \in v) \to (z \in ω \to F (z) \in A)$

Metamath Proof Explorer

Theorem unblem2

Proof