wfrlem10

Description: Lemma for well-founded recursion. When z is an R minimal element of ( A \ dom F ) , then its predecessor class is equal to dom F . (Contributed by Scott Fenton, 21-Apr-2011)

	Ref	Expression
Hypotheses	wfrlem10.1	$⊢ R We A$
	wfrlem10.2	$⊢ F = wrecs (R, A, G)$
Assertion	wfrlem10	$⊢ (z \in (A ∖ dom F) \land Pred (R, (A ∖ dom F), z) = \emptyset) \to Pred (R, A, z) = dom F$

Proof

Step	Hyp	Ref	Expression
1		wfrlem10.1	$⊢ R We A$
2		wfrlem10.2	$⊢ F = wrecs (R, A, G)$
3	2	wfrlem8	$⊢ Pred (R, (A ∖ dom F), z) = \emptyset \leftrightarrow Pred (R, A, z) = Pred (R, dom F, z)$
4	3	biimpi	$⊢ Pred (R, (A ∖ dom F), z) = \emptyset \to Pred (R, A, z) = Pred (R, dom F, z)$
5		predss	$⊢ Pred (R, dom F, z) \subseteq dom F$
6	5	a1i	$⊢ z \in (A ∖ dom F) \to Pred (R, dom F, z) \subseteq dom F$
7		simpr	$⊢ (z \in (A ∖ dom F) \land w \in dom F) \to w \in dom F$
8		eldifn	$⊢ z \in (A ∖ dom F) \to \neg z \in dom F$
9		eleq1w	$⊢ w = z \to (w \in dom F \leftrightarrow z \in dom F)$
10	9	notbid	$⊢ w = z \to (\neg w \in dom F \leftrightarrow \neg z \in dom F)$
11	8 10	syl5ibrcom	$⊢ z \in (A ∖ dom F) \to (w = z \to \neg w \in dom F)$
12	11	con2d	$⊢ z \in (A ∖ dom F) \to (w \in dom F \to \neg w = z)$
13	12	imp	$⊢ (z \in (A ∖ dom F) \land w \in dom F) \to \neg w = z$
14		ssel	$⊢ Pred (R, A, w) \subseteq dom F \to (z \in Pred (R, A, w) \to z \in dom F)$
15	14	con3d	$⊢ Pred (R, A, w) \subseteq dom F \to (\neg z \in dom F \to \neg z \in Pred (R, A, w))$
16	8 15	syl5com	$⊢ z \in (A ∖ dom F) \to (Pred (R, A, w) \subseteq dom F \to \neg z \in Pred (R, A, w))$
17	2	wfrdmcl	$⊢ w \in dom F \to Pred (R, A, w) \subseteq dom F$
18	16 17	impel	$⊢ (z \in (A ∖ dom F) \land w \in dom F) \to \neg z \in Pred (R, A, w)$
19		eldifi	$⊢ z \in (A ∖ dom F) \to z \in A$
20		elpredg	$⊢ (w \in dom F \land z \in A) \to (z \in Pred (R, A, w) \leftrightarrow z R w)$
21	20	ancoms	$⊢ (z \in A \land w \in dom F) \to (z \in Pred (R, A, w) \leftrightarrow z R w)$
22	19 21	sylan	$⊢ (z \in (A ∖ dom F) \land w \in dom F) \to (z \in Pred (R, A, w) \leftrightarrow z R w)$
23	18 22	mtbid	$⊢ (z \in (A ∖ dom F) \land w \in dom F) \to \neg z R w$
24	2	wfrdmss	$⊢ dom F \subseteq A$
25	24	sseli	$⊢ w \in dom F \to w \in A$
26		weso	$⊢ R We A \to R Or A$
27	1 26	ax-mp	$⊢ R Or A$
28		solin	$⊢ (R Or A \land (w \in A \land z \in A)) \to (w R z \lor w = z \lor z R w)$
29	27 28	mpan	$⊢ (w \in A \land z \in A) \to (w R z \lor w = z \lor z R w)$
30	25 19 29	syl2anr	$⊢ (z \in (A ∖ dom F) \land w \in dom F) \to (w R z \lor w = z \lor z R w)$
31	13 23 30	ecase23d	$⊢ (z \in (A ∖ dom F) \land w \in dom F) \to w R z$
32		vex	$⊢ w \in V$
33	32	elpred	$⊢ z \in V \to (w \in Pred (R, dom F, z) \leftrightarrow (w \in dom F \land w R z))$
34	33	elv	$⊢ w \in Pred (R, dom F, z) \leftrightarrow (w \in dom F \land w R z)$
35	7 31 34	sylanbrc	$⊢ (z \in (A ∖ dom F) \land w \in dom F) \to w \in Pred (R, dom F, z)$
36	6 35	eqelssd	$⊢ z \in (A ∖ dom F) \to Pred (R, dom F, z) = dom F$
37	4 36	sylan9eqr	$⊢ (z \in (A ∖ dom F) \land Pred (R, (A ∖ dom F), z) = \emptyset) \to Pred (R, A, z) = dom F$

Metamath Proof Explorer

Theorem wfrlem10

Proof