New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  findsd Unicode version

Theorem findsd 4410
 Description: Principle of finite induction over the finite cardinals, using implicit substitutions. The first hypothesis ensures stratification of , the next four set up the substitutions, and the last two set up the base case and induction hypothesis. This version allows for an extra deduction clause that may make proving stratification simpler. Compare Theorem X.1.13 of [Rosser] p. 277. (Contributed by SF, 31-Jul-2019.)
Hypotheses
Ref Expression
findsd.1
findsd.2 0c
findsd.3
findsd.4 1c
findsd.5
findsd.6
findsd.7 Nn
Assertion
Ref Expression
findsd Nn
Distinct variable groups:   ,   ,   ,   ,   ,   ,   ,   ,
Allowed substitution hints:   ()   ()   ()   ()   ()   ()   ()   (,)

Proof of Theorem findsd
StepHypRef Expression
1 findsd.1 . . . . 5
2 findsd.6 . . . . . 6
3 0cex 4392 . . . . . . 7 0c
4 findsd.2 . . . . . . 7 0c
53, 4elab 2985 . . . . . 6 0c
62, 5sylibr 203 . . . . 5 0c
7 findsd.7 . . . . . . . 8 Nn
8 vex 2862 . . . . . . . . 9
9 findsd.3 . . . . . . . . 9
108, 9elab 2985 . . . . . . . 8
11 1cex 4142 . . . . . . . . . 10 1c
128, 11addcex 4394 . . . . . . . . 9 1c
13 findsd.4 . . . . . . . . 9 1c
1412, 13elab 2985 . . . . . . . 8 1c
157, 10, 143imtr4g 261 . . . . . . 7 Nn 1c
1615ancoms 439 . . . . . 6 Nn 1c
1716ralrimiva 2697 . . . . 5 Nn 1c
18 peano5 4409 . . . . 5 0c Nn 1c Nn
191, 6, 17, 18syl3anc 1182 . . . 4 Nn
2019sseld 3272 . . 3 Nn
2120impcom 419 . 2 Nn
22 findsd.5 . . . 4
2322elabg 2986 . . 3 Nn