Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  tfindsg2 Structured version   Visualization version   Unicode version

Theorem tfindsg2 6707
 Description: Transfinite Induction (inference schema), using implicit substitutions. The first four hypotheses establish the substitutions we need. The last three are the basis, the induction step for successors, and the induction step for limit ordinals. The basis of this version is an arbitrary ordinal instead of zero. (Unnecessary distinct variable restrictions were removed by David Abernethy, 19-Jun-2012.) (Contributed by NM, 5-Jan-2005.)
Hypotheses
Ref Expression
tfindsg2.1
tfindsg2.2
tfindsg2.3
tfindsg2.4
tfindsg2.5
tfindsg2.6
tfindsg2.7
Assertion
Ref Expression
tfindsg2
Distinct variable groups:   ,   ,,   ,   ,   ,   ,
Allowed substitution hints:   ()   (,)   ()   ()   ()   ()

Proof of Theorem tfindsg2
StepHypRef Expression
1 onelon 5455 . . 3
2 sucelon 6663 . . 3
31, 2sylib 201 . 2
4 eloni 5440 . . . 4
5 ordsucss 6664 . . . 4
64, 5syl 17 . . 3
76imp 436 . 2
8 tfindsg2.1 . . . . 5
9 tfindsg2.2 . . . . 5
10 tfindsg2.3 . . . . 5
11 tfindsg2.4 . . . . 5
12 tfindsg2.5 . . . . . 6
132, 12sylbir 218 . . . . 5
14 eloni 5440 . . . . . . . . . 10
15 ordelsuc 6666 . . . . . . . . . 10
1614, 15sylan2 482 . . . . . . . . 9
1716ancoms 460 . . . . . . . 8
18 tfindsg2.6 . . . . . . . . . 10
1918ex 441 . . . . . . . . 9
2019adantr 472 . . . . . . . 8
2117, 20sylbird 243 . . . . . . 7
222, 21sylan2br 484 . . . . . 6
2322imp 436 . . . . 5
24 tfindsg2.7 . . . . . . . . . 10
2524ex 441 . . . . . . . . 9
2625adantr 472 . . . . . . . 8
27 vex 3034 . . . . . . . . . . 11
28 limelon 5493 . . . . . . . . . . 11
2927, 28mpan 684 . . . . . . . . . 10
30 eloni 5440 . . . . . . . . . . . 12
31 ordelsuc 6666 . . . . . . . . . . . 12
3230, 31sylan2 482 . . . . . . . . . . 11
33 onelon 5455 . . . . . . . . . . . . . . . . 17
3433, 14syl 17 . . . . . . . . . . . . . . . 16
3534, 15sylan2 482 . . . . . . . . . . . . . . 15
3635anassrs 660 . . . . . . . . . . . . . 14
3736imbi1d 324 . . . . . . . . . . . . 13
3837ralbidva 2828 . . . . . . . . . . . 12
3938imbi1d 324 . . . . . . . . . . 11
4032, 39imbi12d 327 . . . . . . . . . 10
4129, 40sylan2 482 . . . . . . . . 9
4241ancoms 460 . . . . . . . 8
4326, 42mpbid 215 . . . . . . 7
442, 43sylan2br 484 . . . . . 6
4544imp 436 . . . . 5
468, 9, 10, 11, 13, 23, 45tfindsg 6706 . . . 4
4746expl 630 . . 3