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

Theorem bnj1204 28310
 Description: Well-founded induction. 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.)
Hypothesis
Ref Expression
bnj1204.1
Assertion
Ref Expression
bnj1204
Distinct variable groups:   ,,   ,,   ,
Dummy variable is distinct from all other variables.
Allowed substitution hints:   ()   (,)

Proof of Theorem bnj1204
StepHypRef Expression
1 simp1 957 . . . . . 6
2 ssrab2 3260 . . . . . . 7
32a1i 12 . . . . . 6
4 simp3 959 . . . . . . 7
5 rabn0 3476 . . . . . . 7
64, 5sylibr 205 . . . . . 6
7 nfrab1 2722 . . . . . . . 8
87nfcrii 2414 . . . . . . 7
98bnj1228 28309 . . . . . 6
101, 3, 6, 9syl3anc 1184 . . . . 5
11 biid 229 . . . . 5
12 nfv 1606 . . . . . . 7
13 nfra1 2595 . . . . . . 7
14 nfre1 2601 . . . . . . 7
1512, 13, 14nf3an 1776 . . . . . 6
1615nfri 1744 . . . . 5
1710, 11, 16bnj1521 28151 . . . 4
18 eqid 2285 . . . . . 6
1918, 11bnj1212 28100 . . . . 5
20 nfra1 2595 . . . . . . . 8
21 simp3 959 . . . . . . . . . . . . . . 15
2221bnj1211 28098 . . . . . . . . . . . . . 14
23 con2b 326 . . . . . . . . . . . . . . 15
2423albii 1554 . . . . . . . . . . . . . 14
2522, 24sylib 190 . . . . . . . . . . . . 13
26 simp2 958 . . . . . . . . . . . . 13
27 sp 1717 . . . . . . . . . . . . 13
2825, 26, 27sylc 58 . . . . . . . . . . . 12
29 simp1 957 . . . . . . . . . . . 12
30 nfcv 2421 . . . . . . . . . . . . . . . . . . 19
3130elrabsf 3031 . . . . . . . . . . . . . . . . . 18
32 vex 2793 . . . . . . . . . . . . . . . . . . . 20
33 sbcng 3033 . . . . . . . . . . . . . . . . . . . 20
3432, 33ax-mp 10 . . . . . . . . . . . . . . . . . . 19
3534anbi2i 677 . . . . . . . . . . . . . . . . . 18
3631, 35bitri 242 . . . . . . . . . . . . . . . . 17
3736notbii 289 . . . . . . . . . . . . . . . 16
38 imnan 413 . . . . . . . . . . . . . . . 16
3937, 38bitr4i 245 . . . . . . . . . . . . . . 15
4039biimpi 188 . . . . . . . . . . . . . 14
4140imp 420 . . . . . . . . . . . . 13
42 notnot 284 . . . . . . . . . . . . 13
4341, 42sylibr 205 . . . . . . . . . . . 12
4428, 29, 43syl2anc 644 . . . . . . . . . . 11
45443expa 1153 . . . . . . . . . 10
4645expcom 426 . . . . . . . . 9
4746exp3a 427 . . . . . . . 8
4820, 47ralrimi 2626 . . . . . . 7
49 bnj1204.1 . . . . . . 7
5048, 49sylibr 205 . . . . . 6
51503ad2ant3 980 . . . . 5
52 simp12 988 . . . . 5
53 simp3 959 . . . . . . 7
5453bnj1211 28098 . . . . . 6
55 simp1 957 . . . . . 6
56 simp2 958 . . . . . 6
57 sp 1717 . . . . . 6
5854, 55, 56, 57syl3c 59 . . . . 5
5919, 51, 52, 58syl3anc 1184 . . . 4
60 rabid 2718 . . . . . 6
6160simprbi 452 . . . . 5
62613ad2ant2 979 . . . 4
6317, 59, 62bnj1304 28120 . . 3
6463bnj1224 28102 . 2
65 dfral2 2557 . 2
6664, 65sylibr 205 1
 Colors of variables: wff set class Syntax hints:   wn 5   wi 6   wb 178   wa 360   w3a 936  wal 1528   wcel 1685   wne 2448  wral 2545  wrex 2546  crab 2549  cvv 2790  wsbc 2993   wss 3154  c0 3457   class class class wbr 4025   w-bnj15 27985 This theorem is referenced by:  bnj1417  28339 This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-13 1687  ax-14 1689  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2266  ax-rep 4133  ax-sep 4143  ax-nul 4151  ax-pow 4188  ax-pr 4214  ax-un 4512  ax-reg 7302  ax-inf2 7338 This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 937  df-3an 938  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-eu 2149  df-mo 2150  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-ral 2550  df-rex 2551  df-reu 2552  df-rab 2554  df-v 2792  df-sbc 2994  df-csb 3084  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-pss 3170  df-nul 3458  df-if 3568  df-pw 3629  df-sn 3648  df-pr 3649  df-tp 3650  df-op 3651  df-uni 3830  df-iun 3909  df-br 4026  df-opab 4080  df-mpt 4081  df-tr 4116  df-eprel 4305  df-id 4309  df-po 4314  df-so 4315  df-fr 4352  df-we 4354  df-ord 4395  df-on 4396  df-lim 4397  df-suc 4398  df-om 4657  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-fun 5224  df-fn 5225  df-f 5226  df-f1 5227  df-fo 5228  df-f1o 5229  df-fv 5230  df-1o 6475  df-bnj17 27980  df-bnj14 27982  df-bnj13 27984  df-bnj15 27986  df-bnj18 27988  df-bnj19 27990
 Copyright terms: Public domain W3C validator