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 ( 𝜑𝐴𝑉 )
tfisi.b ( 𝜑𝑇 ∈ On )
tfisi.c ( ( 𝜑 ∧ ( 𝑅 ∈ On ∧ 𝑅𝑇 ) ∧ ∀ 𝑦 ( 𝑆𝑅𝜒 ) ) → 𝜓 )
tfisi.d ( 𝑥 = 𝑦 → ( 𝜓𝜒 ) )
tfisi.e ( 𝑥 = 𝐴 → ( 𝜓𝜃 ) )
tfisi.f ( 𝑥 = 𝑦𝑅 = 𝑆 )
tfisi.g ( 𝑥 = 𝐴𝑅 = 𝑇 )
Assertion tfisi ( 𝜑𝜃 )

Proof

Step Hyp Ref Expression
1 tfisi.a ( 𝜑𝐴𝑉 )
2 tfisi.b ( 𝜑𝑇 ∈ On )
3 tfisi.c ( ( 𝜑 ∧ ( 𝑅 ∈ On ∧ 𝑅𝑇 ) ∧ ∀ 𝑦 ( 𝑆𝑅𝜒 ) ) → 𝜓 )
4 tfisi.d ( 𝑥 = 𝑦 → ( 𝜓𝜒 ) )
5 tfisi.e ( 𝑥 = 𝐴 → ( 𝜓𝜃 ) )
6 tfisi.f ( 𝑥 = 𝑦𝑅 = 𝑆 )
7 tfisi.g ( 𝑥 = 𝐴𝑅 = 𝑇 )
8 ssid 𝑇𝑇
9 eqid 𝑇 = 𝑇
10 eqeq2 ( 𝑧 = 𝑤 → ( 𝑅 = 𝑧𝑅 = 𝑤 ) )
11 sseq1 ( 𝑧 = 𝑤 → ( 𝑧𝑇𝑤𝑇 ) )
12 11 anbi2d ( 𝑧 = 𝑤 → ( ( 𝜑𝑧𝑇 ) ↔ ( 𝜑𝑤𝑇 ) ) )
13 12 imbi1d ( 𝑧 = 𝑤 → ( ( ( 𝜑𝑧𝑇 ) → 𝜓 ) ↔ ( ( 𝜑𝑤𝑇 ) → 𝜓 ) ) )
14 10 13 imbi12d ( 𝑧 = 𝑤 → ( ( 𝑅 = 𝑧 → ( ( 𝜑𝑧𝑇 ) → 𝜓 ) ) ↔ ( 𝑅 = 𝑤 → ( ( 𝜑𝑤𝑇 ) → 𝜓 ) ) ) )
15 14 albidv ( 𝑧 = 𝑤 → ( ∀ 𝑥 ( 𝑅 = 𝑧 → ( ( 𝜑𝑧𝑇 ) → 𝜓 ) ) ↔ ∀ 𝑥 ( 𝑅 = 𝑤 → ( ( 𝜑𝑤𝑇 ) → 𝜓 ) ) ) )
16 6 eqeq1d ( 𝑥 = 𝑦 → ( 𝑅 = 𝑤𝑆 = 𝑤 ) )
17 4 imbi2d ( 𝑥 = 𝑦 → ( ( ( 𝜑𝑤𝑇 ) → 𝜓 ) ↔ ( ( 𝜑𝑤𝑇 ) → 𝜒 ) ) )
18 16 17 imbi12d ( 𝑥 = 𝑦 → ( ( 𝑅 = 𝑤 → ( ( 𝜑𝑤𝑇 ) → 𝜓 ) ) ↔ ( 𝑆 = 𝑤 → ( ( 𝜑𝑤𝑇 ) → 𝜒 ) ) ) )
19 18 cbvalvw ( ∀ 𝑥 ( 𝑅 = 𝑤 → ( ( 𝜑𝑤𝑇 ) → 𝜓 ) ) ↔ ∀ 𝑦 ( 𝑆 = 𝑤 → ( ( 𝜑𝑤𝑇 ) → 𝜒 ) ) )
20 15 19 bitrdi ( 𝑧 = 𝑤 → ( ∀ 𝑥 ( 𝑅 = 𝑧 → ( ( 𝜑𝑧𝑇 ) → 𝜓 ) ) ↔ ∀ 𝑦 ( 𝑆 = 𝑤 → ( ( 𝜑𝑤𝑇 ) → 𝜒 ) ) ) )
21 eqeq2 ( 𝑧 = 𝑇 → ( 𝑅 = 𝑧𝑅 = 𝑇 ) )
22 sseq1 ( 𝑧 = 𝑇 → ( 𝑧𝑇𝑇𝑇 ) )
23 22 anbi2d ( 𝑧 = 𝑇 → ( ( 𝜑𝑧𝑇 ) ↔ ( 𝜑𝑇𝑇 ) ) )
24 23 imbi1d ( 𝑧 = 𝑇 → ( ( ( 𝜑𝑧𝑇 ) → 𝜓 ) ↔ ( ( 𝜑𝑇𝑇 ) → 𝜓 ) ) )
25 21 24 imbi12d ( 𝑧 = 𝑇 → ( ( 𝑅 = 𝑧 → ( ( 𝜑𝑧𝑇 ) → 𝜓 ) ) ↔ ( 𝑅 = 𝑇 → ( ( 𝜑𝑇𝑇 ) → 𝜓 ) ) ) )
26 25 albidv ( 𝑧 = 𝑇 → ( ∀ 𝑥 ( 𝑅 = 𝑧 → ( ( 𝜑𝑧𝑇 ) → 𝜓 ) ) ↔ ∀ 𝑥 ( 𝑅 = 𝑇 → ( ( 𝜑𝑇𝑇 ) → 𝜓 ) ) ) )
27 simp3l ( ( ( 𝑧 ∈ On ∧ ∀ 𝑤𝑧𝑦 ( 𝑆 = 𝑤 → ( ( 𝜑𝑤𝑇 ) → 𝜒 ) ) ) ∧ 𝑅 = 𝑧 ∧ ( 𝜑𝑧𝑇 ) ) → 𝜑 )
28 simp2 ( ( ( 𝑧 ∈ On ∧ ∀ 𝑤𝑧𝑦 ( 𝑆 = 𝑤 → ( ( 𝜑𝑤𝑇 ) → 𝜒 ) ) ) ∧ 𝑅 = 𝑧 ∧ ( 𝜑𝑧𝑇 ) ) → 𝑅 = 𝑧 )
29 simp1l ( ( ( 𝑧 ∈ On ∧ ∀ 𝑤𝑧𝑦 ( 𝑆 = 𝑤 → ( ( 𝜑𝑤𝑇 ) → 𝜒 ) ) ) ∧ 𝑅 = 𝑧 ∧ ( 𝜑𝑧𝑇 ) ) → 𝑧 ∈ On )
30 28 29 eqeltrd ( ( ( 𝑧 ∈ On ∧ ∀ 𝑤𝑧𝑦 ( 𝑆 = 𝑤 → ( ( 𝜑𝑤𝑇 ) → 𝜒 ) ) ) ∧ 𝑅 = 𝑧 ∧ ( 𝜑𝑧𝑇 ) ) → 𝑅 ∈ On )
31 simp3r ( ( ( 𝑧 ∈ On ∧ ∀ 𝑤𝑧𝑦 ( 𝑆 = 𝑤 → ( ( 𝜑𝑤𝑇 ) → 𝜒 ) ) ) ∧ 𝑅 = 𝑧 ∧ ( 𝜑𝑧𝑇 ) ) → 𝑧𝑇 )
32 28 31 eqsstrd ( ( ( 𝑧 ∈ On ∧ ∀ 𝑤𝑧𝑦 ( 𝑆 = 𝑤 → ( ( 𝜑𝑤𝑇 ) → 𝜒 ) ) ) ∧ 𝑅 = 𝑧 ∧ ( 𝜑𝑧𝑇 ) ) → 𝑅𝑇 )
33 simpl3l ( ( ( ( 𝑧 ∈ On ∧ ∀ 𝑤𝑧𝑦 ( 𝑆 = 𝑤 → ( ( 𝜑𝑤𝑇 ) → 𝜒 ) ) ) ∧ 𝑅 = 𝑧 ∧ ( 𝜑𝑧𝑇 ) ) ∧ 𝑣 / 𝑥 𝑅𝑅 ) → 𝜑 )
34 simpl1l ( ( ( ( 𝑧 ∈ On ∧ ∀ 𝑤𝑧𝑦 ( 𝑆 = 𝑤 → ( ( 𝜑𝑤𝑇 ) → 𝜒 ) ) ) ∧ 𝑅 = 𝑧 ∧ ( 𝜑𝑧𝑇 ) ) ∧ 𝑣 / 𝑥 𝑅𝑅 ) → 𝑧 ∈ On )
35 simpr ( ( ( ( 𝑧 ∈ On ∧ ∀ 𝑤𝑧𝑦 ( 𝑆 = 𝑤 → ( ( 𝜑𝑤𝑇 ) → 𝜒 ) ) ) ∧ 𝑅 = 𝑧 ∧ ( 𝜑𝑧𝑇 ) ) ∧ 𝑣 / 𝑥 𝑅𝑅 ) → 𝑣 / 𝑥 𝑅𝑅 )
36 simpl2 ( ( ( ( 𝑧 ∈ On ∧ ∀ 𝑤𝑧𝑦 ( 𝑆 = 𝑤 → ( ( 𝜑𝑤𝑇 ) → 𝜒 ) ) ) ∧ 𝑅 = 𝑧 ∧ ( 𝜑𝑧𝑇 ) ) ∧ 𝑣 / 𝑥 𝑅𝑅 ) → 𝑅 = 𝑧 )
37 35 36 eleqtrd ( ( ( ( 𝑧 ∈ On ∧ ∀ 𝑤𝑧𝑦 ( 𝑆 = 𝑤 → ( ( 𝜑𝑤𝑇 ) → 𝜒 ) ) ) ∧ 𝑅 = 𝑧 ∧ ( 𝜑𝑧𝑇 ) ) ∧ 𝑣 / 𝑥 𝑅𝑅 ) → 𝑣 / 𝑥 𝑅𝑧 )
38 onelss ( 𝑧 ∈ On → ( 𝑣 / 𝑥 𝑅𝑧 𝑣 / 𝑥 𝑅𝑧 ) )
39 34 37 38 sylc ( ( ( ( 𝑧 ∈ On ∧ ∀ 𝑤𝑧𝑦 ( 𝑆 = 𝑤 → ( ( 𝜑𝑤𝑇 ) → 𝜒 ) ) ) ∧ 𝑅 = 𝑧 ∧ ( 𝜑𝑧𝑇 ) ) ∧ 𝑣 / 𝑥 𝑅𝑅 ) → 𝑣 / 𝑥 𝑅𝑧 )
40 simpl3r ( ( ( ( 𝑧 ∈ On ∧ ∀ 𝑤𝑧𝑦 ( 𝑆 = 𝑤 → ( ( 𝜑𝑤𝑇 ) → 𝜒 ) ) ) ∧ 𝑅 = 𝑧 ∧ ( 𝜑𝑧𝑇 ) ) ∧ 𝑣 / 𝑥 𝑅𝑅 ) → 𝑧𝑇 )
41 39 40 sstrd ( ( ( ( 𝑧 ∈ On ∧ ∀ 𝑤𝑧𝑦 ( 𝑆 = 𝑤 → ( ( 𝜑𝑤𝑇 ) → 𝜒 ) ) ) ∧ 𝑅 = 𝑧 ∧ ( 𝜑𝑧𝑇 ) ) ∧ 𝑣 / 𝑥 𝑅𝑅 ) → 𝑣 / 𝑥 𝑅𝑇 )
42 eqeq2 ( 𝑤 = 𝑣 / 𝑥 𝑅 → ( 𝑆 = 𝑤𝑆 = 𝑣 / 𝑥 𝑅 ) )
43 sseq1 ( 𝑤 = 𝑣 / 𝑥 𝑅 → ( 𝑤𝑇 𝑣 / 𝑥 𝑅𝑇 ) )
44 43 anbi2d ( 𝑤 = 𝑣 / 𝑥 𝑅 → ( ( 𝜑𝑤𝑇 ) ↔ ( 𝜑 𝑣 / 𝑥 𝑅𝑇 ) ) )
45 44 imbi1d ( 𝑤 = 𝑣 / 𝑥 𝑅 → ( ( ( 𝜑𝑤𝑇 ) → 𝜒 ) ↔ ( ( 𝜑 𝑣 / 𝑥 𝑅𝑇 ) → 𝜒 ) ) )
46 42 45 imbi12d ( 𝑤 = 𝑣 / 𝑥 𝑅 → ( ( 𝑆 = 𝑤 → ( ( 𝜑𝑤𝑇 ) → 𝜒 ) ) ↔ ( 𝑆 = 𝑣 / 𝑥 𝑅 → ( ( 𝜑 𝑣 / 𝑥 𝑅𝑇 ) → 𝜒 ) ) ) )
47 46 albidv ( 𝑤 = 𝑣 / 𝑥 𝑅 → ( ∀ 𝑦 ( 𝑆 = 𝑤 → ( ( 𝜑𝑤𝑇 ) → 𝜒 ) ) ↔ ∀ 𝑦 ( 𝑆 = 𝑣 / 𝑥 𝑅 → ( ( 𝜑 𝑣 / 𝑥 𝑅𝑇 ) → 𝜒 ) ) ) )
48 simpl1r ( ( ( ( 𝑧 ∈ On ∧ ∀ 𝑤𝑧𝑦 ( 𝑆 = 𝑤 → ( ( 𝜑𝑤𝑇 ) → 𝜒 ) ) ) ∧ 𝑅 = 𝑧 ∧ ( 𝜑𝑧𝑇 ) ) ∧ 𝑣 / 𝑥 𝑅𝑅 ) → ∀ 𝑤𝑧𝑦 ( 𝑆 = 𝑤 → ( ( 𝜑𝑤𝑇 ) → 𝜒 ) ) )
49 47 48 37 rspcdva ( ( ( ( 𝑧 ∈ On ∧ ∀ 𝑤𝑧𝑦 ( 𝑆 = 𝑤 → ( ( 𝜑𝑤𝑇 ) → 𝜒 ) ) ) ∧ 𝑅 = 𝑧 ∧ ( 𝜑𝑧𝑇 ) ) ∧ 𝑣 / 𝑥 𝑅𝑅 ) → ∀ 𝑦 ( 𝑆 = 𝑣 / 𝑥 𝑅 → ( ( 𝜑 𝑣 / 𝑥 𝑅𝑇 ) → 𝜒 ) ) )
50 eqidd ( ( ( ( 𝑧 ∈ On ∧ ∀ 𝑤𝑧𝑦 ( 𝑆 = 𝑤 → ( ( 𝜑𝑤𝑇 ) → 𝜒 ) ) ) ∧ 𝑅 = 𝑧 ∧ ( 𝜑𝑧𝑇 ) ) ∧ 𝑣 / 𝑥 𝑅𝑅 ) → 𝑣 / 𝑥 𝑅 = 𝑣 / 𝑥 𝑅 )
51 nfcv 𝑥 𝑦
52 nfcv 𝑥 𝑆
53 51 52 6 csbhypf ( 𝑣 = 𝑦 𝑣 / 𝑥 𝑅 = 𝑆 )
54 53 eqcomd ( 𝑣 = 𝑦𝑆 = 𝑣 / 𝑥 𝑅 )
55 54 equcoms ( 𝑦 = 𝑣𝑆 = 𝑣 / 𝑥 𝑅 )
56 55 eqeq1d ( 𝑦 = 𝑣 → ( 𝑆 = 𝑣 / 𝑥 𝑅 𝑣 / 𝑥 𝑅 = 𝑣 / 𝑥 𝑅 ) )
57 nfv 𝑥 𝜒
58 57 4 sbhypf ( 𝑣 = 𝑦 → ( [ 𝑣 / 𝑥 ] 𝜓𝜒 ) )
59 58 bicomd ( 𝑣 = 𝑦 → ( 𝜒 ↔ [ 𝑣 / 𝑥 ] 𝜓 ) )
60 59 equcoms ( 𝑦 = 𝑣 → ( 𝜒 ↔ [ 𝑣 / 𝑥 ] 𝜓 ) )
61 60 imbi2d ( 𝑦 = 𝑣 → ( ( ( 𝜑 𝑣 / 𝑥 𝑅𝑇 ) → 𝜒 ) ↔ ( ( 𝜑 𝑣 / 𝑥 𝑅𝑇 ) → [ 𝑣 / 𝑥 ] 𝜓 ) ) )
62 56 61 imbi12d ( 𝑦 = 𝑣 → ( ( 𝑆 = 𝑣 / 𝑥 𝑅 → ( ( 𝜑 𝑣 / 𝑥 𝑅𝑇 ) → 𝜒 ) ) ↔ ( 𝑣 / 𝑥 𝑅 = 𝑣 / 𝑥 𝑅 → ( ( 𝜑 𝑣 / 𝑥 𝑅𝑇 ) → [ 𝑣 / 𝑥 ] 𝜓 ) ) ) )
63 62 spvv ( ∀ 𝑦 ( 𝑆 = 𝑣 / 𝑥 𝑅 → ( ( 𝜑 𝑣 / 𝑥 𝑅𝑇 ) → 𝜒 ) ) → ( 𝑣 / 𝑥 𝑅 = 𝑣 / 𝑥 𝑅 → ( ( 𝜑 𝑣 / 𝑥 𝑅𝑇 ) → [ 𝑣 / 𝑥 ] 𝜓 ) ) )
64 49 50 63 sylc ( ( ( ( 𝑧 ∈ On ∧ ∀ 𝑤𝑧𝑦 ( 𝑆 = 𝑤 → ( ( 𝜑𝑤𝑇 ) → 𝜒 ) ) ) ∧ 𝑅 = 𝑧 ∧ ( 𝜑𝑧𝑇 ) ) ∧ 𝑣 / 𝑥 𝑅𝑅 ) → ( ( 𝜑 𝑣 / 𝑥 𝑅𝑇 ) → [ 𝑣 / 𝑥 ] 𝜓 ) )
65 33 41 64 mp2and ( ( ( ( 𝑧 ∈ On ∧ ∀ 𝑤𝑧𝑦 ( 𝑆 = 𝑤 → ( ( 𝜑𝑤𝑇 ) → 𝜒 ) ) ) ∧ 𝑅 = 𝑧 ∧ ( 𝜑𝑧𝑇 ) ) ∧ 𝑣 / 𝑥 𝑅𝑅 ) → [ 𝑣 / 𝑥 ] 𝜓 )
66 65 ex ( ( ( 𝑧 ∈ On ∧ ∀ 𝑤𝑧𝑦 ( 𝑆 = 𝑤 → ( ( 𝜑𝑤𝑇 ) → 𝜒 ) ) ) ∧ 𝑅 = 𝑧 ∧ ( 𝜑𝑧𝑇 ) ) → ( 𝑣 / 𝑥 𝑅𝑅 → [ 𝑣 / 𝑥 ] 𝜓 ) )
67 66 alrimiv ( ( ( 𝑧 ∈ On ∧ ∀ 𝑤𝑧𝑦 ( 𝑆 = 𝑤 → ( ( 𝜑𝑤𝑇 ) → 𝜒 ) ) ) ∧ 𝑅 = 𝑧 ∧ ( 𝜑𝑧𝑇 ) ) → ∀ 𝑣 ( 𝑣 / 𝑥 𝑅𝑅 → [ 𝑣 / 𝑥 ] 𝜓 ) )
68 53 eleq1d ( 𝑣 = 𝑦 → ( 𝑣 / 𝑥 𝑅𝑅𝑆𝑅 ) )
69 68 58 imbi12d ( 𝑣 = 𝑦 → ( ( 𝑣 / 𝑥 𝑅𝑅 → [ 𝑣 / 𝑥 ] 𝜓 ) ↔ ( 𝑆𝑅𝜒 ) ) )
70 69 cbvalvw ( ∀ 𝑣 ( 𝑣 / 𝑥 𝑅𝑅 → [ 𝑣 / 𝑥 ] 𝜓 ) ↔ ∀ 𝑦 ( 𝑆𝑅𝜒 ) )
71 67 70 sylib ( ( ( 𝑧 ∈ On ∧ ∀ 𝑤𝑧𝑦 ( 𝑆 = 𝑤 → ( ( 𝜑𝑤𝑇 ) → 𝜒 ) ) ) ∧ 𝑅 = 𝑧 ∧ ( 𝜑𝑧𝑇 ) ) → ∀ 𝑦 ( 𝑆𝑅𝜒 ) )
72 27 30 32 71 3 syl121anc ( ( ( 𝑧 ∈ On ∧ ∀ 𝑤𝑧𝑦 ( 𝑆 = 𝑤 → ( ( 𝜑𝑤𝑇 ) → 𝜒 ) ) ) ∧ 𝑅 = 𝑧 ∧ ( 𝜑𝑧𝑇 ) ) → 𝜓 )
73 72 3exp ( ( 𝑧 ∈ On ∧ ∀ 𝑤𝑧𝑦 ( 𝑆 = 𝑤 → ( ( 𝜑𝑤𝑇 ) → 𝜒 ) ) ) → ( 𝑅 = 𝑧 → ( ( 𝜑𝑧𝑇 ) → 𝜓 ) ) )
74 73 alrimiv ( ( 𝑧 ∈ On ∧ ∀ 𝑤𝑧𝑦 ( 𝑆 = 𝑤 → ( ( 𝜑𝑤𝑇 ) → 𝜒 ) ) ) → ∀ 𝑥 ( 𝑅 = 𝑧 → ( ( 𝜑𝑧𝑇 ) → 𝜓 ) ) )
75 74 ex ( 𝑧 ∈ On → ( ∀ 𝑤𝑧𝑦 ( 𝑆 = 𝑤 → ( ( 𝜑𝑤𝑇 ) → 𝜒 ) ) → ∀ 𝑥 ( 𝑅 = 𝑧 → ( ( 𝜑𝑧𝑇 ) → 𝜓 ) ) ) )
76 20 26 75 tfis3 ( 𝑇 ∈ On → ∀ 𝑥 ( 𝑅 = 𝑇 → ( ( 𝜑𝑇𝑇 ) → 𝜓 ) ) )
77 2 76 syl ( 𝜑 → ∀ 𝑥 ( 𝑅 = 𝑇 → ( ( 𝜑𝑇𝑇 ) → 𝜓 ) ) )
78 7 eqeq1d ( 𝑥 = 𝐴 → ( 𝑅 = 𝑇𝑇 = 𝑇 ) )
79 5 imbi2d ( 𝑥 = 𝐴 → ( ( ( 𝜑𝑇𝑇 ) → 𝜓 ) ↔ ( ( 𝜑𝑇𝑇 ) → 𝜃 ) ) )
80 78 79 imbi12d ( 𝑥 = 𝐴 → ( ( 𝑅 = 𝑇 → ( ( 𝜑𝑇𝑇 ) → 𝜓 ) ) ↔ ( 𝑇 = 𝑇 → ( ( 𝜑𝑇𝑇 ) → 𝜃 ) ) ) )
81 80 spcgv ( 𝐴𝑉 → ( ∀ 𝑥 ( 𝑅 = 𝑇 → ( ( 𝜑𝑇𝑇 ) → 𝜓 ) ) → ( 𝑇 = 𝑇 → ( ( 𝜑𝑇𝑇 ) → 𝜃 ) ) ) )
82 1 77 81 sylc ( 𝜑 → ( 𝑇 = 𝑇 → ( ( 𝜑𝑇𝑇 ) → 𝜃 ) ) )
83 9 82 mpi ( 𝜑 → ( ( 𝜑𝑇𝑇 ) → 𝜃 ) )
84 83 expd ( 𝜑 → ( 𝜑 → ( 𝑇𝑇𝜃 ) ) )
85 84 pm2.43i ( 𝜑 → ( 𝑇𝑇𝜃 ) )
86 8 85 mpi ( 𝜑𝜃 )