Metamath Proof Explorer


Theorem 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 A x d pred x A R d
bnj1522.2 Y = x f pred x A R
bnj1522.3 C = f | d B f Fn d x d f x = G Y
bnj1522.4 F = C
Assertion bnj1522 R FrSe A H Fn A x A H x = G x H pred x A R F = H

Proof

Step Hyp Ref Expression
1 bnj1522.1 B = d | d A x d pred x A R d
2 bnj1522.2 Y = x f pred x A R
3 bnj1522.3 C = f | d B f Fn d x d f x = G Y
4 bnj1522.4 F = C
5 biid R FrSe A H Fn A x A H x = G x H pred x A R R FrSe A H Fn A x A H x = G x H pred x A R
6 biid R FrSe A H Fn A x A H x = G x H pred x A R F H R FrSe A H Fn A x A H x = G x H pred x A R F H
7 biid R FrSe A H Fn A x A H x = G x H pred x A R F H x A F x H x R FrSe A H Fn A x A H x = G x H pred x A R F H x A F x H x
8 eqid x A | F x H x = x A | F x H x
9 biid R FrSe A H Fn A x A H x = G x H pred x A R F H x A F x H x y x A | F x H x z x A | F x H x ¬ z R y R FrSe A H Fn A x A H x = G x H pred x A R F H x A F x H x y x A | F x H x z x A | F x H x ¬ z R y
10 1 2 3 4 5 6 7 8 9 bnj1523 R FrSe A H Fn A x A H x = G x H pred x A R F = H