zorn2lem4

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	zorn2lem4	$⊢ (R Po A \land w We A) \to \exists x \in On D = \emptyset$

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		pm3.24	$⊢ \neg (ran F \in V \land \neg ran F \in V)$
5		df-ne	$⊢ D \neq \emptyset \leftrightarrow \neg D = \emptyset$
6	5	ralbii	$⊢ \forall x \in On D \neq \emptyset \leftrightarrow \forall x \in On \neg D = \emptyset$
7		df-ral	$⊢ \forall x \in On D \neq \emptyset \leftrightarrow \forall x (x \in On \to D \neq \emptyset)$
8		ralnex	$⊢ \forall x \in On \neg D = \emptyset \leftrightarrow \neg \exists x \in On D = \emptyset$
9	6 7 8	3bitr3i	$⊢ \forall x (x \in On \to D \neq \emptyset) \leftrightarrow \neg \exists x \in On D = \emptyset$
10		weso	$⊢ w We A \to w Or A$
11	10	adantr	$⊢ (w We A \land \forall x (x \in On \to D \neq \emptyset)) \to w Or A$
12		vex	$⊢ w \in V$
13		soex	$⊢ (w Or A \land w \in V) \to A \in V$
14	11 12 13	sylancl	$⊢ (w We A \land \forall x (x \in On \to D \neq \emptyset)) \to A \in V$
15	1	tfr1	$⊢ F Fn On$
16		fvelrnb	$⊢ F Fn On \to (y \in ran F \leftrightarrow \exists x \in On F (x) = y)$
17	15 16	ax-mp	$⊢ y \in ran F \leftrightarrow \exists x \in On F (x) = y$
18		nfv	$⊢ Ⅎ x w We A$
19		nfa1	$⊢ Ⅎ x \forall x (x \in On \to D \neq \emptyset)$
20	18 19	nfan	$⊢ Ⅎ x (w We A \land \forall x (x \in On \to D \neq \emptyset))$
21		nfv	$⊢ Ⅎ x y \in A$
22	3	ssrab3	$⊢ D \subseteq A$
23	1 2 3	zorn2lem1	$⊢ (x \in On \land (w We A \land D \neq \emptyset)) \to F (x) \in D$
24	22 23	sselid	$⊢ (x \in On \land (w We A \land D \neq \emptyset)) \to F (x) \in A$
25		eleq1	$⊢ F (x) = y \to (F (x) \in A \leftrightarrow y \in A)$
26	24 25	syl5ibcom	$⊢ (x \in On \land (w We A \land D \neq \emptyset)) \to (F (x) = y \to y \in A)$
27	26	exp32	$⊢ x \in On \to (w We A \to (D \neq \emptyset \to (F (x) = y \to y \in A)))$
28	27	com12	$⊢ w We A \to (x \in On \to (D \neq \emptyset \to (F (x) = y \to y \in A)))$
29	28	a2d	$⊢ w We A \to ((x \in On \to D \neq \emptyset) \to (x \in On \to (F (x) = y \to y \in A)))$
30	29	spsd	$⊢ w We A \to (\forall x (x \in On \to D \neq \emptyset) \to (x \in On \to (F (x) = y \to y \in A)))$
31	30	imp	$⊢ (w We A \land \forall x (x \in On \to D \neq \emptyset)) \to (x \in On \to (F (x) = y \to y \in A))$
32	20 21 31	rexlimd	$⊢ (w We A \land \forall x (x \in On \to D \neq \emptyset)) \to (\exists x \in On F (x) = y \to y \in A)$
33	17 32	biimtrid	$⊢ (w We A \land \forall x (x \in On \to D \neq \emptyset)) \to (y \in ran F \to y \in A)$
34	33	ssrdv	$⊢ (w We A \land \forall x (x \in On \to D \neq \emptyset)) \to ran F \subseteq A$
35	14 34	ssexd	$⊢ (w We A \land \forall x (x \in On \to D \neq \emptyset)) \to ran F \in V$
36	35	ex	$⊢ w We A \to (\forall x (x \in On \to D \neq \emptyset) \to ran F \in V)$
37	36	adantl	$⊢ (R Po A \land w We A) \to (\forall x (x \in On \to D \neq \emptyset) \to ran F \in V)$
38	1 2 3	zorn2lem3	$⊢ (R Po A \land (x \in On \land (w We A \land D \neq \emptyset))) \to (y \in x \to \neg F (x) = F (y))$
39	38	exp45	$⊢ R Po A \to (x \in On \to (w We A \to (D \neq \emptyset \to (y \in x \to \neg F (x) = F (y)))))$
40	39	com23	$⊢ R Po A \to (w We A \to (x \in On \to (D \neq \emptyset \to (y \in x \to \neg F (x) = F (y)))))$
41	40	imp	$⊢ (R Po A \land w We A) \to (x \in On \to (D \neq \emptyset \to (y \in x \to \neg F (x) = F (y))))$
42	41	a2d	$⊢ (R Po A \land w We A) \to ((x \in On \to D \neq \emptyset) \to (x \in On \to (y \in x \to \neg F (x) = F (y))))$
43	42	imp4a	$⊢ (R Po A \land w We A) \to ((x \in On \to D \neq \emptyset) \to ((x \in On \land y \in x) \to \neg F (x) = F (y)))$
44	43	alrimdv	$⊢ (R Po A \land w We A) \to ((x \in On \to D \neq \emptyset) \to \forall y ((x \in On \land y \in x) \to \neg F (x) = F (y)))$
45	44	alimdv	$⊢ (R Po A \land w We A) \to (\forall x (x \in On \to D \neq \emptyset) \to \forall x \forall y ((x \in On \land y \in x) \to \neg F (x) = F (y)))$
46		r2al	$⊢ \forall x \in On \forall y \in x \neg F (x) = F (y) \leftrightarrow \forall x \forall y ((x \in On \land y \in x) \to \neg F (x) = F (y))$
47	45 46	syl6ibr	$⊢ (R Po A \land w We A) \to (\forall x (x \in On \to D \neq \emptyset) \to \forall x \in On \forall y \in x \neg F (x) = F (y))$
48		ssid	$⊢ On \subseteq On$
49	15	tz7.48lem	$⊢ (On \subseteq On \land \forall x \in On \forall y \in x \neg F (x) = F (y)) \to Fun {({F ↾}_{On})}^{-1}$
50	48 49	mpan	$⊢ \forall x \in On \forall y \in x \neg F (x) = F (y) \to Fun {({F ↾}_{On})}^{-1}$
51		fnrel	$⊢ F Fn On \to Rel F$
52	15 51	ax-mp	$⊢ Rel F$
53	15	fndmi	$⊢ dom F = On$
54	53	eqimssi	$⊢ dom F \subseteq On$
55		relssres	$⊢ (Rel F \land dom F \subseteq On) \to {F ↾}_{On} = F$
56	52 54 55	mp2an	$⊢ {F ↾}_{On} = F$
57	56	cnveqi	$⊢ {({F ↾}_{On})}^{-1} = F^{-1}$
58	57	funeqi	$⊢ Fun {({F ↾}_{On})}^{-1} \leftrightarrow Fun F^{-1}$
59	50 58	sylib	$⊢ \forall x \in On \forall y \in x \neg F (x) = F (y) \to Fun F^{-1}$
60	47 59	syl6	$⊢ (R Po A \land w We A) \to (\forall x (x \in On \to D \neq \emptyset) \to Fun F^{-1})$
61		onprc	$⊢ \neg On \in V$
62		funrnex	$⊢ dom F^{-1} \in V \to (Fun F^{-1} \to ran F^{-1} \in V)$
63	62	com12	$⊢ Fun F^{-1} \to (dom F^{-1} \in V \to ran F^{-1} \in V)$
64		df-rn	$⊢ ran F = dom F^{-1}$
65	64	eleq1i	$⊢ ran F \in V \leftrightarrow dom F^{-1} \in V$
66		dfdm4	$⊢ dom F = ran F^{-1}$
67	53 66	eqtr3i	$⊢ On = ran F^{-1}$
68	67	eleq1i	$⊢ On \in V \leftrightarrow ran F^{-1} \in V$
69	63 65 68	3imtr4g	$⊢ Fun F^{-1} \to (ran F \in V \to On \in V)$
70	61 69	mtoi	$⊢ Fun F^{-1} \to \neg ran F \in V$
71	60 70	syl6	$⊢ (R Po A \land w We A) \to (\forall x (x \in On \to D \neq \emptyset) \to \neg ran F \in V)$
72	37 71	jcad	$⊢ (R Po A \land w We A) \to (\forall x (x \in On \to D \neq \emptyset) \to (ran F \in V \land \neg ran F \in V))$
73	9 72	biimtrrid	$⊢ (R Po A \land w We A) \to (\neg \exists x \in On D = \emptyset \to (ran F \in V \land \neg ran F \in V))$
74	4 73	mt3i	$⊢ (R Po A \land w We A) \to \exists x \in On D = \emptyset$

Metamath Proof Explorer

Theorem zorn2lem4

Proof