Users' Mathboxes Mathbox for Jonathan Ben-Naim < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bnj110 Unicode version

Theorem bnj110 29206
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.)
Hypotheses
Ref Expression
bnj110.1  |-  A  e. 
_V
bnj110.2  |-  ( ps  <->  A. y  e.  A  ( y R x  ->  [. y  /  x ]. ph ) )
Assertion
Ref Expression
bnj110  |-  ( ( R  Fr  A  /\  A. x  e.  A  ( ps  ->  ph ) )  ->  A. x  e.  A  ph )
Distinct variable groups:    x, A, y    x, R, y    ph, y
Allowed substitution hints:    ph( x)    ps( x, y)

Proof of Theorem bnj110
Dummy variables  z  w are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ralnex 2566 . . . . 5  |-  ( A. z  e.  { x  e.  A  |  -.  ph }  -.  [. z  /  x ]. ph  <->  -.  E. z  e.  { x  e.  A  |  -.  ph } [. z  /  x ]. ph )
2 vex 2804 . . . . . . . 8  |-  z  e. 
_V
3 sbcng 3044 . . . . . . . 8  |-  ( z  e.  _V  ->  ( [. z  /  x ].  -.  ph  <->  -.  [. z  /  x ]. ph ) )
42, 3ax-mp 8 . . . . . . 7  |-  ( [. z  /  x ].  -.  ph  <->  -. 
[. z  /  x ]. ph )
54bicomi 193 . . . . . 6  |-  ( -. 
[. z  /  x ]. ph  <->  [. z  /  x ].  -.  ph )
65ralbii 2580 . . . . 5  |-  ( A. z  e.  { x  e.  A  |  -.  ph }  -.  [. z  /  x ]. ph  <->  A. z  e.  { x  e.  A  |  -.  ph } [. z  /  x ].  -.  ph )
71, 6bitr3i 242 . . . 4  |-  ( -. 
E. z  e.  {
x  e.  A  |  -.  ph } [. z  /  x ]. ph  <->  A. z  e.  { x  e.  A  |  -.  ph } [. z  /  x ].  -.  ph )
8 df-rab 2565 . . . . . . 7  |-  { x  e.  A  |  -.  ph }  =  { x  |  ( x  e.  A  /\  -.  ph ) }
98eleq2i 2360 . . . . . 6  |-  ( z  e.  { x  e.  A  |  -.  ph } 
<->  z  e.  { x  |  ( x  e.  A  /\  -.  ph ) } )
10 df-sbc 3005 . . . . . . 7  |-  ( [. z  /  x ]. (
x  e.  A  /\  -.  ph )  <->  z  e.  { x  |  ( x  e.  A  /\  -.  ph ) } )
11 sbcan 3046 . . . . . . . 8  |-  ( [. z  /  x ]. (
x  e.  A  /\  -.  ph )  <->  ( [. z  /  x ]. x  e.  A  /\  [. z  /  x ].  -.  ph ) )
12 sbcel1gv 3063 . . . . . . . . . 10  |-  ( z  e.  _V  ->  ( [. z  /  x ]. x  e.  A  <->  z  e.  A ) )
132, 12ax-mp 8 . . . . . . . . 9  |-  ( [. z  /  x ]. x  e.  A  <->  z  e.  A
)
1413anbi1i 676 . . . . . . . 8  |-  ( (
[. z  /  x ]. x  e.  A  /\  [. z  /  x ].  -.  ph )  <->  ( z  e.  A  /\  [. z  /  x ].  -.  ph ) )
1511, 14bitri 240 . . . . . . 7  |-  ( [. z  /  x ]. (
x  e.  A  /\  -.  ph )  <->  ( z  e.  A  /\  [. z  /  x ].  -.  ph ) )
1610, 15bitr3i 242 . . . . . 6  |-  ( z  e.  { x  |  ( x  e.  A  /\  -.  ph ) }  <-> 
( z  e.  A  /\  [. z  /  x ].  -.  ph ) )
179, 16bitri 240 . . . . 5  |-  ( z  e.  { x  e.  A  |  -.  ph } 
<->  ( z  e.  A  /\  [. z  /  x ].  -.  ph ) )
1817simprbi 450 . . . 4  |-  ( z  e.  { x  e.  A  |  -.  ph }  ->  [. z  /  x ].  -.  ph )
197, 18mprgbir 2626 . . 3  |-  -.  E. z  e.  { x  e.  A  |  -.  ph } [. z  /  x ]. ph
20 bnj110.1 . . . . . . . . 9  |-  A  e. 
_V
2120rabex 4181 . . . . . . . 8  |-  { x  e.  A  |  -.  ph }  e.  _V
2221biantrur 492 . . . . . . 7  |-  ( R  Fr  A  <->  ( {
x  e.  A  |  -.  ph }  e.  _V  /\  R  Fr  A ) )
23 rexnal 2567 . . . . . . . 8  |-  ( E. x  e.  A  -.  ph  <->  -. 
A. x  e.  A  ph )
24 rabn0 3487 . . . . . . . . 9  |-  ( { x  e.  A  |  -.  ph }  =/=  (/)  <->  E. x  e.  A  -.  ph )
25 ssrab2 3271 . . . . . . . . . 10  |-  { x  e.  A  |  -.  ph }  C_  A
2625biantrur 492 . . . . . . . . 9  |-  ( { x  e.  A  |  -.  ph }  =/=  (/)  <->  ( {
x  e.  A  |  -.  ph }  C_  A  /\  { x  e.  A  |  -.  ph }  =/=  (/) ) )
2724, 26bitr3i 242 . . . . . . . 8  |-  ( E. x  e.  A  -.  ph  <->  ( { x  e.  A  |  -.  ph }  C_  A  /\  { x  e.  A  |  -.  ph }  =/=  (/) ) )
2823, 27bitr3i 242 . . . . . . 7  |-  ( -. 
A. x  e.  A  ph  <->  ( { x  e.  A  |  -.  ph }  C_  A  /\  { x  e.  A  |  -.  ph }  =/=  (/) ) )
29 fri 4371 . . . . . . 7  |-  ( ( ( { 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 )
3022, 28, 29syl2anb 465 . . . . . 6  |-  ( ( 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 )
31 eqid 2296 . . . . . . . 8  |-  { x  e.  A  |  -.  ph }  =  { x  e.  A  |  -.  ph }
3231bnj23 29060 . . . . . . 7  |-  ( A. w  e.  { x  e.  A  |  -.  ph }  -.  w R z  ->  A. y  e.  A  ( y R z  ->  [. y  /  x ]. ph )
)
33 df-ral 2561 . . . . . . . . . 10  |-  ( A. y  e.  A  (
y R x  ->  [. y  /  x ]. ph )  <->  A. y
( y  e.  A  ->  ( y R x  ->  [. y  /  x ]. ph ) ) )
3433sbcbii 3059 . . . . . . . . 9  |-  ( [. 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 ) ) )
35 sbcal 3051 . . . . . . . . . 10  |-  ( [. 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 ) ) )
36 sbcimg 3045 . . . . . . . . . . . . 13  |-  ( 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 )
) ) )
372, 36ax-mp 8 . . . . . . . . . . . 12  |-  ( [. z  /  x ]. (
y  e.  A  -> 
( y R x  ->  [. y  /  x ]. ph ) )  <->  ( [. z  /  x ]. y  e.  A  ->  [. z  /  x ]. ( y R x  ->  [. y  /  x ]. ph )
) )
38 nfv 1609 . . . . . . . . . . . . . . 15  |-  F/ x  y  e.  A
3938sbcgf 3067 . . . . . . . . . . . . . 14  |-  ( z  e.  _V  ->  ( [. z  /  x ]. y  e.  A  <->  y  e.  A ) )
402, 39ax-mp 8 . . . . . . . . . . . . 13  |-  ( [. z  /  x ]. y  e.  A  <->  y  e.  A
)
41 sbcimg 3045 . . . . . . . . . . . . . . 15  |-  ( z  e.  _V  ->  ( [. z  /  x ]. ( y R x  ->  [. y  /  x ]. ph )  <->  ( [. z  /  x ]. y R x  ->  [. z  /  x ]. [. y  /  x ]. ph )
) )
422, 41ax-mp 8 . . . . . . . . . . . . . 14  |-  ( [. z  /  x ]. (
y R x  ->  [. y  /  x ]. ph )  <->  ( [. z  /  x ]. y R x  ->  [. z  /  x ]. [. y  /  x ]. ph )
)
43 sbcbr2g 4091 . . . . . . . . . . . . . . . . 17  |-  ( z  e.  _V  ->  ( [. z  /  x ]. y R x  <->  y R [_ z  /  x ]_ x ) )
442, 43ax-mp 8 . . . . . . . . . . . . . . . 16  |-  ( [. z  /  x ]. y R x  <->  y R [_ z  /  x ]_ x
)
45 csbvarg 3121 . . . . . . . . . . . . . . . . . 18  |-  ( z  e.  _V  ->  [_ z  /  x ]_ x  =  z )
462, 45ax-mp 8 . . . . . . . . . . . . . . . . 17  |-  [_ z  /  x ]_ x  =  z
4746breq2i 4047 . . . . . . . . . . . . . . . 16  |-  ( y R [_ z  /  x ]_ x  <->  y R
z )
4844, 47bitri 240 . . . . . . . . . . . . . . 15  |-  ( [. z  /  x ]. y R x  <->  y R z )
49 nfsbc1v 3023 . . . . . . . . . . . . . . . . 17  |-  F/ x [. y  /  x ]. ph
5049sbcgf 3067 . . . . . . . . . . . . . . . 16  |-  ( z  e.  _V  ->  ( [. z  /  x ]. [. y  /  x ]. ph  <->  [. y  /  x ]. ph ) )
512, 50ax-mp 8 . . . . . . . . . . . . . . 15  |-  ( [. z  /  x ]. [. y  /  x ]. ph  <->  [. y  /  x ]. ph )
5248, 51imbi12i 316 . . . . . . . . . . . . . 14  |-  ( (
[. z  /  x ]. y R x  ->  [. z  /  x ]. [. y  /  x ]. ph )  <->  ( y R z  ->  [. y  /  x ]. ph )
)
5342, 52bitri 240 . . . . . . . . . . . . 13  |-  ( [. z  /  x ]. (
y R x  ->  [. y  /  x ]. ph )  <->  ( y R z  ->  [. y  /  x ]. ph )
)
5440, 53imbi12i 316 . . . . . . . . . . . 12  |-  ( (
[. z  /  x ]. y  e.  A  ->  [. z  /  x ]. ( y R x  ->  [. y  /  x ]. ph ) )  <->  ( y  e.  A  ->  ( y R z  ->  [. y  /  x ]. ph )
) )
5537, 54bitri 240 . . . . . . . . . . 11  |-  ( [. z  /  x ]. (
y  e.  A  -> 
( y R x  ->  [. y  /  x ]. ph ) )  <->  ( y  e.  A  ->  ( y R z  ->  [. y  /  x ]. ph )
) )
5655albii 1556 . . . . . . . . . 10  |-  ( A. y [. z  /  x ]. ( y  e.  A  ->  ( y R x  ->  [. y  /  x ]. ph ) )  <->  A. y
( y  e.  A  ->  ( y R z  ->  [. y  /  x ]. ph ) ) )
5735, 56bitri 240 . . . . . . . . 9  |-  ( [. z  /  x ]. A. y ( y  e.  A  ->  ( y R x  ->  [. y  /  x ]. ph )
)  <->  A. y ( y  e.  A  ->  (
y R z  ->  [. y  /  x ]. ph ) ) )
5834, 57bitri 240 . . . . . . . 8  |-  ( [. z  /  x ]. A. y  e.  A  (
y R x  ->  [. y  /  x ]. ph )  <->  A. y
( y  e.  A  ->  ( y R z  ->  [. y  /  x ]. ph ) ) )
59 bnj110.2 . . . . . . . . 9  |-  ( ps  <->  A. y  e.  A  ( y R x  ->  [. y  /  x ]. ph ) )
6059sbcbii 3059 . . . . . . . 8  |-  ( [. z  /  x ]. ps  <->  [. z  /  x ]. A. y  e.  A  ( y R x  ->  [. y  /  x ]. ph ) )
61 df-ral 2561 . . . . . . . 8  |-  ( A. y  e.  A  (
y R z  ->  [. y  /  x ]. ph )  <->  A. y
( y  e.  A  ->  ( y R z  ->  [. y  /  x ]. ph ) ) )
6258, 60, 613bitr4i 268 . . . . . . 7  |-  ( [. z  /  x ]. ps  <->  A. y  e.  A  ( y R z  ->  [. y  /  x ]. ph ) )
6332, 62sylibr 203 . . . . . 6  |-  ( A. w  e.  { x  e.  A  |  -.  ph }  -.  w R z  ->  [. z  /  x ]. ps )
6430, 63bnj31 29061 . . . . 5  |-  ( ( R  Fr  A  /\  -.  A. x  e.  A  ph )  ->  E. z  e.  { x  e.  A  |  -.  ph } [. z  /  x ]. ps )
65 nfv 1609 . . . . . . . 8  |-  F/ z ( ps  ->  ph )
66 nfsbc1v 3023 . . . . . . . . 9  |-  F/ x [. z  /  x ]. ps
67 nfsbc1v 3023 . . . . . . . . 9  |-  F/ x [. z  /  x ]. ph
6866, 67nfim 1781 . . . . . . . 8  |-  F/ x
( [. z  /  x ]. ps  ->  [. z  /  x ]. ph )
69 sbceq1a 3014 . . . . . . . . 9  |-  ( x  =  z  ->  ( ps 
<-> 
[. z  /  x ]. ps ) )
70 sbceq1a 3014 . . . . . . . . 9  |-  ( x  =  z  ->  ( ph 
<-> 
[. z  /  x ]. ph ) )
7169, 70imbi12d 311 . . . . . . . 8  |-  ( x  =  z  ->  (
( ps  ->  ph )  <->  (
[. z  /  x ]. ps  ->  [. z  /  x ]. ph ) ) )
7265, 68, 71cbvral 2773 . . . . . . 7  |-  ( A. x  e.  A  ( ps  ->  ph )  <->  A. z  e.  A  ( [. z  /  x ]. ps  ->  [. z  /  x ]. ph ) )
7325sseli 3189 . . . . . . . . 9  |-  ( z  e.  { x  e.  A  |  -.  ph }  ->  z  e.  A
)
7473imim1i 54 . . . . . . . 8  |-  ( ( z  e.  A  -> 
( [. z  /  x ]. ps  ->  [. z  /  x ]. ph ) )  ->  ( z  e. 
{ x  e.  A  |  -.  ph }  ->  (
[. z  /  x ]. ps  ->  [. z  /  x ]. ph ) ) )
7574ralimi2 2628 . . . . . . 7  |-  ( A. z  e.  A  ( [. z  /  x ]. ps  ->  [. z  /  x ]. ph )  ->  A. z  e.  { x  e.  A  |  -.  ph }  ( [. z  /  x ]. ps  ->  [. z  /  x ]. ph ) )
7672, 75sylbi 187 . . . . . 6  |-  ( A. x  e.  A  ( ps  ->  ph )  ->  A. z  e.  { x  e.  A  |  -.  ph }  ( [. z  /  x ]. ps  ->  [. z  /  x ]. ph ) )
77 rexim 2660 . . . . . 6  |-  ( 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 )
)
7876, 77syl 15 . . . . 5  |-  ( 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 )
)
7964, 78mpan9 455 . . . 4  |-  ( ( ( R  Fr  A  /\  -.  A. x  e.  A  ph )  /\  A. x  e.  A  ( ps  ->  ph ) )  ->  E. z  e.  {
x  e.  A  |  -.  ph } [. z  /  x ]. ph )
8079an32s 779 . . 3  |-  ( ( ( R  Fr  A  /\  A. x  e.  A  ( ps  ->  ph )
)  /\  -.  A. x  e.  A  ph )  ->  E. z  e.  { x  e.  A  |  -.  ph } [. z  /  x ]. ph )
8119, 80mto 167 . 2  |-  -.  (
( R  Fr  A  /\  A. x  e.  A  ( ps  ->  ph )
)  /\  -.  A. x  e.  A  ph )
82 iman 413 . 2  |-  ( ( ( 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 ) )
8381, 82mpbir 200 1  |-  ( ( R  Fr  A  /\  A. x  e.  A  ( ps  ->  ph ) )  ->  A. x  e.  A  ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    /\ wa 358   A.wal 1530    = wceq 1632    e. wcel 1696   {cab 2282    =/= wne 2459   A.wral 2556   E.wrex 2557   {crab 2560   _Vcvv 2801   [.wsbc 3004   [_csb 3094    C_ wss 3165   (/)c0 3468   class class class wbr 4039    Fr wfr 4365
This theorem is referenced by:  bnj157  29207  bnj580  29261  bnj1052  29321  bnj1030  29333  bnj1133  29335
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-ral 2561  df-rex 2562  df-rab 2565  df-v 2803  df-sbc 3005  df-csb 3095  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-br 4040  df-fr 4368
  Copyright terms: Public domain W3C validator