zorn2lem3

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

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	zorn2lem2	$⊢ (x \in On \land (w We A \land D \neq \emptyset)) \to (y \in x \to F (y) R F (x))$
5	4	adantl	$⊢ (R Po A \land (x \in On \land (w We A \land D \neq \emptyset))) \to (y \in x \to F (y) R F (x))$
6	3	ssrab3	$⊢ D \subseteq A$
7	1 2 3	zorn2lem1	$⊢ (x \in On \land (w We A \land D \neq \emptyset)) \to F (x) \in D$
8	6 7	sselid	$⊢ (x \in On \land (w We A \land D \neq \emptyset)) \to F (x) \in A$
9		breq1	$⊢ F (x) = F (y) \to (F (x) R F (x) \leftrightarrow F (y) R F (x))$
10	9	biimprcd	$⊢ F (y) R F (x) \to (F (x) = F (y) \to F (x) R F (x))$
11		poirr	$⊢ (R Po A \land F (x) \in A) \to \neg F (x) R F (x)$
12	10 11	nsyli	$⊢ F (y) R F (x) \to ((R Po A \land F (x) \in A) \to \neg F (x) = F (y))$
13	12	com12	$⊢ (R Po A \land F (x) \in A) \to (F (y) R F (x) \to \neg F (x) = F (y))$
14	8 13	sylan2	$⊢ (R Po A \land (x \in On \land (w We A \land D \neq \emptyset))) \to (F (y) R F (x) \to \neg F (x) = F (y))$
15	5 14	syld	$⊢ (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))$

Metamath Proof Explorer