bnj1522

Description: Well-founded recursion, part 3 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	bnj1522.1	$⊢ B = \{d \| (d \subseteq A \land \forall x \in d pred (x, A, R) \subseteq d)\}$
	bnj1522.2	$⊢ Y = ⟨x, {f ↾}_{pred (x, A, R)}⟩$
	bnj1522.3	$⊢ C = \{f \| \exists d \in B (f Fn d \land \forall x \in d f (x) = G (Y))\}$
	bnj1522.4	$⊢ F = ⋃ C$
Assertion	bnj1522	$⊢ (R FrSe A \land H Fn A \land \forall x \in A H (x) = G (⟨x, {H ↾}_{pred (x, A, R)}⟩)) \to F = H$

Proof

Step	Hyp	Ref	Expression
1		bnj1522.1	$⊢ B = \{d \| (d \subseteq A \land \forall x \in d pred (x, A, R) \subseteq d)\}$
2		bnj1522.2	$⊢ Y = ⟨x, {f ↾}_{pred (x, A, R)}⟩$
3		bnj1522.3	$⊢ C = \{f \| \exists d \in B (f Fn d \land \forall x \in d f (x) = G (Y))\}$
4		bnj1522.4	$⊢ F = ⋃ C$
5		biid	$⊢ (R FrSe A \land H Fn A \land \forall x \in A H (x) = G (⟨x, {H ↾}_{pred (x, A, R)}⟩)) \leftrightarrow (R FrSe A \land H Fn A \land \forall x \in A H (x) = G (⟨x, {H ↾}_{pred (x, A, R)}⟩))$
6		biid	$⊢ ((R FrSe A \land H Fn A \land \forall x \in A H (x) = G (⟨x, {H ↾}_{pred (x, A, R)}⟩)) \land F \neq H) \leftrightarrow ((R FrSe A \land H Fn A \land \forall x \in A H (x) = G (⟨x, {H ↾}_{pred (x, A, R)}⟩)) \land F \neq H)$
7		biid	$⊢ (((R FrSe A \land H Fn A \land \forall x \in A H (x) = G (⟨x, {H ↾}_{pred (x, A, R)}⟩)) \land F \neq H) \land x \in A \land F (x) \neq H (x)) \leftrightarrow (((R FrSe A \land H Fn A \land \forall x \in A H (x) = G (⟨x, {H ↾}_{pred (x, A, R)}⟩)) \land F \neq H) \land x \in A \land F (x) \neq H (x))$
8		eqid	$⊢ \{x \in A \| F (x) \neq H (x)\} = \{x \in A \| F (x) \neq H (x)\}$
9		biid	$⊢ ((((R FrSe A \land H Fn A \land \forall x \in A H (x) = G (⟨x, {H ↾}_{pred (x, A, R)}⟩)) \land F \neq H) \land x \in A \land F (x) \neq H (x)) \land y \in \{x \in A \| F (x) \neq H (x)\} \land \forall z \in \{x \in A \| F (x) \neq H (x)\} \neg z R y) \leftrightarrow ((((R FrSe A \land H Fn A \land \forall x \in A H (x) = G (⟨x, {H ↾}_{pred (x, A, R)}⟩)) \land F \neq H) \land x \in A \land F (x) \neq H (x)) \land y \in \{x \in A \| F (x) \neq H (x)\} \land \forall z \in \{x \in A \| F (x) \neq H (x)\} \neg z R y)$
10	1 2 3 4 5 6 7 8 9	bnj1523	$⊢ (R FrSe A \land H Fn A \land \forall x \in A H (x) = G (⟨x, {H ↾}_{pred (x, A, R)}⟩)) \to F = H$

Metamath Proof Explorer

Theorem bnj1522

Proof