Users' Mathboxes Mathbox for BJ < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >   Mathboxes  >  bj-findis Structured version   Unicode version

Theorem bj-findis 9409
Description: Principle of induction, using implicit substitutions (the biconditional versions of the hypotheses are implicit substitutions, and we have weakened them to implications). Constructive proof (from CZF). See bj-bdfindis 9381 for a bounded version not requiring ax-setind 4220. See finds 4266 for a proof in IZF. From this version, it is easy to prove of finds 4266, finds2 4267, finds1 4268. (Contributed by BJ, 22-Dec-2019.) (Proof modification is discouraged.)
Hypotheses
Ref Expression
bj-findis.nf0  F/
bj-findis.nf1  F/
bj-findis.nfsuc  F/
bj-findis.0  (/)
bj-findis.1
bj-findis.suc  suc
Assertion
Ref Expression
bj-findis  om  om
Distinct variable groups:   ,   ,
Allowed substitution hints:   ()   (,)   (,)   (,)

Proof of Theorem bj-findis
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 bj-nn0suc 9394 . . . . 5  om  (/)  om  suc
2 pm3.21 251 . . . . . . . 8  (/)  (/)
32ad2antrr 457 . . . . . . 7  om  om  (/)  (/)
4 pm2.04 76 . . . . . . . . . . 11  om  om
54ralimi2 2375 . . . . . . . . . 10  om  om
6 imim2 49 . . . . . . . . . . . 12
76ral2imi 2379 . . . . . . . . . . 11  om  om  om
87imp 115 . . . . . . . . . 10  om  om  om
95, 8sylan2 270 . . . . . . . . 9  om  om  om
10 r19.29 2444 . . . . . . . . . . 11  om  om  suc  om  suc
11 vex 2554 . . . . . . . . . . . . . . . 16 
_V
1211sucid 4120 . . . . . . . . . . . . . . 15 
suc
13 eleq2 2098 . . . . . . . . . . . . . . 15  suc  suc
1412, 13mpbiri 157 . . . . . . . . . . . . . 14  suc
15 ax-1 5 . . . . . . . . . . . . . . 15  suc  suc
16 pm2.27 35 . . . . . . . . . . . . . . 15
1715, 16anim12ii 325 . . . . . . . . . . . . . 14  suc 
suc
1814, 17mpdan 398 . . . . . . . . . . . . 13  suc  suc
1918impcom 116 . . . . . . . . . . . 12  suc  suc
2019reximi 2410 . . . . . . . . . . 11  om  suc  om  suc
2110, 20syl 14 . . . . . . . . . 10  om  om  suc  om  suc
2221ex 108 . . . . . . . . 9  om  om  suc  om  suc
239, 22syl 14 . . . . . . . 8  om  om  om  suc  om  suc
2423adantll 445 . . . . . . 7  om  om  om  suc  om  suc
253, 24orim12d 699 . . . . . 6  om  om  (/)  om  suc  (/)  om  suc
2625ex 108 . . . . 5  om  om  (/)  om  suc  (/)  om 
suc
271, 26syl7bi 154 . . . 4  om  om  om  (/)  om 
suc
2827alrimiv 1751 . . 3  om 
om  om  (/)  om  suc
29 nfv 1418 . . . . 5  F/  om
30 bj-findis.nf1 . . . . 5  F/
3129, 30nfim 1461 . . . 4  F/  om
32 nfv 1418 . . . . 5  F/  om
33 nfv 1418 . . . . . . 7  F/  (/)
34 bj-findis.nf0 . . . . . . 7  F/
3533, 34nfan 1454 . . . . . 6  F/  (/)
36 nfcv 2175 . . . . . . 7  F/_ om
37 nfv 1418 . . . . . . . 8  F/  suc
38 bj-findis.nfsuc . . . . . . . 8  F/
3937, 38nfan 1454 . . . . . . 7  F/  suc
4036, 39nfrexxy 2355 . . . . . 6  F/  om  suc
4135, 40nfor 1463 . . . . 5  F/  (/)  om 
suc
4232, 41nfim 1461 . . . 4  F/  om  (/)  om  suc
43 nfv 1418 . . . 4  F/  om
44 nfv 1418 . . . 4  F/  om
45 eleq1 2097 . . . . . 6  om 
om
4645biimprd 147 . . . . 5  om  om
47 bj-findis.1 . . . . 5
4846, 47imim12d 68 . . . 4  om  om
49 eleq1 2097 . . . . . 6  om 
om
5049biimpd 132 . . . . 5  om  om
51 eqtr 2054 . . . . . . . 8  (/)  (/)
52 bj-findis.0 . . . . . . . 8  (/)
5351, 52syl 14 . . . . . . 7  (/)
5453expimpd 345 . . . . . 6  (/)
55 eqtr 2054 . . . . . . . . 9  suc  suc
56 bj-findis.suc . . . . . . . . 9  suc
5755, 56syl 14 . . . . . . . 8  suc
5857expimpd 345 . . . . . . 7  suc
5958rexlimdvw 2430 . . . . . 6  om  suc
6054, 59jaod 636 . . . . 5  (/)  om 
suc
6150, 60imim12d 68 . . . 4  om  (/)  om  suc  om
6231, 42, 43, 44, 48, 61setindis 9397 . . 3 
om  om  (/)  om  suc  om
6328, 62syl 14 . 2  om  om
64 df-ral 2305 . 2  om  om
6563, 64sylibr 137 1  om  om
Colors of variables: wff set class
Syntax hints:   wi 4   wa 97   wo 628  wal 1240   wceq 1242   F/wnf 1346   wcel 1390  wral 2300  wrex 2301   (/)c0 3218   suc csuc 4068   omcom 4256
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-13 1401  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-nul 3874  ax-pr 3935  ax-un 4136  ax-setind 4220  ax-bd0 9248  ax-bdim 9249  ax-bdan 9250  ax-bdor 9251  ax-bdn 9252  ax-bdal 9253  ax-bdex 9254  ax-bdeq 9255  ax-bdel 9256  ax-bdsb 9257  ax-bdsep 9319  ax-infvn 9375
This theorem depends on definitions:  df-bi 110  df-tru 1245  df-fal 1248  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-rab 2309  df-v 2553  df-dif 2914  df-un 2916  df-in 2918  df-ss 2925  df-nul 3219  df-sn 3373  df-pr 3374  df-uni 3572  df-int 3607  df-suc 4074  df-iom 4257  df-bdc 9276  df-bj-ind 9362
This theorem is referenced by:  bj-findisg  9410  bj-findes  9411
  Copyright terms: Public domain W3C validator