bnj1500

Description: Well-founded recursion, part 2 of 3. The proof has been taken from Chapter 4 of Don Monk's notes on Set Theory. See http://euclid.colorado.edu/~monkd/setth.pdf . (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

	Ref	Expression
Hypotheses	bnj1500.1	$⊢ B = \{d \| (d \subseteq A \land \forall x \in d pred (x, A, R) \subseteq d)\}$
	bnj1500.2	$⊢ Y = ⟨x, {f ↾}_{pred (x, A, R)}⟩$
	bnj1500.3	$⊢ C = \{f \| \exists d \in B (f Fn d \land \forall x \in d f (x) = G (Y))\}$
	bnj1500.4	$⊢ F = ⋃ C$
Assertion	bnj1500	$⊢ R FrSe A \to \forall x \in A F (x) = G (⟨x, {F ↾}_{pred (x, A, R)}⟩)$

Proof

Step	Hyp	Ref	Expression
1		bnj1500.1	$⊢ B = \{d \| (d \subseteq A \land \forall x \in d pred (x, A, R) \subseteq d)\}$
2		bnj1500.2	$⊢ Y = ⟨x, {f ↾}_{pred (x, A, R)}⟩$
3		bnj1500.3	$⊢ C = \{f \| \exists d \in B (f Fn d \land \forall x \in d f (x) = G (Y))\}$
4		bnj1500.4	$⊢ F = ⋃ C$
5		biid	$⊢ (R FrSe A \land x \in A) \leftrightarrow (R FrSe A \land x \in A)$
6		biid	$⊢ ((R FrSe A \land x \in A) \land f \in C \land x \in dom f) \leftrightarrow ((R FrSe A \land x \in A) \land f \in C \land x \in dom f)$
7		biid	$⊢ (((R FrSe A \land x \in A) \land f \in C \land x \in dom f) \land d \in B \land dom f = d) \leftrightarrow (((R FrSe A \land x \in A) \land f \in C \land x \in dom f) \land d \in B \land dom f = d)$
8	1 2 3 4 5 6 7	bnj1501	$⊢ R FrSe A \to \forall x \in A F (x) = G (⟨x, {F ↾}_{pred (x, A, R)}⟩)$

Metamath Proof Explorer

Theorem bnj1500

Proof