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

Theorem bnj110 29231
 Description: Well-founded induction restricted to a set ( ). 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
bnj110.2
Assertion
Ref Expression
bnj110
Distinct variable groups:   ,,   ,,   ,
Allowed substitution hints:   ()   (,)

Proof of Theorem bnj110
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ralnex 2717 . . . . 5
2 vex 2961 . . . . . . . 8
3 sbcng 3203 . . . . . . . 8
42, 3ax-mp 8 . . . . . . 7
54bicomi 195 . . . . . 6
65ralbii 2731 . . . . 5
71, 6bitr3i 244 . . . 4
8 df-rab 2716 . . . . . . 7
98eleq2i 2502 . . . . . 6
10 df-sbc 3164 . . . . . . 7
11 sbcan 3205 . . . . . . . 8
12 sbcel1gv 3222 . . . . . . . . . 10
132, 12ax-mp 8 . . . . . . . . 9
1413anbi1i 678 . . . . . . . 8
1511, 14bitri 242 . . . . . . 7
1610, 15bitr3i 244 . . . . . 6
179, 16bitri 242 . . . . 5
1817simprbi 452 . . . 4
197, 18mprgbir 2778 . . 3
20 bnj110.1 . . . . . . . . 9
2120rabex 4356 . . . . . . . 8
2221biantrur 494 . . . . . . 7
23 rexnal 2718 . . . . . . . 8
24 rabn0 3649 . . . . . . . . 9
25 ssrab2 3430 . . . . . . . . . 10
2625biantrur 494 . . . . . . . . 9
2724, 26bitr3i 244 . . . . . . . 8
2823, 27bitr3i 244 . . . . . . 7
29 fri 4546 . . . . . . 7
3022, 28, 29syl2anb 467 . . . . . 6
31 eqid 2438 . . . . . . . 8
3231bnj23 29085 . . . . . . 7
33 df-ral 2712 . . . . . . . . . 10
3433sbcbii 3218 . . . . . . . . 9
35 sbcal 3210 . . . . . . . . . 10
36 sbcimg 3204 . . . . . . . . . . . . 13
372, 36ax-mp 8 . . . . . . . . . . . 12
38 nfv 1630 . . . . . . . . . . . . . . 15
3938sbcgf 3226 . . . . . . . . . . . . . 14
402, 39ax-mp 8 . . . . . . . . . . . . 13
41 sbcimg 3204 . . . . . . . . . . . . . . 15
422, 41ax-mp 8 . . . . . . . . . . . . . 14
43 sbcbr2g 4266 . . . . . . . . . . . . . . . . 17
442, 43ax-mp 8 . . . . . . . . . . . . . . . 16
45 csbvarg 3280 . . . . . . . . . . . . . . . . . 18
462, 45ax-mp 8 . . . . . . . . . . . . . . . . 17
4746breq2i 4222 . . . . . . . . . . . . . . . 16
4844, 47bitri 242 . . . . . . . . . . . . . . 15
49 nfsbc1v 3182 . . . . . . . . . . . . . . . . 17
5049sbcgf 3226 . . . . . . . . . . . . . . . 16
512, 50ax-mp 8 . . . . . . . . . . . . . . 15
5248, 51imbi12i 318 . . . . . . . . . . . . . 14
5342, 52bitri 242 . . . . . . . . . . . . 13
5440, 53imbi12i 318 . . . . . . . . . . . 12
5537, 54bitri 242 . . . . . . . . . . 11
5655albii 1576 . . . . . . . . . 10
5735, 56bitri 242 . . . . . . . . 9
5834, 57bitri 242 . . . . . . . 8
59 bnj110.2 . . . . . . . . 9
6059sbcbii 3218 . . . . . . . 8
61 df-ral 2712 . . . . . . . 8
6258, 60, 613bitr4i 270 . . . . . . 7
6332, 62sylibr 205 . . . . . 6
6430, 63bnj31 29086 . . . . 5
65 nfv 1630 . . . . . . . 8
66 nfsbc1v 3182 . . . . . . . . 9
67 nfsbc1v 3182 . . . . . . . . 9
6866, 67nfim 1833 . . . . . . . 8
69 sbceq1a 3173 . . . . . . . . 9
70 sbceq1a 3173 . . . . . . . . 9
7169, 70imbi12d 313 . . . . . . . 8
7265, 68, 71cbvral 2930 . . . . . . 7
73 elrabi 3092 . . . . . . . . 9
7473imim1i 57 . . . . . . . 8
7574ralimi2 2780 . . . . . . 7
7672, 75sylbi 189 . . . . . 6
77 rexim 2812 . . . . . 6
7876, 77syl 16 . . . . 5
7964, 78mpan9 457 . . . 4
8079an32s 781 . . 3
8119, 80mto 170 . 2
82 iman 415 . 2
8381, 82mpbir 202 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 178   wa 360  wal 1550   wceq 1653   wcel 1726  cab 2424   wne 2601  wral 2707  wrex 2708  crab 2711  cvv 2958  wsbc 3163  csb 3253   wss 3322  c0 3630   class class class wbr 4214   wfr 4540 This theorem is referenced by:  bnj157  29232  bnj580  29286  bnj1052  29346  bnj1030  29358  bnj1133  29360 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-sep 4332 This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2712  df-rex 2713  df-rab 2716  df-v 2960  df-sbc 3164  df-csb 3254  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-sn 3822  df-pr 3823  df-op 3825  df-br 4215  df-fr 4543
 Copyright terms: Public domain W3C validator