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∧∀yS∈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∧∀yS∈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→∀xR=z→φ∧z⊆T→ψ↔∀xR=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 ⊢∀xR=w→φ∧w⊆T→ψ↔∀yS=w→φ∧w⊆T→χ
20 15 19 bitrdi ⊢z=w→∀xR=z→φ∧z⊆T→ψ↔∀yS=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→∀xR=z→φ∧z⊆T→ψ↔∀xR=T→φ∧T⊆T→ψ
27 simp3l ⊢z∈On∧∀w∈z∀yS=w→φ∧w⊆T→χ∧R=z∧φ∧z⊆T→φ
28 simp2 ⊢z∈On∧∀w∈z∀yS=w→φ∧w⊆T→χ∧R=z∧φ∧z⊆T→R=z
29 simp1l ⊢z∈On∧∀w∈z∀yS=w→φ∧w⊆T→χ∧R=z∧φ∧z⊆T→z∈On
30 28 29 eqeltrd ⊢z∈On∧∀w∈z∀yS=w→φ∧w⊆T→χ∧R=z∧φ∧z⊆T→R∈On
31 simp3r ⊢z∈On∧∀w∈z∀yS=w→φ∧w⊆T→χ∧R=z∧φ∧z⊆T→z⊆T
32 28 31 eqsstrd ⊢z∈On∧∀w∈z∀yS=w→φ∧w⊆T→χ∧R=z∧φ∧z⊆T→R⊆T
33 simpl3l ⊢z∈On∧∀w∈z∀yS=w→φ∧w⊆T→χ∧R=z∧φ∧z⊆T∧⦋v/x⦌R∈R→φ
34 simpl1l ⊢z∈On∧∀w∈z∀yS=w→φ∧w⊆T→χ∧R=z∧φ∧z⊆T∧⦋v/x⦌R∈R→z∈On
35 simpr ⊢z∈On∧∀w∈z∀yS=w→φ∧w⊆T→χ∧R=z∧φ∧z⊆T∧⦋v/x⦌R∈R→⦋v/x⦌R∈R
36 simpl2 ⊢z∈On∧∀w∈z∀yS=w→φ∧w⊆T→χ∧R=z∧φ∧z⊆T∧⦋v/x⦌R∈R→R=z
37 35 36 eleqtrd ⊢z∈On∧∀w∈z∀yS=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∀yS=w→φ∧w⊆T→χ∧R=z∧φ∧z⊆T∧⦋v/x⦌R∈R→⦋v/x⦌R⊆z
40 simpl3r ⊢z∈On∧∀w∈z∀yS=w→φ∧w⊆T→χ∧R=z∧φ∧z⊆T∧⦋v/x⦌R∈R→z⊆T
41 39 40 sstrd ⊢z∈On∧∀w∈z∀yS=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→∀yS=w→φ∧w⊆T→χ↔∀yS=⦋v/x⦌R→φ∧⦋v/x⦌R⊆T→χ
48 simpl1r ⊢z∈On∧∀w∈z∀yS=w→φ∧w⊆T→χ∧R=z∧φ∧z⊆T∧⦋v/x⦌R∈R→∀w∈z∀yS=w→φ∧w⊆T→χ
49 47 48 37 rspcdva ⊢z∈On∧∀w∈z∀yS=w→φ∧w⊆T→χ∧R=z∧φ∧z⊆T∧⦋v/x⦌R∈R→∀yS=⦋v/x⦌R→φ∧⦋v/x⦌R⊆T→χ
50 eqidd ⊢z∈On∧∀w∈z∀yS=w→φ∧w⊆T→χ∧R=z∧φ∧z⊆T∧⦋v/x⦌R∈R→⦋v/x⦌R=⦋v/x⦌R
51 nfcv ⊢Ⅎ_xy
52 nfcv ⊢Ⅎ_xS
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→vxψ↔χ
59 58 bicomd ⊢v=y→χ↔vxψ
60 59 equcoms ⊢y=v→χ↔vxψ
61 60 imbi2d ⊢y=v→φ∧⦋v/x⦌R⊆T→χ↔φ∧⦋v/x⦌R⊆T→vxψ
62 56 61 imbi12d ⊢y=v→S=⦋v/x⦌R→φ∧⦋v/x⦌R⊆T→χ↔⦋v/x⦌R=⦋v/x⦌R→φ∧⦋v/x⦌R⊆T→vxψ
63 62 spvv ⊢∀yS=⦋v/x⦌R→φ∧⦋v/x⦌R⊆T→χ→⦋v/x⦌R=⦋v/x⦌R→φ∧⦋v/x⦌R⊆T→vxψ
64 49 50 63 sylc ⊢z∈On∧∀w∈z∀yS=w→φ∧w⊆T→χ∧R=z∧φ∧z⊆T∧⦋v/x⦌R∈R→φ∧⦋v/x⦌R⊆T→vxψ
65 33 41 64 mp2and ⊢z∈On∧∀w∈z∀yS=w→φ∧w⊆T→χ∧R=z∧φ∧z⊆T∧⦋v/x⦌R∈R→vxψ
66 65 ex ⊢z∈On∧∀w∈z∀yS=w→φ∧w⊆T→χ∧R=z∧φ∧z⊆T→⦋v/x⦌R∈R→vxψ
67 66 alrimiv ⊢z∈On∧∀w∈z∀yS=w→φ∧w⊆T→χ∧R=z∧φ∧z⊆T→∀v⦋v/x⦌R∈R→vxψ
68 53 eleq1d ⊢v=y→⦋v/x⦌R∈R↔S∈R
69 68 58 imbi12d ⊢v=y→⦋v/x⦌R∈R→vxψ↔S∈R→χ
70 69 cbvalvw ⊢∀v⦋v/x⦌R∈R→vxψ↔∀yS∈R→χ
71 67 70 sylib ⊢z∈On∧∀w∈z∀yS=w→φ∧w⊆T→χ∧R=z∧φ∧z⊆T→∀yS∈R→χ
72 27 30 32 71 3 syl121anc ⊢z∈On∧∀w∈z∀yS=w→φ∧w⊆T→χ∧R=z∧φ∧z⊆T→ψ
73 72 3exp ⊢z∈On∧∀w∈z∀yS=w→φ∧w⊆T→χ→R=z→φ∧z⊆T→ψ
74 73 alrimiv ⊢z∈On∧∀w∈z∀yS=w→φ∧w⊆T→χ→∀xR=z→φ∧z⊆T→ψ
75 74 ex ⊢z∈On→∀w∈z∀yS=w→φ∧w⊆T→χ→∀xR=z→φ∧z⊆T→ψ
76 20 26 75 tfis3 ⊢T∈On→∀xR=T→φ∧T⊆T→ψ
77 2 76 syl ⊢φ→∀xR=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→∀xR=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 ⊢φ→θ