Metamath Proof Explorer

Theorem wfrlem8

Description: Lemma for well-founded recursion. Compute the prececessor class for an R minimal element of ( A \ dom F ) . (Contributed by Scott Fenton, 21-Apr-2011)

		Ref	Expression
	Hypothesis	wfrlem6.1	$⊢ F = wrecs (R, A, G)$
	Assertion	wfrlem8	$⊢ Pred (R, (A ∖ dom F), X) = \emptyset \leftrightarrow Pred (R, A, X) = Pred (R, dom F, X)$

Proof

Step	Hyp	Ref	Expression
1		wfrlem6.1	$⊢ F = wrecs (R, A, G)$
2	1	wfrdmss	$⊢ dom F \subseteq A$
3		predpredss	$⊢ dom F \subseteq A \to Pred (R, dom F, X) \subseteq Pred (R, A, X)$
4	2 3	ax-mp	$⊢ Pred (R, dom F, X) \subseteq Pred (R, A, X)$
5	4	biantru	$⊢ Pred (R, A, X) \subseteq Pred (R, dom F, X) \leftrightarrow (Pred (R, A, X) \subseteq Pred (R, dom F, X) \land Pred (R, dom F, X) \subseteq Pred (R, A, X))$
6		preddif	$⊢ Pred (R, (A ∖ dom F), X) = Pred (R, A, X) ∖ Pred (R, dom F, X)$
7	6	eqeq1i	$⊢ Pred (R, (A ∖ dom F), X) = \emptyset \leftrightarrow Pred (R, A, X) ∖ Pred (R, dom F, X) = \emptyset$
8		ssdif0	$⊢ Pred (R, A, X) \subseteq Pred (R, dom F, X) \leftrightarrow Pred (R, A, X) ∖ Pred (R, dom F, X) = \emptyset$
9	7 8	bitr4i	$⊢ Pred (R, (A ∖ dom F), X) = \emptyset \leftrightarrow Pred (R, A, X) \subseteq Pred (R, dom F, X)$
10		eqss	$⊢ Pred (R, A, X) = Pred (R, dom F, X) \leftrightarrow (Pred (R, A, X) \subseteq Pred (R, dom F, X) \land Pred (R, dom F, X) \subseteq Pred (R, A, X))$
11	5 9 10	3bitr4i	$⊢ Pred (R, (A ∖ dom F), X) = \emptyset \leftrightarrow Pred (R, A, X) = Pred (R, dom F, X)$