tfrlem12

Description: Lemma for transfinite recursion. Show C is an acceptable function. (Contributed by NM, 15-Aug-1994) (Revised by Mario Carneiro, 9-May-2015)

	Ref	Expression
Hypotheses	tfrlem.1	$⊢ A = \{f \| \exists x \in On (f Fn x \land \forall y \in x f (y) = F ({f ↾}_{y}))\}$
	tfrlem.3	$⊢ C = recs (F) \cup \{⟨dom recs (F), F (recs (F))⟩\}$
Assertion	tfrlem12	$⊢ recs (F) \in V \to C \in A$

Proof

Step	Hyp	Ref	Expression
1		tfrlem.1	$⊢ A = \{f \| \exists x \in On (f Fn x \land \forall y \in x f (y) = F ({f ↾}_{y}))\}$
2		tfrlem.3	$⊢ C = recs (F) \cup \{⟨dom recs (F), F (recs (F))⟩\}$
3	1	tfrlem8	$⊢ Ord dom recs (F)$
4	3	a1i	$⊢ recs (F) \in V \to Ord dom recs (F)$
5		dmexg	$⊢ recs (F) \in V \to dom recs (F) \in V$
6		elon2	$⊢ dom recs (F) \in On \leftrightarrow (Ord dom recs (F) \land dom recs (F) \in V)$
7	4 5 6	sylanbrc	$⊢ recs (F) \in V \to dom recs (F) \in On$
8		onsuc	$⊢ dom recs (F) \in On \to suc dom recs (F) \in On$
9	1 2	tfrlem10	$⊢ dom recs (F) \in On \to C Fn suc dom recs (F)$
10	1 2	tfrlem11	$⊢ dom recs (F) \in On \to (z \in suc dom recs (F) \to C (z) = F ({C ↾}_{z}))$
11	10	ralrimiv	$⊢ dom recs (F) \in On \to \forall z \in suc dom recs (F) C (z) = F ({C ↾}_{z})$
12		fveq2	$⊢ z = y \to C (z) = C (y)$
13		reseq2	$⊢ z = y \to {C ↾}_{z} = {C ↾}_{y}$
14	13	fveq2d	$⊢ z = y \to F ({C ↾}_{z}) = F ({C ↾}_{y})$
15	12 14	eqeq12d	$⊢ z = y \to (C (z) = F ({C ↾}_{z}) \leftrightarrow C (y) = F ({C ↾}_{y}))$
16	15	cbvralvw	$⊢ \forall z \in suc dom recs (F) C (z) = F ({C ↾}_{z}) \leftrightarrow \forall y \in suc dom recs (F) C (y) = F ({C ↾}_{y})$
17	11 16	sylib	$⊢ dom recs (F) \in On \to \forall y \in suc dom recs (F) C (y) = F ({C ↾}_{y})$
18		fneq2	$⊢ x = suc dom recs (F) \to (C Fn x \leftrightarrow C Fn suc dom recs (F))$
19		raleq	$⊢ x = suc dom recs (F) \to (\forall y \in x C (y) = F ({C ↾}_{y}) \leftrightarrow \forall y \in suc dom recs (F) C (y) = F ({C ↾}_{y}))$
20	18 19	anbi12d	$⊢ x = suc dom recs (F) \to ((C Fn x \land \forall y \in x C (y) = F ({C ↾}_{y})) \leftrightarrow (C Fn suc dom recs (F) \land \forall y \in suc dom recs (F) C (y) = F ({C ↾}_{y})))$
21	20	rspcev	$⊢ (suc dom recs (F) \in On \land (C Fn suc dom recs (F) \land \forall y \in suc dom recs (F) C (y) = F ({C ↾}_{y}))) \to \exists x \in On (C Fn x \land \forall y \in x C (y) = F ({C ↾}_{y}))$
22	8 9 17 21	syl12anc	$⊢ dom recs (F) \in On \to \exists x \in On (C Fn x \land \forall y \in x C (y) = F ({C ↾}_{y}))$
23	7 22	syl	$⊢ recs (F) \in V \to \exists x \in On (C Fn x \land \forall y \in x C (y) = F ({C ↾}_{y}))$
24		snex	$⊢ \{⟨dom recs (F), F (recs (F))⟩\} \in V$
25		unexg	$⊢ (recs (F) \in V \land \{⟨dom recs (F), F (recs (F))⟩\} \in V) \to recs (F) \cup \{⟨dom recs (F), F (recs (F))⟩\} \in V$
26	24 25	mpan2	$⊢ recs (F) \in V \to recs (F) \cup \{⟨dom recs (F), F (recs (F))⟩\} \in V$
27	2 26	eqeltrid	$⊢ recs (F) \in V \to C \in V$
28		fneq1	$⊢ f = C \to (f Fn x \leftrightarrow C Fn x)$
29		fveq1	$⊢ f = C \to f (y) = C (y)$
30		reseq1	$⊢ f = C \to {f ↾}_{y} = {C ↾}_{y}$
31	30	fveq2d	$⊢ f = C \to F ({f ↾}_{y}) = F ({C ↾}_{y})$
32	29 31	eqeq12d	$⊢ f = C \to (f (y) = F ({f ↾}_{y}) \leftrightarrow C (y) = F ({C ↾}_{y}))$
33	32	ralbidv	$⊢ f = C \to (\forall y \in x f (y) = F ({f ↾}_{y}) \leftrightarrow \forall y \in x C (y) = F ({C ↾}_{y}))$
34	28 33	anbi12d	$⊢ f = C \to ((f Fn x \land \forall y \in x f (y) = F ({f ↾}_{y})) \leftrightarrow (C Fn x \land \forall y \in x C (y) = F ({C ↾}_{y})))$
35	34	rexbidv	$⊢ f = C \to (\exists x \in On (f Fn x \land \forall y \in x f (y) = F ({f ↾}_{y})) \leftrightarrow \exists x \in On (C Fn x \land \forall y \in x C (y) = F ({C ↾}_{y})))$
36	35 1	elab2g	$⊢ C \in V \to (C \in A \leftrightarrow \exists x \in On (C Fn x \land \forall y \in x C (y) = F ({C ↾}_{y})))$
37	27 36	syl	$⊢ recs (F) \in V \to (C \in A \leftrightarrow \exists x \in On (C Fn x \land \forall y \in x C (y) = F ({C ↾}_{y})))$
38	23 37	mpbird	$⊢ recs (F) \in V \to C \in A$

Metamath Proof Explorer

Theorem tfrlem12

Proof