zorn2lem7

Description: Lemma for zorn2 . (Contributed by NM, 6-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	zorn2lem7	$⊢ (A \in dom card \land R Po A \land \forall s ((s \subseteq A \land R Or s) \to \exists a \in A \forall r \in s (r R a \lor r = a))) \to \exists a \in A \forall b \in A \neg a R b$

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		ween	$⊢ A \in dom card \leftrightarrow \exists w w We A$
6	1 2 3	zorn2lem4	$⊢ (R Po A \land w We A) \to \exists x \in On D = \emptyset$
7		imaeq2	$⊢ x = y \to F [x] = F [y]$
8	7	raleqdv	$⊢ x = y \to (\forall g \in F [x] g R z \leftrightarrow \forall g \in F [y] g R z)$
9	8	rabbidv	$⊢ x = y \to \{z \in A \| \forall g \in F [x] g R z\} = \{z \in A \| \forall g \in F [y] g R z\}$
10	9 3 4	3eqtr4g	$⊢ x = y \to D = H$
11	10	eqeq1d	$⊢ x = y \to (D = \emptyset \leftrightarrow H = \emptyset)$
12	11	onminex	$⊢ \exists x \in On D = \emptyset \to \exists x \in On (D = \emptyset \land \forall y \in x \neg H = \emptyset)$
13		df-ne	$⊢ H \neq \emptyset \leftrightarrow \neg H = \emptyset$
14	13	ralbii	$⊢ \forall y \in x H \neq \emptyset \leftrightarrow \forall y \in x \neg H = \emptyset$
15	14	anbi2i	$⊢ (D = \emptyset \land \forall y \in x H \neq \emptyset) \leftrightarrow (D = \emptyset \land \forall y \in x \neg H = \emptyset)$
16	15	rexbii	$⊢ \exists x \in On (D = \emptyset \land \forall y \in x H \neq \emptyset) \leftrightarrow \exists x \in On (D = \emptyset \land \forall y \in x \neg H = \emptyset)$
17	12 16	sylibr	$⊢ \exists x \in On D = \emptyset \to \exists x \in On (D = \emptyset \land \forall y \in x H \neq \emptyset)$
18	1 2 3 4	zorn2lem5	$⊢ ((w We A \land x \in On) \land \forall y \in x H \neq \emptyset) \to F [x] \subseteq A$
19	18	a1i	$⊢ R Po A \to (((w We A \land x \in On) \land \forall y \in x H \neq \emptyset) \to F [x] \subseteq A)$
20	1 2 3 4	zorn2lem6	$⊢ R Po A \to (((w We A \land x \in On) \land \forall y \in x H \neq \emptyset) \to R Or F [x])$
21	19 20	jcad	$⊢ R Po A \to (((w We A \land x \in On) \land \forall y \in x H \neq \emptyset) \to (F [x] \subseteq A \land R Or F [x]))$
22	1	tfr1	$⊢ F Fn On$
23		fnfun	$⊢ F Fn On \to Fun F$
24		vex	$⊢ x \in V$
25	24	funimaex	$⊢ Fun F \to F [x] \in V$
26	22 23 25	mp2b	$⊢ F [x] \in V$
27		sseq1	$⊢ s = F [x] \to (s \subseteq A \leftrightarrow F [x] \subseteq A)$
28		soeq2	$⊢ s = F [x] \to (R Or s \leftrightarrow R Or F [x])$
29	27 28	anbi12d	$⊢ s = F [x] \to ((s \subseteq A \land R Or s) \leftrightarrow (F [x] \subseteq A \land R Or F [x]))$
30		raleq	$⊢ s = F [x] \to (\forall r \in s (r R a \lor r = a) \leftrightarrow \forall r \in F [x] (r R a \lor r = a))$
31	30	rexbidv	$⊢ s = F [x] \to (\exists a \in A \forall r \in s (r R a \lor r = a) \leftrightarrow \exists a \in A \forall r \in F [x] (r R a \lor r = a))$
32	29 31	imbi12d	$⊢ s = F [x] \to (((s \subseteq A \land R Or s) \to \exists a \in A \forall r \in s (r R a \lor r = a)) \leftrightarrow ((F [x] \subseteq A \land R Or F [x]) \to \exists a \in A \forall r \in F [x] (r R a \lor r = a)))$
33	26 32	spcv	$⊢ \forall s ((s \subseteq A \land R Or s) \to \exists a \in A \forall r \in s (r R a \lor r = a)) \to ((F [x] \subseteq A \land R Or F [x]) \to \exists a \in A \forall r \in F [x] (r R a \lor r = a))$
34	21 33	sylan9	$⊢ (R Po A \land \forall s ((s \subseteq A \land R Or s) \to \exists a \in A \forall r \in s (r R a \lor r = a))) \to (((w We A \land x \in On) \land \forall y \in x H \neq \emptyset) \to \exists a \in A \forall r \in F [x] (r R a \lor r = a))$
35	34	adantld	$⊢ (R Po A \land \forall s ((s \subseteq A \land R Or s) \to \exists a \in A \forall r \in s (r R a \lor r = a))) \to ((D = \emptyset \land ((w We A \land x \in On) \land \forall y \in x H \neq \emptyset)) \to \exists a \in A \forall r \in F [x] (r R a \lor r = a))$
36	35	imp	$⊢ ((R Po A \land \forall s ((s \subseteq A \land R Or s) \to \exists a \in A \forall r \in s (r R a \lor r = a))) \land (D = \emptyset \land ((w We A \land x \in On) \land \forall y \in x H \neq \emptyset))) \to \exists a \in A \forall r \in F [x] (r R a \lor r = a)$
37		noel	$⊢ \neg b \in \emptyset$
38	18	sseld	$⊢ ((w We A \land x \in On) \land \forall y \in x H \neq \emptyset) \to (r \in F [x] \to r \in A)$
39		3anass	$⊢ (r \in A \land a \in A \land b \in A) \leftrightarrow (r \in A \land (a \in A \land b \in A))$
40		potr	$⊢ (R Po A \land (r \in A \land a \in A \land b \in A)) \to ((r R a \land a R b) \to r R b)$
41	39 40	sylan2br	$⊢ (R Po A \land (r \in A \land (a \in A \land b \in A))) \to ((r R a \land a R b) \to r R b)$
42	41	expcomd	$⊢ (R Po A \land (r \in A \land (a \in A \land b \in A))) \to (a R b \to (r R a \to r R b))$
43	42	imp	$⊢ ((R Po A \land (r \in A \land (a \in A \land b \in A))) \land a R b) \to (r R a \to r R b)$
44		breq1	$⊢ r = a \to (r R b \leftrightarrow a R b)$
45	44	biimprcd	$⊢ a R b \to (r = a \to r R b)$
46	45	adantl	$⊢ ((R Po A \land (r \in A \land (a \in A \land b \in A))) \land a R b) \to (r = a \to r R b)$
47	43 46	jaod	$⊢ ((R Po A \land (r \in A \land (a \in A \land b \in A))) \land a R b) \to ((r R a \lor r = a) \to r R b)$
48	47	exp42	$⊢ R Po A \to (r \in A \to ((a \in A \land b \in A) \to (a R b \to ((r R a \lor r = a) \to r R b))))$
49	38 48	sylan9r	$⊢ (R Po A \land ((w We A \land x \in On) \land \forall y \in x H \neq \emptyset)) \to (r \in F [x] \to ((a \in A \land b \in A) \to (a R b \to ((r R a \lor r = a) \to r R b))))$
50	49	com24	$⊢ (R Po A \land ((w We A \land x \in On) \land \forall y \in x H \neq \emptyset)) \to (a R b \to ((a \in A \land b \in A) \to (r \in F [x] \to ((r R a \lor r = a) \to r R b))))$
51	50	com23	$⊢ (R Po A \land ((w We A \land x \in On) \land \forall y \in x H \neq \emptyset)) \to ((a \in A \land b \in A) \to (a R b \to (r \in F [x] \to ((r R a \lor r = a) \to r R b))))$
52	51	imp31	$⊢ (((R Po A \land ((w We A \land x \in On) \land \forall y \in x H \neq \emptyset)) \land (a \in A \land b \in A)) \land a R b) \to (r \in F [x] \to ((r R a \lor r = a) \to r R b))$
53	52	a2d	$⊢ (((R Po A \land ((w We A \land x \in On) \land \forall y \in x H \neq \emptyset)) \land (a \in A \land b \in A)) \land a R b) \to ((r \in F [x] \to (r R a \lor r = a)) \to (r \in F [x] \to r R b))$
54	53	ralimdv2	$⊢ (((R Po A \land ((w We A \land x \in On) \land \forall y \in x H \neq \emptyset)) \land (a \in A \land b \in A)) \land a R b) \to (\forall r \in F [x] (r R a \lor r = a) \to \forall r \in F [x] r R b)$
55		breq1	$⊢ r = g \to (r R b \leftrightarrow g R b)$
56	55	cbvralvw	$⊢ \forall r \in F [x] r R b \leftrightarrow \forall g \in F [x] g R b$
57		breq2	$⊢ z = b \to (g R z \leftrightarrow g R b)$
58	57	ralbidv	$⊢ z = b \to (\forall g \in F [x] g R z \leftrightarrow \forall g \in F [x] g R b)$
59	58	elrab	$⊢ b \in \{z \in A \| \forall g \in F [x] g R z\} \leftrightarrow (b \in A \land \forall g \in F [x] g R b)$
60	3	eqeq1i	$⊢ D = \emptyset \leftrightarrow \{z \in A \| \forall g \in F [x] g R z\} = \emptyset$
61		eleq2	$⊢ \{z \in A \| \forall g \in F [x] g R z\} = \emptyset \to (b \in \{z \in A \| \forall g \in F [x] g R z\} \leftrightarrow b \in \emptyset)$
62	60 61	sylbi	$⊢ D = \emptyset \to (b \in \{z \in A \| \forall g \in F [x] g R z\} \leftrightarrow b \in \emptyset)$
63	59 62	bitr3id	$⊢ D = \emptyset \to ((b \in A \land \forall g \in F [x] g R b) \leftrightarrow b \in \emptyset)$
64	63	biimpd	$⊢ D = \emptyset \to ((b \in A \land \forall g \in F [x] g R b) \to b \in \emptyset)$
65	64	expdimp	$⊢ (D = \emptyset \land b \in A) \to (\forall g \in F [x] g R b \to b \in \emptyset)$
66	56 65	syl5bi	$⊢ (D = \emptyset \land b \in A) \to (\forall r \in F [x] r R b \to b \in \emptyset)$
67	54 66	sylan9r	$⊢ ((D = \emptyset \land b \in A) \land (((R Po A \land ((w We A \land x \in On) \land \forall y \in x H \neq \emptyset)) \land (a \in A \land b \in A)) \land a R b)) \to (\forall r \in F [x] (r R a \lor r = a) \to b \in \emptyset)$
68	67	exp32	$⊢ (D = \emptyset \land b \in A) \to (((R Po A \land ((w We A \land x \in On) \land \forall y \in x H \neq \emptyset)) \land (a \in A \land b \in A)) \to (a R b \to (\forall r \in F [x] (r R a \lor r = a) \to b \in \emptyset)))$
69	68	com34	$⊢ (D = \emptyset \land b \in A) \to (((R Po A \land ((w We A \land x \in On) \land \forall y \in x H \neq \emptyset)) \land (a \in A \land b \in A)) \to (\forall r \in F [x] (r R a \lor r = a) \to (a R b \to b \in \emptyset)))$
70	69	imp31	$⊢ (((D = \emptyset \land b \in A) \land ((R Po A \land ((w We A \land x \in On) \land \forall y \in x H \neq \emptyset)) \land (a \in A \land b \in A))) \land \forall r \in F [x] (r R a \lor r = a)) \to (a R b \to b \in \emptyset)$
71	37 70	mtoi	$⊢ (((D = \emptyset \land b \in A) \land ((R Po A \land ((w We A \land x \in On) \land \forall y \in x H \neq \emptyset)) \land (a \in A \land b \in A))) \land \forall r \in F [x] (r R a \lor r = a)) \to \neg a R b$
72	71	exp42	$⊢ (D = \emptyset \land b \in A) \to ((R Po A \land ((w We A \land x \in On) \land \forall y \in x H \neq \emptyset)) \to ((a \in A \land b \in A) \to (\forall r \in F [x] (r R a \lor r = a) \to \neg a R b)))$
73	72	exp4a	$⊢ (D = \emptyset \land b \in A) \to ((R Po A \land ((w We A \land x \in On) \land \forall y \in x H \neq \emptyset)) \to (a \in A \to (b \in A \to (\forall r \in F [x] (r R a \lor r = a) \to \neg a R b))))$
74	73	com34	$⊢ (D = \emptyset \land b \in A) \to ((R Po A \land ((w We A \land x \in On) \land \forall y \in x H \neq \emptyset)) \to (b \in A \to (a \in A \to (\forall r \in F [x] (r R a \lor r = a) \to \neg a R b))))$
75	74	ex	$⊢ D = \emptyset \to (b \in A \to ((R Po A \land ((w We A \land x \in On) \land \forall y \in x H \neq \emptyset)) \to (b \in A \to (a \in A \to (\forall r \in F [x] (r R a \lor r = a) \to \neg a R b)))))$
76	75	com4r	$⊢ b \in A \to (D = \emptyset \to (b \in A \to ((R Po A \land ((w We A \land x \in On) \land \forall y \in x H \neq \emptyset)) \to (a \in A \to (\forall r \in F [x] (r R a \lor r = a) \to \neg a R b)))))$
77	76	pm2.43a	$⊢ b \in A \to (D = \emptyset \to ((R Po A \land ((w We A \land x \in On) \land \forall y \in x H \neq \emptyset)) \to (a \in A \to (\forall r \in F [x] (r R a \lor r = a) \to \neg a R b))))$
78	77	impd	$⊢ b \in A \to ((D = \emptyset \land (R Po A \land ((w We A \land x \in On) \land \forall y \in x H \neq \emptyset))) \to (a \in A \to (\forall r \in F [x] (r R a \lor r = a) \to \neg a R b)))$
79	78	com4l	$⊢ (D = \emptyset \land (R Po A \land ((w We A \land x \in On) \land \forall y \in x H \neq \emptyset))) \to (a \in A \to (\forall r \in F [x] (r R a \lor r = a) \to (b \in A \to \neg a R b)))$
80	79	impd	$⊢ (D = \emptyset \land (R Po A \land ((w We A \land x \in On) \land \forall y \in x H \neq \emptyset))) \to ((a \in A \land \forall r \in F [x] (r R a \lor r = a)) \to (b \in A \to \neg a R b))$
81	80	ralrimdv	$⊢ (D = \emptyset \land (R Po A \land ((w We A \land x \in On) \land \forall y \in x H \neq \emptyset))) \to ((a \in A \land \forall r \in F [x] (r R a \lor r = a)) \to \forall b \in A \neg a R b)$
82	81	expd	$⊢ (D = \emptyset \land (R Po A \land ((w We A \land x \in On) \land \forall y \in x H \neq \emptyset))) \to (a \in A \to (\forall r \in F [x] (r R a \lor r = a) \to \forall b \in A \neg a R b))$
83	82	reximdvai	$⊢ (D = \emptyset \land (R Po A \land ((w We A \land x \in On) \land \forall y \in x H \neq \emptyset))) \to (\exists a \in A \forall r \in F [x] (r R a \lor r = a) \to \exists a \in A \forall b \in A \neg a R b)$
84	83	exp32	$⊢ D = \emptyset \to (R Po A \to (((w We A \land x \in On) \land \forall y \in x H \neq \emptyset) \to (\exists a \in A \forall r \in F [x] (r R a \lor r = a) \to \exists a \in A \forall b \in A \neg a R b)))$
85	84	com12	$⊢ R Po A \to (D = \emptyset \to (((w We A \land x \in On) \land \forall y \in x H \neq \emptyset) \to (\exists a \in A \forall r \in F [x] (r R a \lor r = a) \to \exists a \in A \forall b \in A \neg a R b)))$
86	85	adantr	$⊢ (R Po A \land \forall s ((s \subseteq A \land R Or s) \to \exists a \in A \forall r \in s (r R a \lor r = a))) \to (D = \emptyset \to (((w We A \land x \in On) \land \forall y \in x H \neq \emptyset) \to (\exists a \in A \forall r \in F [x] (r R a \lor r = a) \to \exists a \in A \forall b \in A \neg a R b)))$
87	86	imp32	$⊢ ((R Po A \land \forall s ((s \subseteq A \land R Or s) \to \exists a \in A \forall r \in s (r R a \lor r = a))) \land (D = \emptyset \land ((w We A \land x \in On) \land \forall y \in x H \neq \emptyset))) \to (\exists a \in A \forall r \in F [x] (r R a \lor r = a) \to \exists a \in A \forall b \in A \neg a R b)$
88	36 87	mpd	$⊢ ((R Po A \land \forall s ((s \subseteq A \land R Or s) \to \exists a \in A \forall r \in s (r R a \lor r = a))) \land (D = \emptyset \land ((w We A \land x \in On) \land \forall y \in x H \neq \emptyset))) \to \exists a \in A \forall b \in A \neg a R b$
89	88	exp45	$⊢ (R Po A \land \forall s ((s \subseteq A \land R Or s) \to \exists a \in A \forall r \in s (r R a \lor r = a))) \to (D = \emptyset \to ((w We A \land x \in On) \to (\forall y \in x H \neq \emptyset \to \exists a \in A \forall b \in A \neg a R b)))$
90	89	com23	$⊢ (R Po A \land \forall s ((s \subseteq A \land R Or s) \to \exists a \in A \forall r \in s (r R a \lor r = a))) \to ((w We A \land x \in On) \to (D = \emptyset \to (\forall y \in x H \neq \emptyset \to \exists a \in A \forall b \in A \neg a R b)))$
91	90	expdimp	$⊢ ((R Po A \land \forall s ((s \subseteq A \land R Or s) \to \exists a \in A \forall r \in s (r R a \lor r = a))) \land w We A) \to (x \in On \to (D = \emptyset \to (\forall y \in x H \neq \emptyset \to \exists a \in A \forall b \in A \neg a R b)))$
92	91	imp4a	$⊢ ((R Po A \land \forall s ((s \subseteq A \land R Or s) \to \exists a \in A \forall r \in s (r R a \lor r = a))) \land w We A) \to (x \in On \to ((D = \emptyset \land \forall y \in x H \neq \emptyset) \to \exists a \in A \forall b \in A \neg a R b))$
93	92	com3l	$⊢ x \in On \to ((D = \emptyset \land \forall y \in x H \neq \emptyset) \to (((R Po A \land \forall s ((s \subseteq A \land R Or s) \to \exists a \in A \forall r \in s (r R a \lor r = a))) \land w We A) \to \exists a \in A \forall b \in A \neg a R b))$
94	93	rexlimiv	$⊢ \exists x \in On (D = \emptyset \land \forall y \in x H \neq \emptyset) \to (((R Po A \land \forall s ((s \subseteq A \land R Or s) \to \exists a \in A \forall r \in s (r R a \lor r = a))) \land w We A) \to \exists a \in A \forall b \in A \neg a R b)$
95	6 17 94	3syl	$⊢ (R Po A \land w We A) \to (((R Po A \land \forall s ((s \subseteq A \land R Or s) \to \exists a \in A \forall r \in s (r R a \lor r = a))) \land w We A) \to \exists a \in A \forall b \in A \neg a R b)$
96	95	adantlr	$⊢ ((R Po A \land \forall s ((s \subseteq A \land R Or s) \to \exists a \in A \forall r \in s (r R a \lor r = a))) \land w We A) \to (((R Po A \land \forall s ((s \subseteq A \land R Or s) \to \exists a \in A \forall r \in s (r R a \lor r = a))) \land w We A) \to \exists a \in A \forall b \in A \neg a R b)$
97	96	pm2.43i	$⊢ ((R Po A \land \forall s ((s \subseteq A \land R Or s) \to \exists a \in A \forall r \in s (r R a \lor r = a))) \land w We A) \to \exists a \in A \forall b \in A \neg a R b$
98	97	expcom	$⊢ w We A \to ((R Po A \land \forall s ((s \subseteq A \land R Or s) \to \exists a \in A \forall r \in s (r R a \lor r = a))) \to \exists a \in A \forall b \in A \neg a R b)$
99	98	exlimiv	$⊢ \exists w w We A \to ((R Po A \land \forall s ((s \subseteq A \land R Or s) \to \exists a \in A \forall r \in s (r R a \lor r = a))) \to \exists a \in A \forall b \in A \neg a R b)$
100	5 99	sylbi	$⊢ A \in dom card \to ((R Po A \land \forall s ((s \subseteq A \land R Or s) \to \exists a \in A \forall r \in s (r R a \lor r = a))) \to \exists a \in A \forall b \in A \neg a R b)$
101	100	3impib	$⊢ (A \in dom card \land R Po A \land \forall s ((s \subseteq A \land R Or s) \to \exists a \in A \forall r \in s (r R a \lor r = a))) \to \exists a \in A \forall b \in A \neg a R b$

Metamath Proof Explorer

Theorem zorn2lem7

Proof