zorn2lem5

Description: Lemma for zorn2 . (Contributed by NM, 4-Apr-1997) (Revised by Mario Carneiro, 9-May-2015)

	Ref	Expression
Hypotheses	zorn2lem.3	$⊢ F = recs ((f \in V ⟼ (ι v \in C \| \forall u \in C \neg u w v)))$
	zorn2lem.4	$⊢ C = \{z \in A \| \forall g \in ran f g R z\}$
	zorn2lem.5	$⊢ D = \{z \in A \| \forall g \in F [x] g R z\}$
	zorn2lem.7	$⊢ H = \{z \in A \| \forall g \in F [y] g R z\}$
Assertion	zorn2lem5	$⊢ ((w We A \land x \in On) \land \forall y \in x H \neq \emptyset) \to F [x] \subseteq A$

Proof

Step	Hyp	Ref	Expression
1		zorn2lem.3	$⊢ F = recs ((f \in V ⟼ (ι v \in C \| \forall u \in C \neg u w v)))$
2		zorn2lem.4	$⊢ C = \{z \in A \| \forall g \in ran f g R z\}$
3		zorn2lem.5	$⊢ D = \{z \in A \| \forall g \in F [x] g R z\}$
4		zorn2lem.7	$⊢ H = \{z \in A \| \forall g \in F [y] g R z\}$
5	1	tfr1	$⊢ F Fn On$
6		fnfun	$⊢ F Fn On \to Fun F$
7	5 6	ax-mp	$⊢ Fun F$
8		fvelima	$⊢ (Fun F \land s \in F [x]) \to \exists y \in x F (y) = s$
9	7 8	mpan	$⊢ s \in F [x] \to \exists y \in x F (y) = s$
10		nfv	$⊢ Ⅎ y (w We A \land x \in On)$
11		nfra1	$⊢ Ⅎ y \forall y \in x H \neq \emptyset$
12	10 11	nfan	$⊢ Ⅎ y ((w We A \land x \in On) \land \forall y \in x H \neq \emptyset)$
13		nfv	$⊢ Ⅎ y s \in A$
14		df-ral	$⊢ \forall y \in x H \neq \emptyset \leftrightarrow \forall y (y \in x \to H \neq \emptyset)$
15		onelon	$⊢ (x \in On \land y \in x) \to y \in On$
16	4	ssrab3	$⊢ H \subseteq A$
17	1 2 4	zorn2lem1	$⊢ (y \in On \land (w We A \land H \neq \emptyset)) \to F (y) \in H$
18	16 17	sselid	$⊢ (y \in On \land (w We A \land H \neq \emptyset)) \to F (y) \in A$
19		eleq1	$⊢ F (y) = s \to (F (y) \in A \leftrightarrow s \in A)$
20	18 19	imbitrid	$⊢ F (y) = s \to ((y \in On \land (w We A \land H \neq \emptyset)) \to s \in A)$
21	15 20	sylani	$⊢ F (y) = s \to (((x \in On \land y \in x) \land (w We A \land H \neq \emptyset)) \to s \in A)$
22	21	com12	$⊢ ((x \in On \land y \in x) \land (w We A \land H \neq \emptyset)) \to (F (y) = s \to s \in A)$
23	22	exp43	$⊢ x \in On \to (y \in x \to (w We A \to (H \neq \emptyset \to (F (y) = s \to s \in A))))$
24	23	com3r	$⊢ w We A \to (x \in On \to (y \in x \to (H \neq \emptyset \to (F (y) = s \to s \in A))))$
25	24	imp	$⊢ (w We A \land x \in On) \to (y \in x \to (H \neq \emptyset \to (F (y) = s \to s \in A)))$
26	25	a2d	$⊢ (w We A \land x \in On) \to ((y \in x \to H \neq \emptyset) \to (y \in x \to (F (y) = s \to s \in A)))$
27	26	spsd	$⊢ (w We A \land x \in On) \to (\forall y (y \in x \to H \neq \emptyset) \to (y \in x \to (F (y) = s \to s \in A)))$
28	14 27	biimtrid	$⊢ (w We A \land x \in On) \to (\forall y \in x H \neq \emptyset \to (y \in x \to (F (y) = s \to s \in A)))$
29	28	imp	$⊢ ((w We A \land x \in On) \land \forall y \in x H \neq \emptyset) \to (y \in x \to (F (y) = s \to s \in A))$
30	12 13 29	rexlimd	$⊢ ((w We A \land x \in On) \land \forall y \in x H \neq \emptyset) \to (\exists y \in x F (y) = s \to s \in A)$
31	9 30	syl5	$⊢ ((w We A \land x \in On) \land \forall y \in x H \neq \emptyset) \to (s \in F [x] \to s \in A)$
32	31	ssrdv	$⊢ ((w We A \land x \in On) \land \forall y \in x H \neq \emptyset) \to F [x] \subseteq A$

Metamath Proof Explorer

Theorem zorn2lem5

Proof