rdgsucmptnf

Description: The value of the recursive definition generator at a successor (special case where the characteristic function is an ordered-pair class abstraction and where the mapping class D is a proper class). This is a technical lemma that can be used together with rdgsucmptf to help eliminate redundant sethood antecedents. (Contributed by NM, 22-Oct-2003) (Revised by Mario Carneiro, 15-Oct-2016)

	Ref	Expression
Hypotheses	rdgsucmptf.1	$⊢ \underline{Ⅎ} x A$
	rdgsucmptf.2	$⊢ \underline{Ⅎ} x B$
	rdgsucmptf.3	$⊢ \underline{Ⅎ} x D$
	rdgsucmptf.4	$⊢ F = rec ((x \in V ⟼ C), A)$
	rdgsucmptf.5	$⊢ x = F (B) \to C = D$
Assertion	rdgsucmptnf	$⊢ \neg D \in V \to F (suc B) = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		rdgsucmptf.1	$⊢ \underline{Ⅎ} x A$
2		rdgsucmptf.2	$⊢ \underline{Ⅎ} x B$
3		rdgsucmptf.3	$⊢ \underline{Ⅎ} x D$
4		rdgsucmptf.4	$⊢ F = rec ((x \in V ⟼ C), A)$
5		rdgsucmptf.5	$⊢ x = F (B) \to C = D$
6	4	fveq1i	$⊢ F (suc B) = rec ((x \in V ⟼ C), A) (suc B)$
7		rdgdmlim	$⊢ Lim dom rec ((x \in V ⟼ C), A)$
8		limsuc	$⊢ Lim dom rec ((x \in V ⟼ C), A) \to (B \in dom rec ((x \in V ⟼ C), A) \leftrightarrow suc B \in dom rec ((x \in V ⟼ C), A))$
9	7 8	ax-mp	$⊢ B \in dom rec ((x \in V ⟼ C), A) \leftrightarrow suc B \in dom rec ((x \in V ⟼ C), A)$
10		rdgsucg	$⊢ B \in dom rec ((x \in V ⟼ C), A) \to rec ((x \in V ⟼ C), A) (suc B) = (x \in V ⟼ C) (rec ((x \in V ⟼ C), A) (B))$
11	4	fveq1i	$⊢ F (B) = rec ((x \in V ⟼ C), A) (B)$
12	11	fveq2i	$⊢ (x \in V ⟼ C) (F (B)) = (x \in V ⟼ C) (rec ((x \in V ⟼ C), A) (B))$
13	10 12	eqtr4di	$⊢ B \in dom rec ((x \in V ⟼ C), A) \to rec ((x \in V ⟼ C), A) (suc B) = (x \in V ⟼ C) (F (B))$
14		nfmpt1	$⊢ \underline{Ⅎ} x (x \in V ⟼ C)$
15	14 1	nfrdg	$⊢ \underline{Ⅎ} x rec ((x \in V ⟼ C), A)$
16	4 15	nfcxfr	$⊢ \underline{Ⅎ} x F$
17	16 2	nffv	$⊢ \underline{Ⅎ} x F (B)$
18		eqid	$⊢ (x \in V ⟼ C) = (x \in V ⟼ C)$
19	17 3 5 18	fvmptnf	$⊢ \neg D \in V \to (x \in V ⟼ C) (F (B)) = \emptyset$
20	13 19	sylan9eqr	$⊢ (\neg D \in V \land B \in dom rec ((x \in V ⟼ C), A)) \to rec ((x \in V ⟼ C), A) (suc B) = \emptyset$
21	20	ex	$⊢ \neg D \in V \to (B \in dom rec ((x \in V ⟼ C), A) \to rec ((x \in V ⟼ C), A) (suc B) = \emptyset)$
22	9 21	biimtrrid	$⊢ \neg D \in V \to (suc B \in dom rec ((x \in V ⟼ C), A) \to rec ((x \in V ⟼ C), A) (suc B) = \emptyset)$
23		ndmfv	$⊢ \neg suc B \in dom rec ((x \in V ⟼ C), A) \to rec ((x \in V ⟼ C), A) (suc B) = \emptyset$
24	22 23	pm2.61d1	$⊢ \neg D \in V \to rec ((x \in V ⟼ C), A) (suc B) = \emptyset$
25	6 24	eqtrid	$⊢ \neg D \in V \to F (suc B) = \emptyset$

Metamath Proof Explorer

Theorem rdgsucmptnf

Proof