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 syl6bb ⊢ 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 ⊢ φ → θ