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

Theorem bnj110 29741
 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 2834 . . . . 5
2 vex 3034 . . . . . . . 8
3 sbcng 3296 . . . . . . . 8
42, 3ax-mp 5 . . . . . . 7
54bicomi 207 . . . . . 6
65ralbii 2823 . . . . 5
71, 6bitr3i 259 . . . 4
8 df-rab 2765 . . . . . . 7
98eleq2i 2541 . . . . . 6
10 df-sbc 3256 . . . . . . 7
11 sbcan 3298 . . . . . . . 8
12 sbcel1v 3314 . . . . . . . . 9
1312anbi1i 709 . . . . . . . 8
1411, 13bitri 257 . . . . . . 7
1510, 14bitr3i 259 . . . . . 6
169, 15bitri 257 . . . . 5
1716simprbi 471 . . . 4
187, 17mprgbir 2771 . . 3
19 bnj110.1 . . . . . . . . 9
2019rabex 4550 . . . . . . . 8
2120biantrur 514 . . . . . . 7
22 rexnal 2836 . . . . . . . 8
23 rabn0 3755 . . . . . . . . 9
24 ssrab2 3500 . . . . . . . . . 10
2524biantrur 514 . . . . . . . . 9
2623, 25bitr3i 259 . . . . . . . 8
2722, 26bitr3i 259 . . . . . . 7
28 fri 4801 . . . . . . 7
2921, 27, 28syl2anb 487 . . . . . 6
30 eqid 2471 . . . . . . . 8
3130bnj23 29596 . . . . . . 7
32 df-ral 2761 . . . . . . . . . 10
3332sbcbii 3311 . . . . . . . . 9
34 sbcal 3305 . . . . . . . . . 10
35 sbcimg 3297 . . . . . . . . . . . . 13
362, 35ax-mp 5 . . . . . . . . . . . 12
37 nfv 1769 . . . . . . . . . . . . . . 15
3837sbcgf 3319 . . . . . . . . . . . . . 14
392, 38ax-mp 5 . . . . . . . . . . . . 13
40 sbcimg 3297 . . . . . . . . . . . . . . 15
412, 40ax-mp 5 . . . . . . . . . . . . . 14
42 sbcbr2g 4451 . . . . . . . . . . . . . . . . 17
432, 42ax-mp 5 . . . . . . . . . . . . . . . 16
44 csbvarg 3796 . . . . . . . . . . . . . . . . . 18
452, 44ax-mp 5 . . . . . . . . . . . . . . . . 17
4645breq2i 4403 . . . . . . . . . . . . . . . 16
4743, 46bitri 257 . . . . . . . . . . . . . . 15
48 nfsbc1v 3275 . . . . . . . . . . . . . . . . 17
4948sbcgf 3319 . . . . . . . . . . . . . . . 16
502, 49ax-mp 5 . . . . . . . . . . . . . . 15
5147, 50imbi12i 333 . . . . . . . . . . . . . 14
5241, 51bitri 257 . . . . . . . . . . . . 13
5339, 52imbi12i 333 . . . . . . . . . . . 12
5436, 53bitri 257 . . . . . . . . . . 11
5554albii 1699 . . . . . . . . . 10
5634, 55bitri 257 . . . . . . . . 9
5733, 56bitri 257 . . . . . . . 8
58 bnj110.2 . . . . . . . . 9
5958sbcbii 3311 . . . . . . . 8
60 df-ral 2761 . . . . . . . 8
6157, 59, 603bitr4i 285 . . . . . . 7
6231, 61sylibr 217 . . . . . 6
6329, 62bnj31 29597 . . . . 5
64 nfv 1769 . . . . . . . 8
65 nfsbc1v 3275 . . . . . . . . 9
66 nfsbc1v 3275 . . . . . . . . 9
6765, 66nfim 2023 . . . . . . . 8
68 sbceq1a 3266 . . . . . . . . 9
69 sbceq1a 3266 . . . . . . . . 9
7068, 69imbi12d 327 . . . . . . . 8
7164, 67, 70cbvral 3001 . . . . . . 7
72 elrabi 3181 . . . . . . . . 9
7372imim1i 59 . . . . . . . 8
7473ralimi2 2793 . . . . . . 7
7571, 74sylbi 200 . . . . . 6
76 rexim 2849 . . . . . 6
7775, 76syl 17 . . . . 5
7863, 77mpan9 477 . . . 4
7978an32s 821 . . 3
8018, 79mto 181 . 2
81 iman 431 . 2
8280, 81mpbir 214 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 189   wa 376  wal 1450   wceq 1452   wcel 1904  cab 2457   wne 2641  wral 2756  wrex 2757  crab 2760  cvv 3031  wsbc 3255  csb 3349   wss 3390  c0 3722   class class class wbr 4395   wfr 4795 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-sep 4518 This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3an 1009  df-tru 1455  df-fal 1458  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-ral 2761  df-rex 2762  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-nul 3723  df-if 3873  df-sn 3960  df-pr 3962  df-op 3966  df-br 4396  df-fr 4798 This theorem is referenced by:  bnj157  29742  bnj580  29796  bnj1052  29856  bnj1030  29868  bnj1133  29870
 Copyright terms: Public domain W3C validator