This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝜑 → 𝜃 )