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

Theorem bnj110 27579
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
StepHypRef Expression
1 ralnex 2517 . . . . 5  |-  ( A. z  e.  { x  e.  A  |  -.  ph }  -.  [. z  /  x ]. ph  <->  -.  E. z  e.  { x  e.  A  |  -.  ph } [. z  /  x ]. ph )
2 vex 2730 . . . . . . . 8  |-  z  e. 
_V
3 sbcng 2961 . . . . . . . 8  |-  ( z  e.  _V  ->  ( [. z  /  x ].  -.  ph  <->  -.  [. z  /  x ]. ph ) )
42, 3ax-mp 10 . . . . . . 7  |-  ( [. z  /  x ].  -.  ph  <->  -. 
[. z  /  x ]. ph )
54bicomi 195 . . . . . 6  |-  ( -. 
[. z  /  x ]. ph  <->  [. z  /  x ].  -.  ph )
65ralbii 2531 . . . . 5  |-  ( A. z  e.  { x  e.  A  |  -.  ph }  -.  [. z  /  x ]. ph  <->  A. z  e.  { x  e.  A  |  -.  ph } [. z  /  x ].  -.  ph )
71, 6bitr3i 244 . . . 4  |-  ( -. 
E. z  e.  {
x  e.  A  |  -.  ph } [. z  /  x ]. ph  <->  A. z  e.  { x  e.  A  |  -.  ph } [. z  /  x ].  -.  ph )
8 df-rab 2516 . . . . . . 7  |-  { x  e.  A  |  -.  ph }  =  { x  |  ( x  e.  A  /\  -.  ph ) }
98eleq2i 2317 . . . . . 6  |-  ( z  e.  { x  e.  A  |  -.  ph } 
<->  z  e.  { x  |  ( x  e.  A  /\  -.  ph ) } )
10 df-sbc 2922 . . . . . . 7  |-  ( [. z  /  x ]. (
x  e.  A  /\  -.  ph )  <->  z  e.  { x  |  ( x  e.  A  /\  -.  ph ) } )
11 sbcan 2963 . . . . . . . 8  |-  ( [. z  /  x ]. (
x  e.  A  /\  -.  ph )  <->  ( [. z  /  x ]. x  e.  A  /\  [. z  /  x ].  -.  ph ) )
12 sbcel1gv 2980 . . . . . . . . . 10  |-  ( z  e.  _V  ->  ( [. z  /  x ]. x  e.  A  <->  z  e.  A ) )
132, 12ax-mp 10 . . . . . . . . 9  |-  ( [. z  /  x ]. x  e.  A  <->  z  e.  A
)
1413anbi1i 679 . . . . . . . 8  |-  ( (
[. z  /  x ]. x  e.  A  /\  [. z  /  x ].  -.  ph )  <->  ( z  e.  A  /\  [. z  /  x ].  -.  ph ) )
1511, 14bitri 242 . . . . . . 7  |-  ( [. z  /  x ]. (
x  e.  A  /\  -.  ph )  <->  ( z  e.  A  /\  [. z  /  x ].  -.  ph ) )
1610, 15bitr3i 244 . . . . . 6  |-  ( z  e.  { x  |  ( x  e.  A  /\  -.  ph ) }  <-> 
( z  e.  A  /\  [. z  /  x ].  -.  ph ) )
179, 16bitri 242 . . . . 5  |-  ( z  e.  { x  e.  A  |  -.  ph } 
<->  ( z  e.  A  /\  [. z  /  x ].  -.  ph ) )
1817simprbi 452 . . . 4  |-  ( z  e.  { x  e.  A  |  -.  ph }  ->  [. z  /  x ].  -.  ph )
197, 18mprgbir 2575 . . 3  |-  -.  E. z  e.  { x  e.  A  |  -.  ph } [. z  /  x ]. ph
20 bnj110.1 . . . . . . . . 9  |-  A  e. 
_V
2120rabex 4061 . . . . . . . 8  |-  { x  e.  A  |  -.  ph }  e.  _V
2221biantrur 494 . . . . . . 7  |-  ( R  Fr  A  <->  ( {
x  e.  A  |  -.  ph }  e.  _V  /\  R  Fr  A ) )
23 rexnal 2518 . . . . . . . 8  |-  ( E. x  e.  A  -.  ph  <->  -. 
A. x  e.  A  ph )
24 rabn0 3381 . . . . . . . . 9  |-  ( { x  e.  A  |  -.  ph }  =/=  (/)  <->  E. x  e.  A  -.  ph )
25 ssrab2 3179 . . . . . . . . . 10  |-  { x  e.  A  |  -.  ph }  C_  A
2625biantrur 494 . . . . . . . . 9  |-  ( { x  e.  A  |  -.  ph }  =/=  (/)  <->  ( {
x  e.  A  |  -.  ph }  C_  A  /\  { x  e.  A  |  -.  ph }  =/=  (/) ) )
2724, 26bitr3i 244 . . . . . . . 8  |-  ( E. x  e.  A  -.  ph  <->  ( { x  e.  A  |  -.  ph }  C_  A  /\  { x  e.  A  |  -.  ph }  =/=  (/) ) )
2823, 27bitr3i 244 . . . . . . 7  |-  ( -. 
A. x  e.  A  ph  <->  ( { x  e.  A  |  -.  ph }  C_  A  /\  { x  e.  A  |  -.  ph }  =/=  (/) ) )
29 fri 4248 . . . . . . 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 467 . . . . . 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 eqid1 20670 . . . . . . . 8  |-  { x  e.  A  |  -.  ph }  =  { x  e.  A  |  -.  ph }
3231bnj23 27433 . . . . . . 7  |-  ( A. w  e.  { x  e.  A  |  -.  ph }  -.  w R z  ->  A. y  e.  A  ( y R z  ->  [. y  /  x ]. ph )
)
33 df-ral 2513 . . . . . . . . . 10  |-  ( A. y  e.  A  (
y R x  ->  [. y  /  x ]. ph )  <->  A. y
( y  e.  A  ->  ( y R x  ->  [. y  /  x ]. ph ) ) )
3433sbcbii 2976 . . . . . . . . 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 2968 . . . . . . . . . 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 2962 . . . . . . . . . . . . 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 10 . . . . . . . . . . . 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 1629 . . . . . . . . . . . . . . 15  |-  F/ x  y  e.  A
3938sbcgf 2984 . . . . . . . . . . . . . 14  |-  ( z  e.  _V  ->  ( [. z  /  x ]. y  e.  A  <->  y  e.  A ) )
402, 39ax-mp 10 . . . . . . . . . . . . 13  |-  ( [. z  /  x ]. y  e.  A  <->  y  e.  A
)
41 sbcimg 2962 . . . . . . . . . . . . . . 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 10 . . . . . . . . . . . . . 14  |-  ( [. z  /  x ]. (
y R x  ->  [. y  /  x ]. ph )  <->  ( [. z  /  x ]. y R x  ->  [. z  /  x ]. [. y  /  x ]. ph )
)
43 sbcbr2g 3972 . . . . . . . . . . . . . . . . 17  |-  ( z  e.  _V  ->  ( [. z  /  x ]. y R x  <->  y R [_ z  /  x ]_ x ) )
442, 43ax-mp 10 . . . . . . . . . . . . . . . 16  |-  ( [. z  /  x ]. y R x  <->  y R [_ z  /  x ]_ x
)
45 csbvarg 3036 . . . . . . . . . . . . . . . . . 18  |-  ( z  e.  _V  ->  [_ z  /  x ]_ x  =  z )
462, 45ax-mp 10 . . . . . . . . . . . . . . . . 17  |-  [_ z  /  x ]_ x  =  z
4746breq2i 3928 . . . . . . . . . . . . . . . 16  |-  ( y R [_ z  /  x ]_ x  <->  y R
z )
4844, 47bitri 242 . . . . . . . . . . . . . . 15  |-  ( [. z  /  x ]. y R x  <->  y R z )
49 nfsbc1v 2940 . . . . . . . . . . . . . . . . 17  |-  F/ x [. y  /  x ]. ph
5049sbcgf 2984 . . . . . . . . . . . . . . . 16  |-  ( z  e.  _V  ->  ( [. z  /  x ]. [. y  /  x ]. ph  <->  [. y  /  x ]. ph ) )
512, 50ax-mp 10 . . . . . . . . . . . . . . 15  |-  ( [. z  /  x ]. [. y  /  x ]. ph  <->  [. y  /  x ]. ph )
5248, 51imbi12i 318 . . . . . . . . . . . . . 14  |-  ( (
[. z  /  x ]. y R x  ->  [. z  /  x ]. [. y  /  x ]. ph )  <->  ( y R z  ->  [. y  /  x ]. ph )
)
5342, 52bitri 242 . . . . . . . . . . . . 13  |-  ( [. z  /  x ]. (
y R x  ->  [. y  /  x ]. ph )  <->  ( y R z  ->  [. y  /  x ]. ph )
)
5440, 53imbi12i 318 . . . . . . . . . . . 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 242 . . . . . . . . . . 11  |-  ( [. z  /  x ]. (
y  e.  A  -> 
( y R x  ->  [. y  /  x ]. ph ) )  <->  ( y  e.  A  ->  ( y R z  ->  [. y  /  x ]. ph )
) )
5655albii 1554 . . . . . . . . . 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 242 . . . . . . . . 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 242 . . . . . . . 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 2976 . . . . . . . 8  |-  ( [. z  /  x ]. ps  <->  [. z  /  x ]. A. y  e.  A  ( y R x  ->  [. y  /  x ]. ph ) )
61 df-ral 2513 . . . . . . . 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 270 . . . . . . 7  |-  ( [. z  /  x ]. ps  <->  A. y  e.  A  ( y R z  ->  [. y  /  x ]. ph ) )
6332, 62sylibr 205 . . . . . 6  |-  ( A. w  e.  { x  e.  A  |  -.  ph }  -.  w R z  ->  [. z  /  x ]. ps )
6430, 63bnj31 27434 . . . . 5  |-  ( ( R  Fr  A  /\  -.  A. x  e.  A  ph )  ->  E. z  e.  { x  e.  A  |  -.  ph } [. z  /  x ]. ps )
65 nfv 1629 . . . . . . . 8  |-  F/ z ( ps  ->  ph )
66 nfsbc1v 2940 . . . . . . . . 9  |-  F/ x [. z  /  x ]. ps
67 nfsbc1v 2940 . . . . . . . . 9  |-  F/ x [. z  /  x ]. ph
6866, 67nfim 1735 . . . . . . . 8  |-  F/ x
( [. z  /  x ]. ps  ->  [. z  /  x ]. ph )
69 sbceq1a 2931 . . . . . . . . 9  |-  ( x  =  z  ->  ( ps 
<-> 
[. z  /  x ]. ps ) )
70 sbceq1a 2931 . . . . . . . . 9  |-  ( x  =  z  ->  ( ph 
<-> 
[. z  /  x ]. ph ) )
7169, 70imbi12d 313 . . . . . . . 8  |-  ( x  =  z  ->  (
( ps  ->  ph )  <->  (
[. z  /  x ]. ps  ->  [. z  /  x ]. ph ) ) )
7265, 68, 71cbvral 2705 . . . . . . 7  |-  ( A. x  e.  A  ( ps  ->  ph )  <->  A. z  e.  A  ( [. z  /  x ]. ps  ->  [. z  /  x ]. ph ) )
7325sseli 3099 . . . . . . . . 9  |-  ( z  e.  { x  e.  A  |  -.  ph }  ->  z  e.  A
)
7473imim1i 56 . . . . . . . 8  |-  ( ( z  e.  A  -> 
( [. z  /  x ]. ps  ->  [. z  /  x ]. ph ) )  ->  ( z  e. 
{ x  e.  A  |  -.  ph }  ->  (
[. z  /  x ]. ps  ->  [. z  /  x ]. ph ) ) )
7574ralimi2 2577 . . . . . . 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 189 . . . . . 6  |-  ( A. x  e.  A  ( ps  ->  ph )  ->  A. z  e.  { x  e.  A  |  -.  ph }  ( [. z  /  x ]. ps  ->  [. z  /  x ]. ph ) )
77 rexim 2609 . . . . . 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 17 . . . . 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 457 . . . 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 782 . . 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 169 . 2  |-  -.  (
( R  Fr  A  /\  A. x  e.  A  ( ps  ->  ph )
)  /\  -.  A. x  e.  A  ph )
82 iman 415 . 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 202 1  |-  ( ( R  Fr  A  /\  A. x  e.  A  ( ps  ->  ph ) )  ->  A. x  e.  A  ph )
Colors of variables: wff set class
Syntax hints:   -. wn 5    -> wi 6    <-> wb 178    /\ wa 360   A.wal 1532    = wceq 1619    e. wcel 1621   {cab 2239    =/= wne 2412   A.wral 2509   E.wrex 2510   {crab 2512   _Vcvv 2727   [.wsbc 2921   [_csb 3009    C_ wss 3078   (/)c0 3362   class class class wbr 3920    Fr wfr 4242
This theorem is referenced by:  bnj157  27580  bnj580  27634  bnj1052  27694  bnj1030  27706  bnj1133  27708
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234  ax-sep 4038
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-ne 2414  df-ral 2513  df-rex 2514  df-rab 2516  df-v 2729  df-sbc 2922  df-csb 3010  df-dif 3081  df-un 3083  df-in 3085  df-ss 3089  df-nul 3363  df-if 3471  df-sn 3550  df-pr 3551  df-op 3553  df-br 3921  df-fr 4245
  Copyright terms: Public domain W3C validator