Metamath Proof Explorer

Theorem tfisi

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)

Ref Expression
Hypotheses tfisi.a 
|- ( ph -> A e. V )
tfisi.b 
|- ( ph -> T e. On )
tfisi.c 
|- ( ( ph /\ ( R e. On /\ R C_ T ) /\ A. y ( S e. R -> ch ) ) -> ps )
tfisi.d 
|- ( x = y -> ( ps <-> ch ) )
tfisi.e 
|- ( x = A -> ( ps <-> th ) )
tfisi.f 
|- ( x = y -> R = S )
tfisi.g 
|- ( x = A -> R = T )
Assertion tfisi 
|- ( ph -> th )

Proof

Step Hyp Ref Expression
1 tfisi.a 
 |-  ( ph -> A e. V )
2 tfisi.b 
 |-  ( ph -> T e. On )
3 tfisi.c 
 |-  ( ( ph /\ ( R e. On /\ R C_ T ) /\ A. y ( S e. R -> ch ) ) -> ps )
4 tfisi.d 
 |-  ( x = y -> ( ps <-> ch ) )
5 tfisi.e 
 |-  ( x = A -> ( ps <-> th ) )
6 tfisi.f 
 |-  ( x = y -> R = S )
7 tfisi.g 
 |-  ( x = A -> R = T )
8 ssid 
 |-  T C_ T
9 eqid 
 |-  T = T
10 eqeq2 
 |-  ( z = w -> ( R = z <-> R = w ) )
11 sseq1 
 |-  ( z = w -> ( z C_ T <-> w C_ T ) )
12 11 anbi2d 
 |-  ( z = w -> ( ( ph /\ z C_ T ) <-> ( ph /\ w C_ T ) ) )
13 12 imbi1d 
 |-  ( z = w -> ( ( ( ph /\ z C_ T ) -> ps ) <-> ( ( ph /\ w C_ T ) -> ps ) ) )
14 10 13 imbi12d 
 |-  ( z = w -> ( ( R = z -> ( ( ph /\ z C_ T ) -> ps ) ) <-> ( R = w -> ( ( ph /\ w C_ T ) -> ps ) ) ) )
15 14 albidv 
 |-  ( z = w -> ( A. x ( R = z -> ( ( ph /\ z C_ T ) -> ps ) ) <-> A. x ( R = w -> ( ( ph /\ w C_ T ) -> ps ) ) ) )
16 6 eqeq1d 
 |-  ( x = y -> ( R = w <-> S = w ) )
17 4 imbi2d 
 |-  ( x = y -> ( ( ( ph /\ w C_ T ) -> ps ) <-> ( ( ph /\ w C_ T ) -> ch ) ) )
18 16 17 imbi12d 
 |-  ( x = y -> ( ( R = w -> ( ( ph /\ w C_ T ) -> ps ) ) <-> ( S = w -> ( ( ph /\ w C_ T ) -> ch ) ) ) )
19 18 cbvalvw 
 |-  ( A. x ( R = w -> ( ( ph /\ w C_ T ) -> ps ) ) <-> A. y ( S = w -> ( ( ph /\ w C_ T ) -> ch ) ) )
20 15 19 bitrdi 
 |-  ( z = w -> ( A. x ( R = z -> ( ( ph /\ z C_ T ) -> ps ) ) <-> A. y ( S = w -> ( ( ph /\ w C_ T ) -> ch ) ) ) )
21 eqeq2 
 |-  ( z = T -> ( R = z <-> R = T ) )
22 sseq1 
 |-  ( z = T -> ( z C_ T <-> T C_ T ) )
23 22 anbi2d 
 |-  ( z = T -> ( ( ph /\ z C_ T ) <-> ( ph /\ T C_ T ) ) )
24 23 imbi1d 
 |-  ( z = T -> ( ( ( ph /\ z C_ T ) -> ps ) <-> ( ( ph /\ T C_ T ) -> ps ) ) )
25 21 24 imbi12d 
 |-  ( z = T -> ( ( R = z -> ( ( ph /\ z C_ T ) -> ps ) ) <-> ( R = T -> ( ( ph /\ T C_ T ) -> ps ) ) ) )
26 25 albidv 
 |-  ( z = T -> ( A. x ( R = z -> ( ( ph /\ z C_ T ) -> ps ) ) <-> A. x ( R = T -> ( ( ph /\ T C_ T ) -> ps ) ) ) )
27 simp3l 
 |-  ( ( ( z e. On /\ A. w e. z A. y ( S = w -> ( ( ph /\ w C_ T ) -> ch ) ) ) /\ R = z /\ ( ph /\ z C_ T ) ) -> ph )
28 simp2 
 |-  ( ( ( z e. On /\ A. w e. z A. y ( S = w -> ( ( ph /\ w C_ T ) -> ch ) ) ) /\ R = z /\ ( ph /\ z C_ T ) ) -> R = z )
29 simp1l 
 |-  ( ( ( z e. On /\ A. w e. z A. y ( S = w -> ( ( ph /\ w C_ T ) -> ch ) ) ) /\ R = z /\ ( ph /\ z C_ T ) ) -> z e. On )
30 28 29 eqeltrd 
 |-  ( ( ( z e. On /\ A. w e. z A. y ( S = w -> ( ( ph /\ w C_ T ) -> ch ) ) ) /\ R = z /\ ( ph /\ z C_ T ) ) -> R e. On )
31 simp3r 
 |-  ( ( ( z e. On /\ A. w e. z A. y ( S = w -> ( ( ph /\ w C_ T ) -> ch ) ) ) /\ R = z /\ ( ph /\ z C_ T ) ) -> z C_ T )
32 28 31 eqsstrd 
 |-  ( ( ( z e. On /\ A. w e. z A. y ( S = w -> ( ( ph /\ w C_ T ) -> ch ) ) ) /\ R = z /\ ( ph /\ z C_ T ) ) -> R C_ T )
33 simpl3l 
 |-  ( ( ( ( z e. On /\ A. w e. z A. y ( S = w -> ( ( ph /\ w C_ T ) -> ch ) ) ) /\ R = z /\ ( ph /\ z C_ T ) ) /\ [_ v / x ]_ R e. R ) -> ph )
34 simpl1l 
 |-  ( ( ( ( z e. On /\ A. w e. z A. y ( S = w -> ( ( ph /\ w C_ T ) -> ch ) ) ) /\ R = z /\ ( ph /\ z C_ T ) ) /\ [_ v / x ]_ R e. R ) -> z e. On )
35 simpr 
 |-  ( ( ( ( z e. On /\ A. w e. z A. y ( S = w -> ( ( ph /\ w C_ T ) -> ch ) ) ) /\ R = z /\ ( ph /\ z C_ T ) ) /\ [_ v / x ]_ R e. R ) -> [_ v / x ]_ R e. R )
36 simpl2 
 |-  ( ( ( ( z e. On /\ A. w e. z A. y ( S = w -> ( ( ph /\ w C_ T ) -> ch ) ) ) /\ R = z /\ ( ph /\ z C_ T ) ) /\ [_ v / x ]_ R e. R ) -> R = z )
37 35 36 eleqtrd 
 |-  ( ( ( ( z e. On /\ A. w e. z A. y ( S = w -> ( ( ph /\ w C_ T ) -> ch ) ) ) /\ R = z /\ ( ph /\ z C_ T ) ) /\ [_ v / x ]_ R e. R ) -> [_ v / x ]_ R e. z )
38 onelss 
 |-  ( z e. On -> ( [_ v / x ]_ R e. z -> [_ v / x ]_ R C_ z ) )
39 34 37 38 sylc 
 |-  ( ( ( ( z e. On /\ A. w e. z A. y ( S = w -> ( ( ph /\ w C_ T ) -> ch ) ) ) /\ R = z /\ ( ph /\ z C_ T ) ) /\ [_ v / x ]_ R e. R ) -> [_ v / x ]_ R C_ z )
40 simpl3r 
 |-  ( ( ( ( z e. On /\ A. w e. z A. y ( S = w -> ( ( ph /\ w C_ T ) -> ch ) ) ) /\ R = z /\ ( ph /\ z C_ T ) ) /\ [_ v / x ]_ R e. R ) -> z C_ T )
41 39 40 sstrd 
 |-  ( ( ( ( z e. On /\ A. w e. z A. y ( S = w -> ( ( ph /\ w C_ T ) -> ch ) ) ) /\ R = z /\ ( ph /\ z C_ T ) ) /\ [_ v / x ]_ R e. R ) -> [_ v / x ]_ R C_ T )
42 eqeq2 
 |-  ( w = [_ v / x ]_ R -> ( S = w <-> S = [_ v / x ]_ R ) )
43 sseq1 
 |-  ( w = [_ v / x ]_ R -> ( w C_ T <-> [_ v / x ]_ R C_ T ) )
44 43 anbi2d 
 |-  ( w = [_ v / x ]_ R -> ( ( ph /\ w C_ T ) <-> ( ph /\ [_ v / x ]_ R C_ T ) ) )
45 44 imbi1d 
 |-  ( w = [_ v / x ]_ R -> ( ( ( ph /\ w C_ T ) -> ch ) <-> ( ( ph /\ [_ v / x ]_ R C_ T ) -> ch ) ) )
46 42 45 imbi12d 
 |-  ( w = [_ v / x ]_ R -> ( ( S = w -> ( ( ph /\ w C_ T ) -> ch ) ) <-> ( S = [_ v / x ]_ R -> ( ( ph /\ [_ v / x ]_ R C_ T ) -> ch ) ) ) )
47 46 albidv 
 |-  ( w = [_ v / x ]_ R -> ( A. y ( S = w -> ( ( ph /\ w C_ T ) -> ch ) ) <-> A. y ( S = [_ v / x ]_ R -> ( ( ph /\ [_ v / x ]_ R C_ T ) -> ch ) ) ) )
48 simpl1r 
 |-  ( ( ( ( z e. On /\ A. w e. z A. y ( S = w -> ( ( ph /\ w C_ T ) -> ch ) ) ) /\ R = z /\ ( ph /\ z C_ T ) ) /\ [_ v / x ]_ R e. R ) -> A. w e. z A. y ( S = w -> ( ( ph /\ w C_ T ) -> ch ) ) )
49 47 48 37 rspcdva 
 |-  ( ( ( ( z e. On /\ A. w e. z A. y ( S = w -> ( ( ph /\ w C_ T ) -> ch ) ) ) /\ R = z /\ ( ph /\ z C_ T ) ) /\ [_ v / x ]_ R e. R ) -> A. y ( S = [_ v / x ]_ R -> ( ( ph /\ [_ v / x ]_ R C_ T ) -> ch ) ) )
50 eqidd 
 |-  ( ( ( ( z e. On /\ A. w e. z A. y ( S = w -> ( ( ph /\ w C_ T ) -> ch ) ) ) /\ R = z /\ ( ph /\ z C_ T ) ) /\ [_ v / x ]_ R e. R ) -> [_ v / x ]_ R = [_ v / x ]_ R )
51 nfcv 
 |-  F/_ x y
52 nfcv 
 |-  F/_ x S
53 51 52 6 csbhypf 
 |-  ( v = y -> [_ v / x ]_ R = S )
54 53 eqcomd 
 |-  ( v = y -> S = [_ v / x ]_ R )
55 54 equcoms 
 |-  ( y = v -> S = [_ v / x ]_ R )
56 55 eqeq1d 
 |-  ( y = v -> ( S = [_ v / x ]_ R <-> [_ v / x ]_ R = [_ v / x ]_ R ) )
57 nfv 
 |-  F/ x ch
58 57 4 sbhypf 
 |-  ( v = y -> ( [ v / x ] ps <-> ch ) )
59 58 bicomd 
 |-  ( v = y -> ( ch <-> [ v / x ] ps ) )
60 59 equcoms 
 |-  ( y = v -> ( ch <-> [ v / x ] ps ) )
61 60 imbi2d 
 |-  ( y = v -> ( ( ( ph /\ [_ v / x ]_ R C_ T ) -> ch ) <-> ( ( ph /\ [_ v / x ]_ R C_ T ) -> [ v / x ] ps ) ) )
62 56 61 imbi12d 
 |-  ( y = v -> ( ( S = [_ v / x ]_ R -> ( ( ph /\ [_ v / x ]_ R C_ T ) -> ch ) ) <-> ( [_ v / x ]_ R = [_ v / x ]_ R -> ( ( ph /\ [_ v / x ]_ R C_ T ) -> [ v / x ] ps ) ) ) )
63 62 spvv 
 |-  ( A. y ( S = [_ v / x ]_ R -> ( ( ph /\ [_ v / x ]_ R C_ T ) -> ch ) ) -> ( [_ v / x ]_ R = [_ v / x ]_ R -> ( ( ph /\ [_ v / x ]_ R C_ T ) -> [ v / x ] ps ) ) )
64 49 50 63 sylc 
 |-  ( ( ( ( z e. On /\ A. w e. z A. y ( S = w -> ( ( ph /\ w C_ T ) -> ch ) ) ) /\ R = z /\ ( ph /\ z C_ T ) ) /\ [_ v / x ]_ R e. R ) -> ( ( ph /\ [_ v / x ]_ R C_ T ) -> [ v / x ] ps ) )
65 33 41 64 mp2and 
 |-  ( ( ( ( z e. On /\ A. w e. z A. y ( S = w -> ( ( ph /\ w C_ T ) -> ch ) ) ) /\ R = z /\ ( ph /\ z C_ T ) ) /\ [_ v / x ]_ R e. R ) -> [ v / x ] ps )
66 65 ex 
 |-  ( ( ( z e. On /\ A. w e. z A. y ( S = w -> ( ( ph /\ w C_ T ) -> ch ) ) ) /\ R = z /\ ( ph /\ z C_ T ) ) -> ( [_ v / x ]_ R e. R -> [ v / x ] ps ) )
67 66 alrimiv 
 |-  ( ( ( z e. On /\ A. w e. z A. y ( S = w -> ( ( ph /\ w C_ T ) -> ch ) ) ) /\ R = z /\ ( ph /\ z C_ T ) ) -> A. v ( [_ v / x ]_ R e. R -> [ v / x ] ps ) )
68 53 eleq1d 
 |-  ( v = y -> ( [_ v / x ]_ R e. R <-> S e. R ) )
69 68 58 imbi12d 
 |-  ( v = y -> ( ( [_ v / x ]_ R e. R -> [ v / x ] ps ) <-> ( S e. R -> ch ) ) )
70 69 cbvalvw 
 |-  ( A. v ( [_ v / x ]_ R e. R -> [ v / x ] ps ) <-> A. y ( S e. R -> ch ) )
71 67 70 sylib 
 |-  ( ( ( z e. On /\ A. w e. z A. y ( S = w -> ( ( ph /\ w C_ T ) -> ch ) ) ) /\ R = z /\ ( ph /\ z C_ T ) ) -> A. y ( S e. R -> ch ) )
72 27 30 32 71 3 syl121anc 
 |-  ( ( ( z e. On /\ A. w e. z A. y ( S = w -> ( ( ph /\ w C_ T ) -> ch ) ) ) /\ R = z /\ ( ph /\ z C_ T ) ) -> ps )
73 72 3exp 
 |-  ( ( z e. On /\ A. w e. z A. y ( S = w -> ( ( ph /\ w C_ T ) -> ch ) ) ) -> ( R = z -> ( ( ph /\ z C_ T ) -> ps ) ) )
74 73 alrimiv 
 |-  ( ( z e. On /\ A. w e. z A. y ( S = w -> ( ( ph /\ w C_ T ) -> ch ) ) ) -> A. x ( R = z -> ( ( ph /\ z C_ T ) -> ps ) ) )
75 74 ex 
 |-  ( z e. On -> ( A. w e. z A. y ( S = w -> ( ( ph /\ w C_ T ) -> ch ) ) -> A. x ( R = z -> ( ( ph /\ z C_ T ) -> ps ) ) ) )
76 20 26 75 tfis3 
 |-  ( T e. On -> A. x ( R = T -> ( ( ph /\ T C_ T ) -> ps ) ) )
77 2 76 syl 
 |-  ( ph -> A. x ( R = T -> ( ( ph /\ T C_ T ) -> ps ) ) )
78 7 eqeq1d 
 |-  ( x = A -> ( R = T <-> T = T ) )
79 5 imbi2d 
 |-  ( x = A -> ( ( ( ph /\ T C_ T ) -> ps ) <-> ( ( ph /\ T C_ T ) -> th ) ) )
80 78 79 imbi12d 
 |-  ( x = A -> ( ( R = T -> ( ( ph /\ T C_ T ) -> ps ) ) <-> ( T = T -> ( ( ph /\ T C_ T ) -> th ) ) ) )
81 80 spcgv 
 |-  ( A e. V -> ( A. x ( R = T -> ( ( ph /\ T C_ T ) -> ps ) ) -> ( T = T -> ( ( ph /\ T C_ T ) -> th ) ) ) )
82 1 77 81 sylc 
 |-  ( ph -> ( T = T -> ( ( ph /\ T C_ T ) -> th ) ) )
83 9 82 mpi 
 |-  ( ph -> ( ( ph /\ T C_ T ) -> th ) )
84 83 expd 
 |-  ( ph -> ( ph -> ( T C_ T -> th ) ) )
85 84 pm2.43i 
 |-  ( ph -> ( T C_ T -> th ) )
86 8 85 mpi 
 |-  ( ph -> th )