Metamath Proof Explorer

Theorem bnj110

Description: Well-founded induction restricted to a set ( A e. _V ). 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 bnj110.1 
|- A e. _V
bnj110.2 
|- ( ps <-> A. y e. A ( y R x -> [. y / x ]. ph ) )
Assertion bnj110 
|- ( ( R Fr A /\ A. x e. A ( ps -> ph ) ) -> A. x e. A ph )

Proof

Step Hyp Ref Expression
1 bnj110.1 
 |-  A e. _V
2 bnj110.2 
 |-  ( ps <-> A. y e. A ( y R x -> [. y / x ]. ph ) )
3 ralnex 
 |-  ( A. z e. { x e. A | -. ph } -. [. z / x ]. ph <-> -. E. z e. { x e. A | -. ph } [. z / x ]. ph )
4 sbcng 
 |-  ( z e. _V -> ( [. z / x ]. -. ph <-> -. [. z / x ]. ph ) )
5 4 elv 
 |-  ( [. z / x ]. -. ph <-> -. [. z / x ]. ph )
6 5 bicomi 
 |-  ( -. [. z / x ]. ph <-> [. z / x ]. -. ph )
7 6 ralbii 
 |-  ( A. z e. { x e. A | -. ph } -. [. z / x ]. ph <-> A. z e. { x e. A | -. ph } [. z / x ]. -. ph )
8 3 7 bitr3i 
 |-  ( -. E. z e. { x e. A | -. ph } [. z / x ]. ph <-> A. z e. { x e. A | -. ph } [. z / x ]. -. ph )
9 df-rab 
 |-  { x e. A | -. ph } = { x | ( x e. A /\ -. ph ) }
10 9 eleq2i 
 |-  ( z e. { x e. A | -. ph } <-> z e. { x | ( x e. A /\ -. ph ) } )
11 df-sbc 
 |-  ( [. z / x ]. ( x e. A /\ -. ph ) <-> z e. { x | ( x e. A /\ -. ph ) } )
12 sbcan 
 |-  ( [. z / x ]. ( x e. A /\ -. ph ) <-> ( [. z / x ]. x e. A /\ [. z / x ]. -. ph ) )
13 sbcel1v 
 |-  ( [. z / x ]. x e. A <-> z e. A )
14 13 anbi1i 
 |-  ( ( [. z / x ]. x e. A /\ [. z / x ]. -. ph ) <-> ( z e. A /\ [. z / x ]. -. ph ) )
15 12 14 bitri 
 |-  ( [. z / x ]. ( x e. A /\ -. ph ) <-> ( z e. A /\ [. z / x ]. -. ph ) )
16 11 15 bitr3i 
 |-  ( z e. { x | ( x e. A /\ -. ph ) } <-> ( z e. A /\ [. z / x ]. -. ph ) )
17 10 16 bitri 
 |-  ( z e. { x e. A | -. ph } <-> ( z e. A /\ [. z / x ]. -. ph ) )
18 17 simprbi 
 |-  ( z e. { x e. A | -. ph } -> [. z / x ]. -. ph )
19 8 18 mprgbir 
 |-  -. E. z e. { x e. A | -. ph } [. z / x ]. ph
20 1 rabex 
 |-  { x e. A | -. ph } e. _V
21 20 biantrur 
 |-  ( R Fr A <-> ( { x e. A | -. ph } e. _V /\ R Fr A ) )
22 rexnal 
 |-  ( E. x e. A -. ph <-> -. A. x e. A ph )
23 rabn0 
 |-  ( { x e. A | -. ph } =/= (/) <-> E. x e. A -. ph )
24 ssrab2 
 |-  { x e. A | -. ph } C_ A
25 24 biantrur 
 |-  ( { x e. A | -. ph } =/= (/) <-> ( { x e. A | -. ph } C_ A /\ { x e. A | -. ph } =/= (/) ) )
26 23 25 bitr3i 
 |-  ( E. x e. A -. ph <-> ( { x e. A | -. ph } C_ A /\ { x e. A | -. ph } =/= (/) ) )
27 22 26 bitr3i 
 |-  ( -. A. x e. A ph <-> ( { x e. A | -. ph } C_ A /\ { x e. A | -. ph } =/= (/) ) )
28 fri 
 |-  ( ( ( { x e. A | -. ph } e. _V /\ R Fr A ) /\ ( { x e. A | -. ph } C_ A /\ { x e. A | -. ph } =/= (/) ) ) -> E. z e. { x e. A | -. ph } A. w e. { x e. A | -. ph } -. w R z )
29 21 27 28 syl2anb 
 |-  ( ( R Fr A /\ -. A. x e. A ph ) -> E. z e. { x e. A | -. ph } A. w e. { x e. A | -. ph } -. w R z )
30 eqid 
 |-  { x e. A | -. ph } = { x e. A | -. ph }
31 30 bnj23 
 |-  ( A. w e. { x e. A | -. ph } -. w R z -> A. y e. A ( y R z -> [. y / x ]. ph ) )
32 df-ral 
 |-  ( A. y e. A ( y R x -> [. y / x ]. ph ) <-> A. y ( y e. A -> ( y R x -> [. y / x ]. ph ) ) )
33 32 sbcbii 
 |-  ( [. z / x ]. A. y e. A ( y R x -> [. y / x ]. ph ) <-> [. z / x ]. A. y ( y e. A -> ( y R x -> [. y / x ]. ph ) ) )
34 sbcal 
 |-  ( [. z / x ]. A. y ( y e. A -> ( y R x -> [. y / x ]. ph ) ) <-> A. y [. z / x ]. ( y e. A -> ( y R x -> [. y / x ]. ph ) ) )
35 sbcimg 
 |-  ( z e. _V -> ( [. z / x ]. ( y e. A -> ( y R x -> [. y / x ]. ph ) ) <-> ( [. z / x ]. y e. A -> [. z / x ]. ( y R x -> [. y / x ]. ph ) ) ) )
36 35 elv 
 |-  ( [. z / x ]. ( y e. A -> ( y R x -> [. y / x ]. ph ) ) <-> ( [. z / x ]. y e. A -> [. z / x ]. ( y R x -> [. y / x ]. ph ) ) )
37 vex 
 |-  z e. _V
38 nfv 
 |-  F/ x y e. A
39 37 38 sbcgfi 
 |-  ( [. z / x ]. y e. A <-> y e. A )
40 sbcimg 
 |-  ( z e. _V -> ( [. z / x ]. ( y R x -> [. y / x ]. ph ) <-> ( [. z / x ]. y R x -> [. z / x ]. [. y / x ]. ph ) ) )
41 40 elv 
 |-  ( [. z / x ]. ( y R x -> [. y / x ]. ph ) <-> ( [. z / x ]. y R x -> [. z / x ]. [. y / x ]. ph ) )
42 sbcbr2g 
 |-  ( z e. _V -> ( [. z / x ]. y R x <-> y R [_ z / x ]_ x ) )
43 42 elv 
 |-  ( [. z / x ]. y R x <-> y R [_ z / x ]_ x )
44 37 csbvargi 
 |-  [_ z / x ]_ x = z
45 44 breq2i 
 |-  ( y R [_ z / x ]_ x <-> y R z )
46 43 45 bitri 
 |-  ( [. z / x ]. y R x <-> y R z )
47 nfsbc1v 
 |-  F/ x [. y / x ]. ph
48 37 47 sbcgfi 
 |-  ( [. z / x ]. [. y / x ]. ph <-> [. y / x ]. ph )
49 46 48 imbi12i 
 |-  ( ( [. z / x ]. y R x -> [. z / x ]. [. y / x ]. ph ) <-> ( y R z -> [. y / x ]. ph ) )
50 41 49 bitri 
 |-  ( [. z / x ]. ( y R x -> [. y / x ]. ph ) <-> ( y R z -> [. y / x ]. ph ) )
51 39 50 imbi12i 
 |-  ( ( [. z / x ]. y e. A -> [. z / x ]. ( y R x -> [. y / x ]. ph ) ) <-> ( y e. A -> ( y R z -> [. y / x ]. ph ) ) )
52 36 51 bitri 
 |-  ( [. z / x ]. ( y e. A -> ( y R x -> [. y / x ]. ph ) ) <-> ( y e. A -> ( y R z -> [. y / x ]. ph ) ) )
53 52 albii 
 |-  ( A. y [. z / x ]. ( y e. A -> ( y R x -> [. y / x ]. ph ) ) <-> A. y ( y e. A -> ( y R z -> [. y / x ]. ph ) ) )
54 34 53 bitri 
 |-  ( [. z / x ]. A. y ( y e. A -> ( y R x -> [. y / x ]. ph ) ) <-> A. y ( y e. A -> ( y R z -> [. y / x ]. ph ) ) )
55 33 54 bitri 
 |-  ( [. z / x ]. A. y e. A ( y R x -> [. y / x ]. ph ) <-> A. y ( y e. A -> ( y R z -> [. y / x ]. ph ) ) )
56 2 sbcbii 
 |-  ( [. z / x ]. ps <-> [. z / x ]. A. y e. A ( y R x -> [. y / x ]. ph ) )
57 df-ral 
 |-  ( A. y e. A ( y R z -> [. y / x ]. ph ) <-> A. y ( y e. A -> ( y R z -> [. y / x ]. ph ) ) )
58 55 56 57 3bitr4i 
 |-  ( [. z / x ]. ps <-> A. y e. A ( y R z -> [. y / x ]. ph ) )
59 31 58 sylibr 
 |-  ( A. w e. { x e. A | -. ph } -. w R z -> [. z / x ]. ps )
60 29 59 bnj31 
 |-  ( ( R Fr A /\ -. A. x e. A ph ) -> E. z e. { x e. A | -. ph } [. z / x ]. ps )
61 nfv 
 |-  F/ z ( ps -> ph )
62 nfsbc1v 
 |-  F/ x [. z / x ]. ps
63 nfsbc1v 
 |-  F/ x [. z / x ]. ph
64 62 63 nfim 
 |-  F/ x ( [. z / x ]. ps -> [. z / x ]. ph )
65 sbceq1a 
 |-  ( x = z -> ( ps <-> [. z / x ]. ps ) )
66 sbceq1a 
 |-  ( x = z -> ( ph <-> [. z / x ]. ph ) )
67 65 66 imbi12d 
 |-  ( x = z -> ( ( ps -> ph ) <-> ( [. z / x ]. ps -> [. z / x ]. ph ) ) )
68 61 64 67 cbvralw 
 |-  ( A. x e. A ( ps -> ph ) <-> A. z e. A ( [. z / x ]. ps -> [. z / x ]. ph ) )
69 elrabi 
 |-  ( z e. { x e. A | -. ph } -> z e. A )
70 69 imim1i 
 |-  ( ( z e. A -> ( [. z / x ]. ps -> [. z / x ]. ph ) ) -> ( z e. { x e. A | -. ph } -> ( [. z / x ]. ps -> [. z / x ]. ph ) ) )
71 70 ralimi2 
 |-  ( A. z e. A ( [. z / x ]. ps -> [. z / x ]. ph ) -> A. z e. { x e. A | -. ph } ( [. z / x ]. ps -> [. z / x ]. ph ) )
72 68 71 sylbi 
 |-  ( A. x e. A ( ps -> ph ) -> A. z e. { x e. A | -. ph } ( [. z / x ]. ps -> [. z / x ]. ph ) )
73 rexim 
 |-  ( A. z e. { x e. A | -. ph } ( [. z / x ]. ps -> [. z / x ]. ph ) -> ( E. z e. { x e. A | -. ph } [. z / x ]. ps -> E. z e. { x e. A | -. ph } [. z / x ]. ph ) )
74 72 73 syl 
 |-  ( A. x e. A ( ps -> ph ) -> ( E. z e. { x e. A | -. ph } [. z / x ]. ps -> E. z e. { x e. A | -. ph } [. z / x ]. ph ) )
75 60 74 mpan9 
 |-  ( ( ( R Fr A /\ -. A. x e. A ph ) /\ A. x e. A ( ps -> ph ) ) -> E. z e. { x e. A | -. ph } [. z / x ]. ph )
76 75 an32s 
 |-  ( ( ( R Fr A /\ A. x e. A ( ps -> ph ) ) /\ -. A. x e. A ph ) -> E. z e. { x e. A | -. ph } [. z / x ]. ph )
77 19 76 mto 
 |-  -. ( ( R Fr A /\ A. x e. A ( ps -> ph ) ) /\ -. A. x e. A ph )
78 iman 
 |-  ( ( ( R Fr A /\ A. x e. A ( ps -> ph ) ) -> A. x e. A ph ) <-> -. ( ( R Fr A /\ A. x e. A ( ps -> ph ) ) /\ -. A. x e. A ph ) )
79 77 78 mpbir 
 |-  ( ( R Fr A /\ A. x e. A ( ps -> ph ) ) -> A. x e. A ph )