zorn2lem6

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	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])$

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		poss	$⊢ F [x] \subseteq A \to (R Po A \to R Po F [x])$
6	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$
7	5 6	syl11	$⊢ R Po A \to (((w We A \land x \in On) \land \forall y \in x H \neq \emptyset) \to R Po F [x])$
8	1	tfr1	$⊢ F Fn On$
9		fnfun	$⊢ F Fn On \to Fun F$
10		fvelima	$⊢ (Fun F \land s \in F [x]) \to \exists b \in x F (b) = s$
11		df-rex	$⊢ \exists b \in x F (b) = s \leftrightarrow \exists b (b \in x \land F (b) = s)$
12	10 11	sylib	$⊢ (Fun F \land s \in F [x]) \to \exists b (b \in x \land F (b) = s)$
13	12	ex	$⊢ Fun F \to (s \in F [x] \to \exists b (b \in x \land F (b) = s))$
14		fvelima	$⊢ (Fun F \land r \in F [x]) \to \exists a \in x F (a) = r$
15		df-rex	$⊢ \exists a \in x F (a) = r \leftrightarrow \exists a (a \in x \land F (a) = r)$
16	14 15	sylib	$⊢ (Fun F \land r \in F [x]) \to \exists a (a \in x \land F (a) = r)$
17	16	ex	$⊢ Fun F \to (r \in F [x] \to \exists a (a \in x \land F (a) = r))$
18	13 17	anim12d	$⊢ Fun F \to ((s \in F [x] \land r \in F [x]) \to (\exists b (b \in x \land F (b) = s) \land \exists a (a \in x \land F (a) = r)))$
19	8 9 18	mp2b	$⊢ (s \in F [x] \land r \in F [x]) \to (\exists b (b \in x \land F (b) = s) \land \exists a (a \in x \land F (a) = r))$
20		an4	$⊢ ((b \in x \land a \in x) \land (F (b) = s \land F (a) = r)) \leftrightarrow ((b \in x \land F (b) = s) \land (a \in x \land F (a) = r))$
21	20	2exbii	$⊢ \exists b \exists a ((b \in x \land a \in x) \land (F (b) = s \land F (a) = r)) \leftrightarrow \exists b \exists a ((b \in x \land F (b) = s) \land (a \in x \land F (a) = r))$
22		exdistrv	$⊢ \exists b \exists a ((b \in x \land F (b) = s) \land (a \in x \land F (a) = r)) \leftrightarrow (\exists b (b \in x \land F (b) = s) \land \exists a (a \in x \land F (a) = r))$
23	21 22	bitri	$⊢ \exists b \exists a ((b \in x \land a \in x) \land (F (b) = s \land F (a) = r)) \leftrightarrow (\exists b (b \in x \land F (b) = s) \land \exists a (a \in x \land F (a) = r))$
24	19 23	sylibr	$⊢ (s \in F [x] \land r \in F [x]) \to \exists b \exists a ((b \in x \land a \in x) \land (F (b) = s \land F (a) = r))$
25	4	neeq1i	$⊢ H \neq \emptyset \leftrightarrow \{z \in A \| \forall g \in F [y] g R z\} \neq \emptyset$
26	25	ralbii	$⊢ \forall y \in x H \neq \emptyset \leftrightarrow \forall y \in x \{z \in A \| \forall g \in F [y] g R z\} \neq \emptyset$
27		imaeq2	$⊢ y = b \to F [y] = F [b]$
28	27	raleqdv	$⊢ y = b \to (\forall g \in F [y] g R z \leftrightarrow \forall g \in F [b] g R z)$
29	28	rabbidv	$⊢ y = b \to \{z \in A \| \forall g \in F [y] g R z\} = \{z \in A \| \forall g \in F [b] g R z\}$
30	29	neeq1d	$⊢ y = b \to (\{z \in A \| \forall g \in F [y] g R z\} \neq \emptyset \leftrightarrow \{z \in A \| \forall g \in F [b] g R z\} \neq \emptyset)$
31	30	rspccv	$⊢ \forall y \in x \{z \in A \| \forall g \in F [y] g R z\} \neq \emptyset \to (b \in x \to \{z \in A \| \forall g \in F [b] g R z\} \neq \emptyset)$
32		imaeq2	$⊢ y = a \to F [y] = F [a]$
33	32	raleqdv	$⊢ y = a \to (\forall g \in F [y] g R z \leftrightarrow \forall g \in F [a] g R z)$
34	33	rabbidv	$⊢ y = a \to \{z \in A \| \forall g \in F [y] g R z\} = \{z \in A \| \forall g \in F [a] g R z\}$
35	34	neeq1d	$⊢ y = a \to (\{z \in A \| \forall g \in F [y] g R z\} \neq \emptyset \leftrightarrow \{z \in A \| \forall g \in F [a] g R z\} \neq \emptyset)$
36	35	rspccv	$⊢ \forall y \in x \{z \in A \| \forall g \in F [y] g R z\} \neq \emptyset \to (a \in x \to \{z \in A \| \forall g \in F [a] g R z\} \neq \emptyset)$
37	31 36	anim12d	$⊢ \forall y \in x \{z \in A \| \forall g \in F [y] g R z\} \neq \emptyset \to ((b \in x \land a \in x) \to (\{z \in A \| \forall g \in F [b] g R z\} \neq \emptyset \land \{z \in A \| \forall g \in F [a] g R z\} \neq \emptyset))$
38	26 37	sylbi	$⊢ \forall y \in x H \neq \emptyset \to ((b \in x \land a \in x) \to (\{z \in A \| \forall g \in F [b] g R z\} \neq \emptyset \land \{z \in A \| \forall g \in F [a] g R z\} \neq \emptyset))$
39		onelon	$⊢ (x \in On \land b \in x) \to b \in On$
40		onelon	$⊢ (x \in On \land a \in x) \to a \in On$
41	39 40	anim12dan	$⊢ (x \in On \land (b \in x \land a \in x)) \to (b \in On \land a \in On)$
42	41	ex	$⊢ x \in On \to ((b \in x \land a \in x) \to (b \in On \land a \in On))$
43		eloni	$⊢ b \in On \to Ord b$
44		eloni	$⊢ a \in On \to Ord a$
45		ordtri3or	$⊢ (Ord b \land Ord a) \to (b \in a \lor b = a \lor a \in b)$
46	43 44 45	syl2an	$⊢ (b \in On \land a \in On) \to (b \in a \lor b = a \lor a \in b)$
47		eqid	$⊢ \{z \in A \| \forall g \in F [a] g R z\} = \{z \in A \| \forall g \in F [a] g R z\}$
48	1 2 47	zorn2lem2	$⊢ (a \in On \land (w We A \land \{z \in A \| \forall g \in F [a] g R z\} \neq \emptyset)) \to (b \in a \to F (b) R F (a))$
49	48	adantll	$⊢ ((b \in On \land a \in On) \land (w We A \land \{z \in A \| \forall g \in F [a] g R z\} \neq \emptyset)) \to (b \in a \to F (b) R F (a))$
50		breq12	$⊢ (F (b) = s \land F (a) = r) \to (F (b) R F (a) \leftrightarrow s R r)$
51	50	biimpcd	$⊢ F (b) R F (a) \to ((F (b) = s \land F (a) = r) \to s R r)$
52	49 51	syl6	$⊢ ((b \in On \land a \in On) \land (w We A \land \{z \in A \| \forall g \in F [a] g R z\} \neq \emptyset)) \to (b \in a \to ((F (b) = s \land F (a) = r) \to s R r))$
53	52	com23	$⊢ ((b \in On \land a \in On) \land (w We A \land \{z \in A \| \forall g \in F [a] g R z\} \neq \emptyset)) \to ((F (b) = s \land F (a) = r) \to (b \in a \to s R r))$
54	53	adantrrl	$⊢ ((b \in On \land a \in On) \land (w We A \land (\{z \in A \| \forall g \in F [b] g R z\} \neq \emptyset \land \{z \in A \| \forall g \in F [a] g R z\} \neq \emptyset))) \to ((F (b) = s \land F (a) = r) \to (b \in a \to s R r))$
55	54	imp	$⊢ (((b \in On \land a \in On) \land (w We A \land (\{z \in A \| \forall g \in F [b] g R z\} \neq \emptyset \land \{z \in A \| \forall g \in F [a] g R z\} \neq \emptyset))) \land (F (b) = s \land F (a) = r)) \to (b \in a \to s R r)$
56		fveq2	$⊢ b = a \to F (b) = F (a)$
57		eqeq12	$⊢ (F (b) = s \land F (a) = r) \to (F (b) = F (a) \leftrightarrow s = r)$
58	56 57	syl5ib	$⊢ (F (b) = s \land F (a) = r) \to (b = a \to s = r)$
59	58	adantl	$⊢ (((b \in On \land a \in On) \land (w We A \land (\{z \in A \| \forall g \in F [b] g R z\} \neq \emptyset \land \{z \in A \| \forall g \in F [a] g R z\} \neq \emptyset))) \land (F (b) = s \land F (a) = r)) \to (b = a \to s = r)$
60		eqid	$⊢ \{z \in A \| \forall g \in F [b] g R z\} = \{z \in A \| \forall g \in F [b] g R z\}$
61	1 2 60	zorn2lem2	$⊢ (b \in On \land (w We A \land \{z \in A \| \forall g \in F [b] g R z\} \neq \emptyset)) \to (a \in b \to F (a) R F (b))$
62	61	adantlr	$⊢ ((b \in On \land a \in On) \land (w We A \land \{z \in A \| \forall g \in F [b] g R z\} \neq \emptyset)) \to (a \in b \to F (a) R F (b))$
63		breq12	$⊢ (F (a) = r \land F (b) = s) \to (F (a) R F (b) \leftrightarrow r R s)$
64	63	ancoms	$⊢ (F (b) = s \land F (a) = r) \to (F (a) R F (b) \leftrightarrow r R s)$
65	64	biimpcd	$⊢ F (a) R F (b) \to ((F (b) = s \land F (a) = r) \to r R s)$
66	62 65	syl6	$⊢ ((b \in On \land a \in On) \land (w We A \land \{z \in A \| \forall g \in F [b] g R z\} \neq \emptyset)) \to (a \in b \to ((F (b) = s \land F (a) = r) \to r R s))$
67	66	com23	$⊢ ((b \in On \land a \in On) \land (w We A \land \{z \in A \| \forall g \in F [b] g R z\} \neq \emptyset)) \to ((F (b) = s \land F (a) = r) \to (a \in b \to r R s))$
68	67	adantrrr	$⊢ ((b \in On \land a \in On) \land (w We A \land (\{z \in A \| \forall g \in F [b] g R z\} \neq \emptyset \land \{z \in A \| \forall g \in F [a] g R z\} \neq \emptyset))) \to ((F (b) = s \land F (a) = r) \to (a \in b \to r R s))$
69	68	imp	$⊢ (((b \in On \land a \in On) \land (w We A \land (\{z \in A \| \forall g \in F [b] g R z\} \neq \emptyset \land \{z \in A \| \forall g \in F [a] g R z\} \neq \emptyset))) \land (F (b) = s \land F (a) = r)) \to (a \in b \to r R s)$
70	55 59 69	3orim123d	$⊢ (((b \in On \land a \in On) \land (w We A \land (\{z \in A \| \forall g \in F [b] g R z\} \neq \emptyset \land \{z \in A \| \forall g \in F [a] g R z\} \neq \emptyset))) \land (F (b) = s \land F (a) = r)) \to ((b \in a \lor b = a \lor a \in b) \to (s R r \lor s = r \lor r R s))$
71	46 70	syl5	$⊢ (((b \in On \land a \in On) \land (w We A \land (\{z \in A \| \forall g \in F [b] g R z\} \neq \emptyset \land \{z \in A \| \forall g \in F [a] g R z\} \neq \emptyset))) \land (F (b) = s \land F (a) = r)) \to ((b \in On \land a \in On) \to (s R r \lor s = r \lor r R s))$
72	71	exp31	$⊢ (b \in On \land a \in On) \to ((w We A \land (\{z \in A \| \forall g \in F [b] g R z\} \neq \emptyset \land \{z \in A \| \forall g \in F [a] g R z\} \neq \emptyset)) \to ((F (b) = s \land F (a) = r) \to ((b \in On \land a \in On) \to (s R r \lor s = r \lor r R s))))$
73	72	com4r	$⊢ (b \in On \land a \in On) \to ((b \in On \land a \in On) \to ((w We A \land (\{z \in A \| \forall g \in F [b] g R z\} \neq \emptyset \land \{z \in A \| \forall g \in F [a] g R z\} \neq \emptyset)) \to ((F (b) = s \land F (a) = r) \to (s R r \lor s = r \lor r R s))))$
74	42 42 73	syl6c	$⊢ x \in On \to ((b \in x \land a \in x) \to ((w We A \land (\{z \in A \| \forall g \in F [b] g R z\} \neq \emptyset \land \{z \in A \| \forall g \in F [a] g R z\} \neq \emptyset)) \to ((F (b) = s \land F (a) = r) \to (s R r \lor s = r \lor r R s))))$
75	74	exp4a	$⊢ x \in On \to ((b \in x \land a \in x) \to (w We A \to ((\{z \in A \| \forall g \in F [b] g R z\} \neq \emptyset \land \{z \in A \| \forall g \in F [a] g R z\} \neq \emptyset) \to ((F (b) = s \land F (a) = r) \to (s R r \lor s = r \lor r R s)))))$
76	75	com3r	$⊢ w We A \to (x \in On \to ((b \in x \land a \in x) \to ((\{z \in A \| \forall g \in F [b] g R z\} \neq \emptyset \land \{z \in A \| \forall g \in F [a] g R z\} \neq \emptyset) \to ((F (b) = s \land F (a) = r) \to (s R r \lor s = r \lor r R s)))))$
77	76	imp	$⊢ (w We A \land x \in On) \to ((b \in x \land a \in x) \to ((\{z \in A \| \forall g \in F [b] g R z\} \neq \emptyset \land \{z \in A \| \forall g \in F [a] g R z\} \neq \emptyset) \to ((F (b) = s \land F (a) = r) \to (s R r \lor s = r \lor r R s))))$
78	77	a2d	$⊢ (w We A \land x \in On) \to (((b \in x \land a \in x) \to (\{z \in A \| \forall g \in F [b] g R z\} \neq \emptyset \land \{z \in A \| \forall g \in F [a] g R z\} \neq \emptyset)) \to ((b \in x \land a \in x) \to ((F (b) = s \land F (a) = r) \to (s R r \lor s = r \lor r R s))))$
79	38 78	syl5	$⊢ (w We A \land x \in On) \to (\forall y \in x H \neq \emptyset \to ((b \in x \land a \in x) \to ((F (b) = s \land F (a) = r) \to (s R r \lor s = r \lor r R s))))$
80	79	imp4b	$⊢ ((w We A \land x \in On) \land \forall y \in x H \neq \emptyset) \to (((b \in x \land a \in x) \land (F (b) = s \land F (a) = r)) \to (s R r \lor s = r \lor r R s))$
81	80	exlimdvv	$⊢ ((w We A \land x \in On) \land \forall y \in x H \neq \emptyset) \to (\exists b \exists a ((b \in x \land a \in x) \land (F (b) = s \land F (a) = r)) \to (s R r \lor s = r \lor r R s))$
82	24 81	syl5	$⊢ ((w We A \land x \in On) \land \forall y \in x H \neq \emptyset) \to ((s \in F [x] \land r \in F [x]) \to (s R r \lor s = r \lor r R s))$
83	82	ralrimivv	$⊢ ((w We A \land x \in On) \land \forall y \in x H \neq \emptyset) \to \forall s \in F [x] \forall r \in F [x] (s R r \lor s = r \lor r R s)$
84	7 83	jca2	$⊢ R Po A \to (((w We A \land x \in On) \land \forall y \in x H \neq \emptyset) \to (R Po F [x] \land \forall s \in F [x] \forall r \in F [x] (s R r \lor s = r \lor r R s)))$
85		df-so	$⊢ R Or F [x] \leftrightarrow (R Po F [x] \land \forall s \in F [x] \forall r \in F [x] (s R r \lor s = r \lor r R s))$
86	84 85	syl6ibr	$⊢ R Po A \to (((w We A \land x \in On) \land \forall y \in x H \neq \emptyset) \to R Or F [x])$

Metamath Proof Explorer

Theorem zorn2lem6

Proof