zorn2lem2

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	zorn2lem2	$⊢ (x \in On \land (w We A \land D \neq \emptyset)) \to (y \in x \to F (y) R F (x))$

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 2 3	zorn2lem1	$⊢ (x \in On \land (w We A \land D \neq \emptyset)) \to F (x) \in D$
5		breq2	$⊢ z = F (x) \to (g R z \leftrightarrow g R F (x))$
6	5	ralbidv	$⊢ z = F (x) \to (\forall g \in F [x] g R z \leftrightarrow \forall g \in F [x] g R F (x))$
7	6 3	elrab2	$⊢ F (x) \in D \leftrightarrow (F (x) \in A \land \forall g \in F [x] g R F (x))$
8	7	simprbi	$⊢ F (x) \in D \to \forall g \in F [x] g R F (x)$
9	4 8	syl	$⊢ (x \in On \land (w We A \land D \neq \emptyset)) \to \forall g \in F [x] g R F (x)$
10	1	tfr1	$⊢ F Fn On$
11		onss	$⊢ x \in On \to x \subseteq On$
12		fnfvima	$⊢ (F Fn On \land x \subseteq On \land y \in x) \to F (y) \in F [x]$
13	12	3expia	$⊢ (F Fn On \land x \subseteq On) \to (y \in x \to F (y) \in F [x])$
14	10 11 13	sylancr	$⊢ x \in On \to (y \in x \to F (y) \in F [x])$
15	14	adantr	$⊢ (x \in On \land (w We A \land D \neq \emptyset)) \to (y \in x \to F (y) \in F [x])$
16		breq1	$⊢ g = F (y) \to (g R F (x) \leftrightarrow F (y) R F (x))$
17	16	rspccv	$⊢ \forall g \in F [x] g R F (x) \to (F (y) \in F [x] \to F (y) R F (x))$
18	9 15 17	sylsyld	$⊢ (x \in On \land (w We A \land D \neq \emptyset)) \to (y \in x \to F (y) R F (x))$

Metamath Proof Explorer