omsmolem

Description: Lemma for omsmo . (Contributed by NM, 30-Nov-2003) (Revised by David Abernethy, 1-Jan-2014)

		Ref	Expression
	Assertion	omsmolem	$⊢ y \in ω \to (((A \subseteq On \land F : ω ⟶ A) \land \forall x \in ω F (x) \in F (suc x)) \to (z \in y \to F (z) \in F (y)))$

Proof

Step	Hyp	Ref	Expression
1		eleq2	$⊢ y = \emptyset \to (z \in y \leftrightarrow z \in \emptyset)$
2		fveq2	$⊢ y = \emptyset \to F (y) = F (\emptyset)$
3	2	eleq2d	$⊢ y = \emptyset \to (F (z) \in F (y) \leftrightarrow F (z) \in F (\emptyset))$
4	1 3	imbi12d	$⊢ y = \emptyset \to ((z \in y \to F (z) \in F (y)) \leftrightarrow (z \in \emptyset \to F (z) \in F (\emptyset)))$
5		eleq2	$⊢ y = w \to (z \in y \leftrightarrow z \in w)$
6		fveq2	$⊢ y = w \to F (y) = F (w)$
7	6	eleq2d	$⊢ y = w \to (F (z) \in F (y) \leftrightarrow F (z) \in F (w))$
8	5 7	imbi12d	$⊢ y = w \to ((z \in y \to F (z) \in F (y)) \leftrightarrow (z \in w \to F (z) \in F (w)))$
9		eleq2	$⊢ y = suc w \to (z \in y \leftrightarrow z \in suc w)$
10		fveq2	$⊢ y = suc w \to F (y) = F (suc w)$
11	10	eleq2d	$⊢ y = suc w \to (F (z) \in F (y) \leftrightarrow F (z) \in F (suc w))$
12	9 11	imbi12d	$⊢ y = suc w \to ((z \in y \to F (z) \in F (y)) \leftrightarrow (z \in suc w \to F (z) \in F (suc w)))$
13		noel	$⊢ \neg z \in \emptyset$
14	13	pm2.21i	$⊢ z \in \emptyset \to F (z) \in F (\emptyset)$
15	14	a1i	$⊢ ((A \subseteq On \land F : ω ⟶ A) \land \forall x \in ω F (x) \in F (suc x)) \to (z \in \emptyset \to F (z) \in F (\emptyset))$
16		vex	$⊢ z \in V$
17	16	elsuc	$⊢ z \in suc w \leftrightarrow (z \in w \lor z = w)$
18		fveq2	$⊢ x = w \to F (x) = F (w)$
19		suceq	$⊢ x = w \to suc x = suc w$
20	19	fveq2d	$⊢ x = w \to F (suc x) = F (suc w)$
21	18 20	eleq12d	$⊢ x = w \to (F (x) \in F (suc x) \leftrightarrow F (w) \in F (suc w))$
22	21	rspccva	$⊢ (\forall x \in ω F (x) \in F (suc x) \land w \in ω) \to F (w) \in F (suc w)$
23	22	adantll	$⊢ (((A \subseteq On \land F : ω ⟶ A) \land \forall x \in ω F (x) \in F (suc x)) \land w \in ω) \to F (w) \in F (suc w)$
24		peano2b	$⊢ w \in ω \leftrightarrow suc w \in ω$
25		ffvelrn	$⊢ (F : ω ⟶ A \land suc w \in ω) \to F (suc w) \in A$
26	24 25	sylan2b	$⊢ (F : ω ⟶ A \land w \in ω) \to F (suc w) \in A$
27		ssel	$⊢ A \subseteq On \to (F (suc w) \in A \to F (suc w) \in On)$
28		ontr1	$⊢ F (suc w) \in On \to ((F (z) \in F (w) \land F (w) \in F (suc w)) \to F (z) \in F (suc w))$
29	28	expcomd	$⊢ F (suc w) \in On \to (F (w) \in F (suc w) \to (F (z) \in F (w) \to F (z) \in F (suc w)))$
30	26 27 29	syl56	$⊢ A \subseteq On \to ((F : ω ⟶ A \land w \in ω) \to (F (w) \in F (suc w) \to (F (z) \in F (w) \to F (z) \in F (suc w))))$
31	30	impl	$⊢ ((A \subseteq On \land F : ω ⟶ A) \land w \in ω) \to (F (w) \in F (suc w) \to (F (z) \in F (w) \to F (z) \in F (suc w)))$
32	31	adantlr	$⊢ (((A \subseteq On \land F : ω ⟶ A) \land \forall x \in ω F (x) \in F (suc x)) \land w \in ω) \to (F (w) \in F (suc w) \to (F (z) \in F (w) \to F (z) \in F (suc w)))$
33	23 32	mpd	$⊢ (((A \subseteq On \land F : ω ⟶ A) \land \forall x \in ω F (x) \in F (suc x)) \land w \in ω) \to (F (z) \in F (w) \to F (z) \in F (suc w))$
34	33	imim2d	$⊢ (((A \subseteq On \land F : ω ⟶ A) \land \forall x \in ω F (x) \in F (suc x)) \land w \in ω) \to ((z \in w \to F (z) \in F (w)) \to (z \in w \to F (z) \in F (suc w)))$
35	34	imp	$⊢ ((((A \subseteq On \land F : ω ⟶ A) \land \forall x \in ω F (x) \in F (suc x)) \land w \in ω) \land (z \in w \to F (z) \in F (w))) \to (z \in w \to F (z) \in F (suc w))$
36		fveq2	$⊢ z = w \to F (z) = F (w)$
37	36	eleq1d	$⊢ z = w \to (F (z) \in F (suc w) \leftrightarrow F (w) \in F (suc w))$
38	22 37	syl5ibrcom	$⊢ (\forall x \in ω F (x) \in F (suc x) \land w \in ω) \to (z = w \to F (z) \in F (suc w))$
39	38	ad4ant23	$⊢ ((((A \subseteq On \land F : ω ⟶ A) \land \forall x \in ω F (x) \in F (suc x)) \land w \in ω) \land (z \in w \to F (z) \in F (w))) \to (z = w \to F (z) \in F (suc w))$
40	35 39	jaod	$⊢ ((((A \subseteq On \land F : ω ⟶ A) \land \forall x \in ω F (x) \in F (suc x)) \land w \in ω) \land (z \in w \to F (z) \in F (w))) \to ((z \in w \lor z = w) \to F (z) \in F (suc w))$
41	17 40	syl5bi	$⊢ ((((A \subseteq On \land F : ω ⟶ A) \land \forall x \in ω F (x) \in F (suc x)) \land w \in ω) \land (z \in w \to F (z) \in F (w))) \to (z \in suc w \to F (z) \in F (suc w))$
42	41	exp31	$⊢ ((A \subseteq On \land F : ω ⟶ A) \land \forall x \in ω F (x) \in F (suc x)) \to (w \in ω \to ((z \in w \to F (z) \in F (w)) \to (z \in suc w \to F (z) \in F (suc w))))$
43	42	com12	$⊢ w \in ω \to (((A \subseteq On \land F : ω ⟶ A) \land \forall x \in ω F (x) \in F (suc x)) \to ((z \in w \to F (z) \in F (w)) \to (z \in suc w \to F (z) \in F (suc w))))$
44	4 8 12 15 43	finds2	$⊢ y \in ω \to (((A \subseteq On \land F : ω ⟶ A) \land \forall x \in ω F (x) \in F (suc x)) \to (z \in y \to F (z) \in F (y)))$

Metamath Proof Explorer

Theorem omsmolem

Proof