ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  tfisi Structured version   Unicode version

Theorem tfisi 4253
Description: A transfinite induction scheme in "implicit" form where the induction is done on an object derived from the object of interest. (Contributed by Stefan O'Rear, 24-Aug-2015.)
Hypotheses
Ref Expression
tfisi.a  V
tfisi.b  T  On
tfisi.c  R  On  R  C_  T  S  R
tfisi.d
tfisi.e
tfisi.f  R  S
tfisi.g  R  T
Assertion
Ref Expression
tfisi
Distinct variable groups:   ,, T   , R   , S   ,   ,,   ,   ,   ,
Allowed substitution hints:   ()   ()   ()   ()    R()    S()    V(,)

Proof of Theorem tfisi
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ssid 2958 . 2  T  C_  T
2 eqid 2037 . . . . 5  T  T
3 tfisi.a . . . . . 6  V
4 tfisi.b . . . . . . 7  T  On
5 eqeq2 2046 . . . . . . . . . . 11  R  R
6 sseq1 2960 . . . . . . . . . . . . 13  C_  T  C_  T
76anbi2d 437 . . . . . . . . . . . 12  C_  T  C_  T
87imbi1d 220 . . . . . . . . . . 11  C_  T  C_  T
95, 8imbi12d 223 . . . . . . . . . 10  R  C_  T  R  C_  T
109albidv 1702 . . . . . . . . 9  R  C_  T  R  C_  T
11 tfisi.f . . . . . . . . . . . 12  R  S
1211eqeq1d 2045 . . . . . . . . . . 11  R  S
13 tfisi.d . . . . . . . . . . . 12
1413imbi2d 219 . . . . . . . . . . 11  C_  T  C_  T
1512, 14imbi12d 223 . . . . . . . . . 10  R  C_  T  S  C_  T
1615cbvalv 1791 . . . . . . . . 9  R  C_  T  S  C_  T
1710, 16syl6bb 185 . . . . . . . 8  R  C_  T  S  C_  T
18 eqeq2 2046 . . . . . . . . . 10  T  R  R  T
19 sseq1 2960 . . . . . . . . . . . 12  T  C_  T  T  C_  T
2019anbi2d 437 . . . . . . . . . . 11  T  C_  T  T  C_  T
2120imbi1d 220 . . . . . . . . . 10  T  C_  T  T  C_  T
2218, 21imbi12d 223 . . . . . . . . 9  T  R  C_  T  R  T  T  C_  T
2322albidv 1702 . . . . . . . 8  T  R  C_  T  R  T  T  C_  T
24 simp3l 931 . . . . . . . . . . . 12  On  S  C_  T  R  C_  T
25 simp2 904 . . . . . . . . . . . . 13  On  S  C_  T  R  C_  T  R
26 simp1l 927 . . . . . . . . . . . . 13  On  S  C_  T  R  C_  T  On
2725, 26eqeltrd 2111 . . . . . . . . . . . 12  On  S  C_  T  R  C_  T  R  On
28 simp3r 932 . . . . . . . . . . . . 13  On  S  C_  T  R  C_  T  C_  T
2925, 28eqsstrd 2973 . . . . . . . . . . . 12  On  S  C_  T  R  C_  T  R  C_  T
30 simpl3l 958 . . . . . . . . . . . . . . . 16  On  S  C_  T  R  C_  T  [_  ]_ R  R
31 simpl1l 954 . . . . . . . . . . . . . . . . . 18  On  S  C_  T  R  C_  T  [_  ]_ R  R  On
32 simpr 103 . . . . . . . . . . . . . . . . . . 19  On  S  C_  T  R  C_  T  [_  ]_ R  R  [_  ]_ R  R
33 simpl2 907 . . . . . . . . . . . . . . . . . . 19  On  S  C_  T  R  C_  T  [_  ]_ R  R  R
3432, 33eleqtrd 2113 . . . . . . . . . . . . . . . . . 18  On  S  C_  T  R  C_  T  [_  ]_ R  R  [_  ]_ R
35 onelss 4090 . . . . . . . . . . . . . . . . . 18  On  [_  ]_ R  [_  ]_ R  C_
3631, 34, 35sylc 56 . . . . . . . . . . . . . . . . 17  On  S  C_  T  R  C_  T  [_  ]_ R  R  [_  ]_ R  C_
37 simpl3r 959 . . . . . . . . . . . . . . . . 17  On  S  C_  T  R  C_  T  [_  ]_ R  R  C_  T
3836, 37sstrd 2949 . . . . . . . . . . . . . . . 16  On  S  C_  T  R  C_  T  [_  ]_ R  R  [_  ]_ R  C_  T
39 simpl1r 955 . . . . . . . . . . . . . . . . . 18  On  S  C_  T  R  C_  T  [_  ]_ R  R  S  C_  T
40 eqeq2 2046 . . . . . . . . . . . . . . . . . . . . 21  [_  ]_ R  S  S 
[_  ]_ R
41 sseq1 2960 . . . . . . . . . . . . . . . . . . . . . . 23  [_  ]_ R  C_  T  [_  ]_ R  C_  T
4241anbi2d 437 . . . . . . . . . . . . . . . . . . . . . 22  [_  ]_ R  C_  T 
[_  ]_ R  C_  T
4342imbi1d 220 . . . . . . . . . . . . . . . . . . . . 21  [_  ]_ R  C_  T  [_  ]_ R  C_  T
4440, 43imbi12d 223 . . . . . . . . . . . . . . . . . . . 20  [_  ]_ R  S  C_  T  S  [_  ]_ R  [_  ]_ R  C_  T
4544albidv 1702 . . . . . . . . . . . . . . . . . . 19  [_  ]_ R  S  C_  T  S 
[_  ]_ R  [_  ]_ R  C_  T
4645rspcva 2648 . . . . . . . . . . . . . . . . . 18 
[_  ]_ R  S  C_  T  S 
[_  ]_ R  [_  ]_ R  C_  T
4734, 39, 46syl2anc 391 . . . . . . . . . . . . . . . . 17  On  S  C_  T  R  C_  T  [_  ]_ R  R  S  [_  ]_ R  [_  ]_ R  C_  T
48 eqidd 2038 . . . . . . . . . . . . . . . . 17  On  S  C_  T  R  C_  T  [_  ]_ R  R  [_  ]_ R  [_  ]_ R
49 nfcv 2175 . . . . . . . . . . . . . . . . . . . . . . 23  F/_
50 nfcv 2175 . . . . . . . . . . . . . . . . . . . . . . 23  F/_ S
5149, 50, 11csbhypf 2879 . . . . . . . . . . . . . . . . . . . . . 22  [_  ]_ R  S
5251eqcomd 2042 . . . . . . . . . . . . . . . . . . . . 21  S  [_  ]_ R
5352equcoms 1591 . . . . . . . . . . . . . . . . . . . 20  S  [_  ]_ R
5453eqeq1d 2045 . . . . . . . . . . . . . . . . . . 19  S  [_  ]_ R  [_  ]_ R 
[_  ]_ R
55 nfv 1418 . . . . . . . . . . . . . . . . . . . . . . 23  F/
5655, 13sbhypf 2597 . . . . . . . . . . . . . . . . . . . . . 22
5756bicomd 129 . . . . . . . . . . . . . . . . . . . . 21
5857equcoms 1591 . . . . . . . . . . . . . . . . . . . 20
5958imbi2d 219 . . . . . . . . . . . . . . . . . . 19  [_  ]_ R  C_  T  [_  ]_ R  C_  T
6054, 59imbi12d 223 . . . . . . . . . . . . . . . . . 18  S  [_  ]_ R  [_  ]_ R  C_  T  [_  ]_ R  [_  ]_ R  [_  ]_ R  C_  T
6160spv 1737 . . . . . . . . . . . . . . . . 17  S  [_  ]_ R  [_  ]_ R  C_  T  [_  ]_ R  [_  ]_ R  [_  ]_ R  C_  T
6247, 48, 61sylc 56 . . . . . . . . . . . . . . . 16  On  S  C_  T  R  C_  T  [_  ]_ R  R  [_  ]_ R  C_  T
6330, 38, 62mp2and 409 . . . . . . . . . . . . . . 15  On  S  C_  T  R  C_  T  [_  ]_ R  R
6463ex 108 . . . . . . . . . . . . . 14  On  S  C_  T  R  C_  T  [_  ]_ R  R
6564alrimiv 1751 . . . . . . . . . . . . 13  On  S  C_  T  R  C_  T 
[_  ]_ R  R
6651eleq1d 2103 . . . . . . . . . . . . . . 15  [_  ]_ R  R  S  R
6766, 56imbi12d 223 . . . . . . . . . . . . . 14  [_  ]_ R  R  S  R
6867cbvalv 1791 . . . . . . . . . . . . 13  [_  ]_ R  R  S  R
6965, 68sylib 127 . . . . . . . . . . . 12  On  S  C_  T  R  C_  T  S  R
70 tfisi.c . . . . . . . . . . . 12  R  On  R  C_  T  S  R
7124, 27, 29, 69, 70syl121anc 1139 . . . . . . . . . . 11  On  S  C_  T  R  C_  T
72713exp 1102 . . . . . . . . . 10  On  S  C_  T  R  C_  T
7372alrimiv 1751 . . . . . . . . 9  On  S  C_  T  R  C_  T
7473ex 108 . . . . . . . 8  On  S  C_  T  R  C_  T
7517, 23, 74tfis3 4252 . . . . . . 7  T  On  R  T  T  C_  T
764, 75syl 14 . . . . . 6  R  T  T  C_  T
77 tfisi.g . . . . . . . . 9  R  T
7877eqeq1d 2045 . . . . . . . 8  R  T  T  T
79 tfisi.e . . . . . . . . 9
8079imbi2d 219 . . . . . . . 8  T  C_  T  T  C_  T
8178, 80imbi12d 223 . . . . . . 7  R  T  T  C_  T  T  T  T  C_  T
8281spcgv 2634 . . . . . 6  V  R  T  T  C_  T  T  T  T  C_  T
833, 76, 82sylc 56 . . . . 5  T  T  T  C_  T
842, 83mpi 15 . . . 4  T  C_  T
8584expd 245 . . 3  T  C_  T
8685pm2.43i 43 . 2  T  C_  T
871, 86mpi 15 1
Colors of variables: wff set class
Syntax hints:   wi 4   wa 97   wb 98   w3a 884  wal 1240   wceq 1242   wcel 1390  wsb 1642  wral 2300   [_csb 2846    C_ wss 2911   Oncon0 4066
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-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-bndl 1396  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-setind 4220
This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  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-sbc 2759  df-csb 2847  df-in 2918  df-ss 2925  df-uni 3572  df-tr 3846  df-iord 4069  df-on 4071
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator