frsucmptn

Description: The value of the finite recursive definition generator at a successor (special case where the characteristic function is a mapping abstraction and where the mapping class D is a proper class). This is a technical lemma that can be used together with frsucmpt to help eliminate redundant sethood antecedents. (Contributed by Scott Fenton, 19-Feb-2011) (Revised by Mario Carneiro, 11-Sep-2015)

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

Proof

Step	Hyp	Ref	Expression
1		frsucmpt.1	$⊢ \underline{Ⅎ} x A$
2		frsucmpt.2	$⊢ \underline{Ⅎ} x B$
3		frsucmpt.3	$⊢ \underline{Ⅎ} x D$
4		frsucmpt.4	$⊢ F = {rec ((x \in V ⟼ C), A) ↾}_{ω}$
5		frsucmpt.5	$⊢ x = F (B) \to C = D$
6	4	fveq1i	$⊢ F (suc B) = ({rec ((x \in V ⟼ C), A) ↾}_{ω}) (suc B)$
7		frfnom	$⊢ ({rec ((x \in V ⟼ C), A) ↾}_{ω}) Fn ω$
8		fndm	$⊢ ({rec ((x \in V ⟼ C), A) ↾}_{ω}) Fn ω \to dom ({rec ((x \in V ⟼ C), A) ↾}_{ω}) = ω$
9	7 8	ax-mp	$⊢ dom ({rec ((x \in V ⟼ C), A) ↾}_{ω}) = ω$
10	9	eleq2i	$⊢ suc B \in dom ({rec ((x \in V ⟼ C), A) ↾}_{ω}) \leftrightarrow suc B \in ω$
11		peano2b	$⊢ B \in ω \leftrightarrow suc B \in ω$
12		frsuc	$⊢ B \in ω \to ({rec ((x \in V ⟼ C), A) ↾}_{ω}) (suc B) = (x \in V ⟼ C) (({rec ((x \in V ⟼ C), A) ↾}_{ω}) (B))$
13	4	fveq1i	$⊢ F (B) = ({rec ((x \in V ⟼ C), A) ↾}_{ω}) (B)$
14	13	fveq2i	$⊢ (x \in V ⟼ C) (F (B)) = (x \in V ⟼ C) (({rec ((x \in V ⟼ C), A) ↾}_{ω}) (B))$
15	12 14	eqtr4di	$⊢ B \in ω \to ({rec ((x \in V ⟼ C), A) ↾}_{ω}) (suc B) = (x \in V ⟼ C) (F (B))$
16		nfmpt1	$⊢ \underline{Ⅎ} x (x \in V ⟼ C)$
17	16 1	nfrdg	$⊢ \underline{Ⅎ} x rec ((x \in V ⟼ C), A)$
18		nfcv	$⊢ \underline{Ⅎ} x ω$
19	17 18	nfres	$⊢ \underline{Ⅎ} x ({rec ((x \in V ⟼ C), A) ↾}_{ω})$
20	4 19	nfcxfr	$⊢ \underline{Ⅎ} x F$
21	20 2	nffv	$⊢ \underline{Ⅎ} x F (B)$
22		eqid	$⊢ (x \in V ⟼ C) = (x \in V ⟼ C)$
23	21 3 5 22	fvmptnf	$⊢ \neg D \in V \to (x \in V ⟼ C) (F (B)) = \emptyset$
24	15 23	sylan9eqr	$⊢ (\neg D \in V \land B \in ω) \to ({rec ((x \in V ⟼ C), A) ↾}_{ω}) (suc B) = \emptyset$
25	24	ex	$⊢ \neg D \in V \to (B \in ω \to ({rec ((x \in V ⟼ C), A) ↾}_{ω}) (suc B) = \emptyset)$
26	11 25	syl5bir	$⊢ \neg D \in V \to (suc B \in ω \to ({rec ((x \in V ⟼ C), A) ↾}_{ω}) (suc B) = \emptyset)$
27	10 26	syl5bi	$⊢ \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)$
28		ndmfv	$⊢ \neg suc B \in dom ({rec ((x \in V ⟼ C), A) ↾}_{ω}) \to ({rec ((x \in V ⟼ C), A) ↾}_{ω}) (suc B) = \emptyset$
29	27 28	pm2.61d1	$⊢ \neg D \in V \to ({rec ((x \in V ⟼ C), A) ↾}_{ω}) (suc B) = \emptyset$
30	6 29	eqtrid	$⊢ \neg D \in V \to F (suc B) = \emptyset$

Metamath Proof Explorer

Theorem frsucmptn

Proof