unblem3

Description: Lemma for unbnn . The value of the function F is less than its value at a successor. (Contributed by NM, 3-Dec-2003)

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

Proof

Step	Hyp	Ref	Expression
1		unblem.2	$⊢ F = {rec ((x \in V ⟼ ⋂ (A ∖ suc x)), ⋂ A) ↾}_{ω}$
2	1	unblem2	$⊢ (A \subseteq ω \land \forall w \in ω \exists v \in A w \in v) \to (z \in ω \to F (z) \in A)$
3	2	imp	$⊢ ((A \subseteq ω \land \forall w \in ω \exists v \in A w \in v) \land z \in ω) \to F (z) \in A$
4		omsson	$⊢ ω \subseteq On$
5		sstr	$⊢ (A \subseteq ω \land ω \subseteq On) \to A \subseteq On$
6	4 5	mpan2	$⊢ A \subseteq ω \to A \subseteq On$
7		ssel	$⊢ A \subseteq On \to (F (z) \in A \to F (z) \in On)$
8	7	anc2li	$⊢ A \subseteq On \to (F (z) \in A \to (A \subseteq On \land F (z) \in On))$
9	6 8	syl	$⊢ A \subseteq ω \to (F (z) \in A \to (A \subseteq On \land F (z) \in On))$
10	9	ad2antrr	$⊢ ((A \subseteq ω \land \forall w \in ω \exists v \in A w \in v) \land z \in ω) \to (F (z) \in A \to (A \subseteq On \land F (z) \in On))$
11	3 10	mpd	$⊢ ((A \subseteq ω \land \forall w \in ω \exists v \in A w \in v) \land z \in ω) \to (A \subseteq On \land F (z) \in On)$
12		onmindif	$⊢ (A \subseteq On \land F (z) \in On) \to F (z) \in ⋂ (A ∖ suc F (z))$
13	11 12	syl	$⊢ ((A \subseteq ω \land \forall w \in ω \exists v \in A w \in v) \land z \in ω) \to F (z) \in ⋂ (A ∖ suc F (z))$
14		unblem1	$⊢ ((A \subseteq ω \land \forall w \in ω \exists v \in A w \in v) \land F (z) \in A) \to ⋂ (A ∖ suc F (z)) \in A$
15	14	ex	$⊢ (A \subseteq ω \land \forall w \in ω \exists v \in A w \in v) \to (F (z) \in A \to ⋂ (A ∖ suc F (z)) \in A)$
16	2 15	syld	$⊢ (A \subseteq ω \land \forall w \in ω \exists v \in A w \in v) \to (z \in ω \to ⋂ (A ∖ suc F (z)) \in A)$
17		suceq	$⊢ y = x \to suc y = suc x$
18	17	difeq2d	$⊢ y = x \to A ∖ suc y = A ∖ suc x$
19	18	inteqd	$⊢ y = x \to ⋂ (A ∖ suc y) = ⋂ (A ∖ suc x)$
20		suceq	$⊢ y = F (z) \to suc y = suc F (z)$
21	20	difeq2d	$⊢ y = F (z) \to A ∖ suc y = A ∖ suc F (z)$
22	21	inteqd	$⊢ y = F (z) \to ⋂ (A ∖ suc y) = ⋂ (A ∖ suc F (z))$
23	1 19 22	frsucmpt2	$⊢ (z \in ω \land ⋂ (A ∖ suc F (z)) \in A) \to F (suc z) = ⋂ (A ∖ suc F (z))$
24	23	ex	$⊢ z \in ω \to (⋂ (A ∖ suc F (z)) \in A \to F (suc z) = ⋂ (A ∖ suc F (z)))$
25	16 24	sylcom	$⊢ (A \subseteq ω \land \forall w \in ω \exists v \in A w \in v) \to (z \in ω \to F (suc z) = ⋂ (A ∖ suc F (z)))$
26	25	imp	$⊢ ((A \subseteq ω \land \forall w \in ω \exists v \in A w \in v) \land z \in ω) \to F (suc z) = ⋂ (A ∖ suc F (z))$
27	13 26	eleqtrrd	$⊢ ((A \subseteq ω \land \forall w \in ω \exists v \in A w \in v) \land z \in ω) \to F (z) \in F (suc z)$
28	27	ex	$⊢ (A \subseteq ω \land \forall w \in ω \exists v \in A w \in v) \to (z \in ω \to F (z) \in F (suc z))$

Metamath Proof Explorer

Theorem unblem3

Proof