zorn2lem1

Description: Lemma for zorn2 . (Contributed by NM, 3-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\}$
Assertion	zorn2lem1	$⊢ (x \in On \land (w We A \land D \neq \emptyset)) \to F (x) \in D$

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	1	tfr2	$⊢ x \in On \to F (x) = (f \in V ⟼ (ι v \in C \| \forall u \in C \neg u w v)) ({F ↾}_{x})$
5	4	adantr	$⊢ (x \in On \land (w We A \land D \neq \emptyset)) \to F (x) = (f \in V ⟼ (ι v \in C \| \forall u \in C \neg u w v)) ({F ↾}_{x})$
6	1	tfr1	$⊢ F Fn On$
7		fnfun	$⊢ F Fn On \to Fun F$
8	6 7	ax-mp	$⊢ Fun F$
9		vex	$⊢ x \in V$
10		resfunexg	$⊢ (Fun F \land x \in V) \to {F ↾}_{x} \in V$
11	8 9 10	mp2an	$⊢ {F ↾}_{x} \in V$
12		rneq	$⊢ f = {F ↾}_{x} \to ran f = ran ({F ↾}_{x})$
13		df-ima	$⊢ F [x] = ran ({F ↾}_{x})$
14	12 13	syl6eqr	$⊢ f = {F ↾}_{x} \to ran f = F [x]$
15	14	eleq2d	$⊢ f = {F ↾}_{x} \to (g \in ran f \leftrightarrow g \in F [x])$
16	15	imbi1d	$⊢ f = {F ↾}_{x} \to ((g \in ran f \to g R z) \leftrightarrow (g \in F [x] \to g R z))$
17	16	ralbidv2	$⊢ f = {F ↾}_{x} \to (\forall g \in ran f g R z \leftrightarrow \forall g \in F [x] g R z)$
18	17	rabbidv	$⊢ f = {F ↾}_{x} \to \{z \in A \| \forall g \in ran f g R z\} = \{z \in A \| \forall g \in F [x] g R z\}$
19	18 2 3	3eqtr4g	$⊢ f = {F ↾}_{x} \to C = D$
20	19	eleq2d	$⊢ f = {F ↾}_{x} \to (u \in C \leftrightarrow u \in D)$
21	20	imbi1d	$⊢ f = {F ↾}_{x} \to ((u \in C \to \neg u w v) \leftrightarrow (u \in D \to \neg u w v))$
22	21	ralbidv2	$⊢ f = {F ↾}_{x} \to (\forall u \in C \neg u w v \leftrightarrow \forall u \in D \neg u w v)$
23	19 22	riotaeqbidv	$⊢ f = {F ↾}_{x} \to (ι v \in C \| \forall u \in C \neg u w v) = (ι v \in D \| \forall u \in D \neg u w v)$
24		eqid	$⊢ (f \in V ⟼ (ι v \in C \| \forall u \in C \neg u w v)) = (f \in V ⟼ (ι v \in C \| \forall u \in C \neg u w v))$
25		riotaex	$⊢ (ι v \in D \| \forall u \in D \neg u w v) \in V$
26	23 24 25	fvmpt	$⊢ {F ↾}_{x} \in V \to (f \in V ⟼ (ι v \in C \| \forall u \in C \neg u w v)) ({F ↾}_{x}) = (ι v \in D \| \forall u \in D \neg u w v)$
27	11 26	ax-mp	$⊢ (f \in V ⟼ (ι v \in C \| \forall u \in C \neg u w v)) ({F ↾}_{x}) = (ι v \in D \| \forall u \in D \neg u w v)$
28	5 27	syl6eq	$⊢ (x \in On \land (w We A \land D \neq \emptyset)) \to F (x) = (ι v \in D \| \forall u \in D \neg u w v)$
29		simprl	$⊢ (x \in On \land (w We A \land D \neq \emptyset)) \to w We A$
30		weso	$⊢ w We A \to w Or A$
31	30	ad2antrl	$⊢ (x \in On \land (w We A \land D \neq \emptyset)) \to w Or A$
32		vex	$⊢ w \in V$
33		soex	$⊢ (w Or A \land w \in V) \to A \in V$
34	31 32 33	sylancl	$⊢ (x \in On \land (w We A \land D \neq \emptyset)) \to A \in V$
35	3 34	rabexd	$⊢ (x \in On \land (w We A \land D \neq \emptyset)) \to D \in V$
36	3	ssrab3	$⊢ D \subseteq A$
37	36	a1i	$⊢ (x \in On \land (w We A \land D \neq \emptyset)) \to D \subseteq A$
38		simprr	$⊢ (x \in On \land (w We A \land D \neq \emptyset)) \to D \neq \emptyset$
39		wereu	$⊢ (w We A \land (D \in V \land D \subseteq A \land D \neq \emptyset)) \to \exists! v \in D \forall u \in D \neg u w v$
40	29 35 37 38 39	syl13anc	$⊢ (x \in On \land (w We A \land D \neq \emptyset)) \to \exists! v \in D \forall u \in D \neg u w v$
41		riotacl	$⊢ \exists! v \in D \forall u \in D \neg u w v \to (ι v \in D \| \forall u \in D \neg u w v) \in D$
42	40 41	syl	$⊢ (x \in On \land (w We A \land D \neq \emptyset)) \to (ι v \in D \| \forall u \in D \neg u w v) \in D$
43	28 42	eqeltrd	$⊢ (x \in On \land (w We A \land D \neq \emptyset)) \to F (x) \in D$

Metamath Proof Explorer

Theorem zorn2lem1

Proof