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 φ A V
tfisi.b φ T On
tfisi.c φ R On R T y S R χ ψ
tfisi.d x = y ψ χ
tfisi.e x = A ψ θ
tfisi.f x = y R = S
tfisi.g x = A R = T
Assertion tfisi φ θ

Proof

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