Metamath Proof Explorer

Theorem bnj1204

Description: Well-founded induction. 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
Hypothesis bnj1204.1 
|- ( ps <-> A. y e. A ( y R x -> [. y / x ]. ph ) )
Assertion bnj1204 
|- ( ( R _FrSe A /\ A. x e. A ( ps -> ph ) ) -> A. x e. A ph )

Proof

Step Hyp Ref Expression
1 bnj1204.1 
 |-  ( ps <-> A. y e. A ( y R x -> [. y / x ]. ph ) )
2 simp1 
 |-  ( ( R _FrSe A /\ A. x e. A ( ps -> ph ) /\ E. x e. A -. ph ) -> R _FrSe A )
3 ssrab2 
 |-  { x e. A | -. ph } C_ A
4 3 a1i 
 |-  ( ( R _FrSe A /\ A. x e. A ( ps -> ph ) /\ E. x e. A -. ph ) -> { x e. A | -. ph } C_ A )
5 simp3 
 |-  ( ( R _FrSe A /\ A. x e. A ( ps -> ph ) /\ E. x e. A -. ph ) -> E. x e. A -. ph )
6 rabn0 
 |-  ( { x e. A | -. ph } =/= (/) <-> E. x e. A -. ph )
7 5 6 sylibr 
 |-  ( ( R _FrSe A /\ A. x e. A ( ps -> ph ) /\ E. x e. A -. ph ) -> { x e. A | -. ph } =/= (/) )
8 nfrab1 
 |-  F/_ x { x e. A | -. ph }
9 8 nfcrii 
 |-  ( z e. { x e. A | -. ph } -> A. x z e. { x e. A | -. ph } )
10 9 bnj1228 
 |-  ( ( R _FrSe A /\ { x e. A | -. ph } C_ A /\ { x e. A | -. ph } =/= (/) ) -> E. x e. { x e. A | -. ph } A. y e. { x e. A | -. ph } -. y R x )
11 2 4 7 10 syl3anc 
 |-  ( ( R _FrSe A /\ A. x e. A ( ps -> ph ) /\ E. x e. A -. ph ) -> E. x e. { x e. A | -. ph } A. y e. { x e. A | -. ph } -. y R x )
12 biid 
 |-  ( ( ( R _FrSe A /\ A. x e. A ( ps -> ph ) /\ E. x e. A -. ph ) /\ x e. { x e. A | -. ph } /\ A. y e. { x e. A | -. ph } -. y R x ) <-> ( ( R _FrSe A /\ A. x e. A ( ps -> ph ) /\ E. x e. A -. ph ) /\ x e. { x e. A | -. ph } /\ A. y e. { x e. A | -. ph } -. y R x ) )
13 nfv 
 |-  F/ x R _FrSe A
14 nfra1 
 |-  F/ x A. x e. A ( ps -> ph )
15 nfre1 
 |-  F/ x E. x e. A -. ph
16 13 14 15 nf3an 
 |-  F/ x ( R _FrSe A /\ A. x e. A ( ps -> ph ) /\ E. x e. A -. ph )
17 16 nf5ri 
 |-  ( ( R _FrSe A /\ A. x e. A ( ps -> ph ) /\ E. x e. A -. ph ) -> A. x ( R _FrSe A /\ A. x e. A ( ps -> ph ) /\ E. x e. A -. ph ) )
18 11 12 17 bnj1521 
 |-  ( ( R _FrSe A /\ A. x e. A ( ps -> ph ) /\ E. x e. A -. ph ) -> E. x ( ( R _FrSe A /\ A. x e. A ( ps -> ph ) /\ E. x e. A -. ph ) /\ x e. { x e. A | -. ph } /\ A. y e. { x e. A | -. ph } -. y R x ) )
19 eqid 
 |-  { x e. A | -. ph } = { x e. A | -. ph }
20 19 12 bnj1212 
 |-  ( ( ( R _FrSe A /\ A. x e. A ( ps -> ph ) /\ E. x e. A -. ph ) /\ x e. { x e. A | -. ph } /\ A. y e. { x e. A | -. ph } -. y R x ) -> x e. A )
21 nfra1 
 |-  F/ y A. y e. { x e. A | -. ph } -. y R x
22 simp3 
 |-  ( ( y e. A /\ y R x /\ A. y e. { x e. A | -. ph } -. y R x ) -> A. y e. { x e. A | -. ph } -. y R x )
23 22 bnj1211 
 |-  ( ( y e. A /\ y R x /\ A. y e. { x e. A | -. ph } -. y R x ) -> A. y ( y e. { x e. A | -. ph } -> -. y R x ) )
24 con2b 
 |-  ( ( y e. { x e. A | -. ph } -> -. y R x ) <-> ( y R x -> -. y e. { x e. A | -. ph } ) )
25 24 albii 
 |-  ( A. y ( y e. { x e. A | -. ph } -> -. y R x ) <-> A. y ( y R x -> -. y e. { x e. A | -. ph } ) )
26 23 25 sylib 
 |-  ( ( y e. A /\ y R x /\ A. y e. { x e. A | -. ph } -. y R x ) -> A. y ( y R x -> -. y e. { x e. A | -. ph } ) )
27 simp2 
 |-  ( ( y e. A /\ y R x /\ A. y e. { x e. A | -. ph } -. y R x ) -> y R x )
28 sp 
 |-  ( A. y ( y R x -> -. y e. { x e. A | -. ph } ) -> ( y R x -> -. y e. { x e. A | -. ph } ) )
29 26 27 28 sylc 
 |-  ( ( y e. A /\ y R x /\ A. y e. { x e. A | -. ph } -. y R x ) -> -. y e. { x e. A | -. ph } )
30 simp1 
 |-  ( ( y e. A /\ y R x /\ A. y e. { x e. A | -. ph } -. y R x ) -> y e. A )
31 nfcv 
 |-  F/_ x A
32 31 elrabsf 
 |-  ( y e. { x e. A | -. ph } <-> ( y e. A /\ [. y / x ]. -. ph ) )
33 vex 
 |-  y e. _V
34 sbcng 
 |-  ( y e. _V -> ( [. y / x ]. -. ph <-> -. [. y / x ]. ph ) )
35 33 34 ax-mp 
 |-  ( [. y / x ]. -. ph <-> -. [. y / x ]. ph )
36 35 anbi2i 
 |-  ( ( y e. A /\ [. y / x ]. -. ph ) <-> ( y e. A /\ -. [. y / x ]. ph ) )
37 32 36 bitri 
 |-  ( y e. { x e. A | -. ph } <-> ( y e. A /\ -. [. y / x ]. ph ) )
38 37 notbii 
 |-  ( -. y e. { x e. A | -. ph } <-> -. ( y e. A /\ -. [. y / x ]. ph ) )
39 imnan 
 |-  ( ( y e. A -> -. -. [. y / x ]. ph ) <-> -. ( y e. A /\ -. [. y / x ]. ph ) )
40 38 39 sylbb2 
 |-  ( -. y e. { x e. A | -. ph } -> ( y e. A -> -. -. [. y / x ]. ph ) )
41 40 imp 
 |-  ( ( -. y e. { x e. A | -. ph } /\ y e. A ) -> -. -. [. y / x ]. ph )
42 41 notnotrd 
 |-  ( ( -. y e. { x e. A | -. ph } /\ y e. A ) -> [. y / x ]. ph )
43 29 30 42 syl2anc 
 |-  ( ( y e. A /\ y R x /\ A. y e. { x e. A | -. ph } -. y R x ) -> [. y / x ]. ph )
44 43 3expa 
 |-  ( ( ( y e. A /\ y R x ) /\ A. y e. { x e. A | -. ph } -. y R x ) -> [. y / x ]. ph )
45 44 expcom 
 |-  ( A. y e. { x e. A | -. ph } -. y R x -> ( ( y e. A /\ y R x ) -> [. y / x ]. ph ) )
46 45 expd 
 |-  ( A. y e. { x e. A | -. ph } -. y R x -> ( y e. A -> ( y R x -> [. y / x ]. ph ) ) )
47 21 46 ralrimi 
 |-  ( A. y e. { x e. A | -. ph } -. y R x -> A. y e. A ( y R x -> [. y / x ]. ph ) )
48 47 1 sylibr 
 |-  ( A. y e. { x e. A | -. ph } -. y R x -> ps )
49 48 3ad2ant3 
 |-  ( ( ( R _FrSe A /\ A. x e. A ( ps -> ph ) /\ E. x e. A -. ph ) /\ x e. { x e. A | -. ph } /\ A. y e. { x e. A | -. ph } -. y R x ) -> ps )
50 simp12 
 |-  ( ( ( R _FrSe A /\ A. x e. A ( ps -> ph ) /\ E. x e. A -. ph ) /\ x e. { x e. A | -. ph } /\ A. y e. { x e. A | -. ph } -. y R x ) -> A. x e. A ( ps -> ph ) )
51 simp3 
 |-  ( ( x e. A /\ ps /\ A. x e. A ( ps -> ph ) ) -> A. x e. A ( ps -> ph ) )
52 51 bnj1211 
 |-  ( ( x e. A /\ ps /\ A. x e. A ( ps -> ph ) ) -> A. x ( x e. A -> ( ps -> ph ) ) )
53 simp1 
 |-  ( ( x e. A /\ ps /\ A. x e. A ( ps -> ph ) ) -> x e. A )
54 simp2 
 |-  ( ( x e. A /\ ps /\ A. x e. A ( ps -> ph ) ) -> ps )
55 sp 
 |-  ( A. x ( x e. A -> ( ps -> ph ) ) -> ( x e. A -> ( ps -> ph ) ) )
56 52 53 54 55 syl3c 
 |-  ( ( x e. A /\ ps /\ A. x e. A ( ps -> ph ) ) -> ph )
57 20 49 50 56 syl3anc 
 |-  ( ( ( R _FrSe A /\ A. x e. A ( ps -> ph ) /\ E. x e. A -. ph ) /\ x e. { x e. A | -. ph } /\ A. y e. { x e. A | -. ph } -. y R x ) -> ph )
58 rabid 
 |-  ( x e. { x e. A | -. ph } <-> ( x e. A /\ -. ph ) )
59 58 simprbi 
 |-  ( x e. { x e. A | -. ph } -> -. ph )
60 59 3ad2ant2 
 |-  ( ( ( R _FrSe A /\ A. x e. A ( ps -> ph ) /\ E. x e. A -. ph ) /\ x e. { x e. A | -. ph } /\ A. y e. { x e. A | -. ph } -. y R x ) -> -. ph )
61 18 57 60 bnj1304 
 |-  -. ( R _FrSe A /\ A. x e. A ( ps -> ph ) /\ E. x e. A -. ph )
62 61 bnj1224 
 |-  ( ( R _FrSe A /\ A. x e. A ( ps -> ph ) ) -> -. E. x e. A -. ph )
63 dfral2 
 |-  ( A. x e. A ph <-> -. E. x e. A -. ph )
64 62 63 sylibr 
 |-  ( ( R _FrSe A /\ A. x e. A ( ps -> ph ) ) -> A. x e. A ph )