tfrlem3a

Description: Lemma for transfinite recursion. Let A be the class of "acceptable" functions. The final thing we're interested in is the union of all these acceptable functions. This lemma just changes some bound variables in A for later use. (Contributed by NM, 9-Apr-1995)

	Ref	Expression
Hypotheses	tfrlem3.1	$⊢ A = \{f \| \exists x \in On (f Fn x \land \forall y \in x f (y) = F ({f ↾}_{y}))\}$
	tfrlem3.2	$⊢ G \in V$
Assertion	tfrlem3a	$⊢ G \in A \leftrightarrow \exists z \in On (G Fn z \land \forall w \in z G (w) = F ({G ↾}_{w}))$

Proof

Step	Hyp	Ref	Expression
1		tfrlem3.1	$⊢ A = \{f \| \exists x \in On (f Fn x \land \forall y \in x f (y) = F ({f ↾}_{y}))\}$
2		tfrlem3.2	$⊢ G \in V$
3		fneq12	$⊢ (f = G \land x = z) \to (f Fn x \leftrightarrow G Fn z)$
4		simpll	$⊢ ((f = G \land x = z) \land y = w) \to f = G$
5		simpr	$⊢ ((f = G \land x = z) \land y = w) \to y = w$
6	4 5	fveq12d	$⊢ ((f = G \land x = z) \land y = w) \to f (y) = G (w)$
7	4 5	reseq12d	$⊢ ((f = G \land x = z) \land y = w) \to {f ↾}_{y} = {G ↾}_{w}$
8	7	fveq2d	$⊢ ((f = G \land x = z) \land y = w) \to F ({f ↾}_{y}) = F ({G ↾}_{w})$
9	6 8	eqeq12d	$⊢ ((f = G \land x = z) \land y = w) \to (f (y) = F ({f ↾}_{y}) \leftrightarrow G (w) = F ({G ↾}_{w}))$
10		simplr	$⊢ ((f = G \land x = z) \land y = w) \to x = z$
11	9 10	cbvraldva2	$⊢ (f = G \land x = z) \to (\forall y \in x f (y) = F ({f ↾}_{y}) \leftrightarrow \forall w \in z G (w) = F ({G ↾}_{w}))$
12	3 11	anbi12d	$⊢ (f = G \land x = z) \to ((f Fn x \land \forall y \in x f (y) = F ({f ↾}_{y})) \leftrightarrow (G Fn z \land \forall w \in z G (w) = F ({G ↾}_{w})))$
13	12	cbvrexdva	$⊢ f = G \to (\exists x \in On (f Fn x \land \forall y \in x f (y) = F ({f ↾}_{y})) \leftrightarrow \exists z \in On (G Fn z \land \forall w \in z G (w) = F ({G ↾}_{w})))$
14	2 13 1	elab2	$⊢ G \in A \leftrightarrow \exists z \in On (G Fn z \land \forall w \in z G (w) = F ({G ↾}_{w}))$

Metamath Proof Explorer

Theorem tfrlem3a

Proof