wfrlem8OLD

Description: Lemma for well-ordered recursion. Compute the prececessor class for an R minimal element of ( A \ dom F ) . Obsolete as of 18-Nov-2024. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Scott Fenton, 21-Apr-2011)

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

Proof

Step	Hyp	Ref	Expression
1		wfrlem6OLD.1	$⊢ F = wrecs (R, A, G)$
2	1	wfrdmssOLD	$⊢ 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)$

Metamath Proof Explorer

Theorem wfrlem8OLD

Proof