Theorem tfisi 7863

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.)

Hypotheses

Ref	Expression
tfisi.a	⊢ (𝜑 → 𝐴 ∈ 𝑉)
tfisi.b	⊢ (𝜑 → 𝑇 ∈ On)
tfisi.c	⊢ ((𝜑 ∧ (𝑅 ∈ On ∧ 𝑅 ⊆ 𝑇) ∧ ∀𝑦(𝑆 ∈ 𝑅 → 𝜒)) → 𝜓)
tfisi.d	⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))
tfisi.e	⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃))
tfisi.f	⊢ (𝑥 = 𝑦 → 𝑅 = 𝑆)
tfisi.g	⊢ (𝑥 = 𝐴 → 𝑅 = 𝑇)

Assertion

Ref	Expression
tfisi	⊢ (𝜑 → 𝜃)

Distinct variable groups:   𝑥,𝑦,𝑇   𝑦,𝑅   𝑥,𝑆   𝜒,𝑥   𝜑,𝑥,𝑦   𝜓,𝑦   𝑥,𝐴   𝜃,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑦)   𝜃(𝑦)   𝐴(𝑦)   𝑅(𝑥)   𝑆(𝑦)   𝑉(𝑥,𝑦)

Proof of Theorem tfisi

Dummy variables 𝑣 𝑤 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ssid 4002	. 2 ⊢ 𝑇 ⊆ 𝑇
2		eqid 2728	. . . . 5 ⊢ 𝑇 = 𝑇
3		tfisi.a	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
4		tfisi.b	. . . . . . 7 ⊢ (𝜑 → 𝑇 ∈ On)
5		eqeq2 2740	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑤 → (𝑅 = 𝑧 ↔ 𝑅 = 𝑤))
6		sseq1 4005	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑤 → (𝑧 ⊆ 𝑇 ↔ 𝑤 ⊆ 𝑇))
7	6	anbi2d 629	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑤 → ((𝜑 ∧ 𝑧 ⊆ 𝑇) ↔ (𝜑 ∧ 𝑤 ⊆ 𝑇)))
8	7	imbi1d 341	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑤 → (((𝜑 ∧ 𝑧 ⊆ 𝑇) → 𝜓) ↔ ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜓)))
9	5, 8	imbi12d 344	. . . . . . . . . 10 ⊢ (𝑧 = 𝑤 → ((𝑅 = 𝑧 → ((𝜑 ∧ 𝑧 ⊆ 𝑇) → 𝜓)) ↔ (𝑅 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜓))))
10	9	albidv 1916	. . . . . . . . 9 ⊢ (𝑧 = 𝑤 → (∀𝑥(𝑅 = 𝑧 → ((𝜑 ∧ 𝑧 ⊆ 𝑇) → 𝜓)) ↔ ∀𝑥(𝑅 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜓))))
11		tfisi.f	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → 𝑅 = 𝑆)
12	11	eqeq1d 2730	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (𝑅 = 𝑤 ↔ 𝑆 = 𝑤))
13		tfisi.d	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))
14	13	imbi2d 340	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜓) ↔ ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒)))
15	12, 14	imbi12d 344	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → ((𝑅 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜓)) ↔ (𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))))
16	15	cbvalvw 2032	. . . . . . . . 9 ⊢ (∀𝑥(𝑅 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜓)) ↔ ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒)))
17	10, 16	bitrdi 287	. . . . . . . 8 ⊢ (𝑧 = 𝑤 → (∀𝑥(𝑅 = 𝑧 → ((𝜑 ∧ 𝑧 ⊆ 𝑇) → 𝜓)) ↔ ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))))
18		eqeq2 2740	. . . . . . . . . 10 ⊢ (𝑧 = 𝑇 → (𝑅 = 𝑧 ↔ 𝑅 = 𝑇))
19		sseq1 4005	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑇 → (𝑧 ⊆ 𝑇 ↔ 𝑇 ⊆ 𝑇))
20	19	anbi2d 629	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑇 → ((𝜑 ∧ 𝑧 ⊆ 𝑇) ↔ (𝜑 ∧ 𝑇 ⊆ 𝑇)))
21	20	imbi1d 341	. . . . . . . . . 10 ⊢ (𝑧 = 𝑇 → (((𝜑 ∧ 𝑧 ⊆ 𝑇) → 𝜓) ↔ ((𝜑 ∧ 𝑇 ⊆ 𝑇) → 𝜓)))
22	18, 21	imbi12d 344	. . . . . . . . 9 ⊢ (𝑧 = 𝑇 → ((𝑅 = 𝑧 → ((𝜑 ∧ 𝑧 ⊆ 𝑇) → 𝜓)) ↔ (𝑅 = 𝑇 → ((𝜑 ∧ 𝑇 ⊆ 𝑇) → 𝜓))))
23	22	albidv 1916	. . . . . . . 8 ⊢ (𝑧 = 𝑇 → (∀𝑥(𝑅 = 𝑧 → ((𝜑 ∧ 𝑧 ⊆ 𝑇) → 𝜓)) ↔ ∀𝑥(𝑅 = 𝑇 → ((𝜑 ∧ 𝑇 ⊆ 𝑇) → 𝜓))))
24		simp3l 1199	. . . . . . . . . . . 12 ⊢ (((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) → 𝜑)
25		simp2 1135	. . . . . . . . . . . . 13 ⊢ (((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) → 𝑅 = 𝑧)
26		simp1l 1195	. . . . . . . . . . . . 13 ⊢ (((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) → 𝑧 ∈ On)
27	25, 26	eqeltrd 2829	. . . . . . . . . . . 12 ⊢ (((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) → 𝑅 ∈ On)
28		simp3r 1200	. . . . . . . . . . . . 13 ⊢ (((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) → 𝑧 ⊆ 𝑇)
29	25, 28	eqsstrd 4018	. . . . . . . . . . . 12 ⊢ (((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) → 𝑅 ⊆ 𝑇)
30		simpl3l 1226	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) ∧ ⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅) → 𝜑)
31		simpl1l 1222	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) ∧ ⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅) → 𝑧 ∈ On)
32		simpr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) ∧ ⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅) → ⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅)
33		simpl2 1190	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) ∧ ⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅) → 𝑅 = 𝑧)
34	32, 33	eleqtrd 2831	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) ∧ ⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅) → ⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑧)
35		onelss 6411	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ On → (⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑧 → ⦋𝑣 / 𝑥⦌𝑅 ⊆ 𝑧))
36	31, 34, 35	sylc 65	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) ∧ ⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅) → ⦋𝑣 / 𝑥⦌𝑅 ⊆ 𝑧)
37		simpl3r 1227	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) ∧ ⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅) → 𝑧 ⊆ 𝑇)
38	36, 37	sstrd 3990	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) ∧ ⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅) → ⦋𝑣 / 𝑥⦌𝑅 ⊆ 𝑇)
39		eqeq2 2740	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = ⦋𝑣 / 𝑥⦌𝑅 → (𝑆 = 𝑤 ↔ 𝑆 = ⦋𝑣 / 𝑥⦌𝑅))
40		sseq1 4005	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 = ⦋𝑣 / 𝑥⦌𝑅 → (𝑤 ⊆ 𝑇 ↔ ⦋𝑣 / 𝑥⦌𝑅 ⊆ 𝑇))
41	40	anbi2d 629	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = ⦋𝑣 / 𝑥⦌𝑅 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) ↔ (𝜑 ∧ ⦋𝑣 / 𝑥⦌𝑅 ⊆ 𝑇)))
42	41	imbi1d 341	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = ⦋𝑣 / 𝑥⦌𝑅 → (((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒) ↔ ((𝜑 ∧ ⦋𝑣 / 𝑥⦌𝑅 ⊆ 𝑇) → 𝜒)))
43	39, 42	imbi12d 344	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = ⦋𝑣 / 𝑥⦌𝑅 → ((𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒)) ↔ (𝑆 = ⦋𝑣 / 𝑥⦌𝑅 → ((𝜑 ∧ ⦋𝑣 / 𝑥⦌𝑅 ⊆ 𝑇) → 𝜒))))
44	43	albidv 1916	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 = ⦋𝑣 / 𝑥⦌𝑅 → (∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒)) ↔ ∀𝑦(𝑆 = ⦋𝑣 / 𝑥⦌𝑅 → ((𝜑 ∧ ⦋𝑣 / 𝑥⦌𝑅 ⊆ 𝑇) → 𝜒))))
45		simpl1r 1223	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) ∧ ⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅) → ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒)))
46	44, 45, 34	rspcdva 3610	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) ∧ ⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅) → ∀𝑦(𝑆 = ⦋𝑣 / 𝑥⦌𝑅 → ((𝜑 ∧ ⦋𝑣 / 𝑥⦌𝑅 ⊆ 𝑇) → 𝜒)))
47		eqidd 2729	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) ∧ ⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅) → ⦋𝑣 / 𝑥⦌𝑅 = ⦋𝑣 / 𝑥⦌𝑅)
48		nfcv 2899	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑥𝑦
49		nfcv 2899	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑥𝑆
50	48, 49, 11	csbhypf 3921	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 = 𝑦 → ⦋𝑣 / 𝑥⦌𝑅 = 𝑆)
51	50	eqcomd 2734	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 = 𝑦 → 𝑆 = ⦋𝑣 / 𝑥⦌𝑅)
52	51	equcoms 2016	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑣 → 𝑆 = ⦋𝑣 / 𝑥⦌𝑅)
53	52	eqeq1d 2730	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑣 → (𝑆 = ⦋𝑣 / 𝑥⦌𝑅 ↔ ⦋𝑣 / 𝑥⦌𝑅 = ⦋𝑣 / 𝑥⦌𝑅))
54		nfv 1910	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑥𝜒
55	54, 13	sbhypf 3536	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 = 𝑦 → ([𝑣 / 𝑥]𝜓 ↔ 𝜒))
56	55	bicomd 222	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 = 𝑦 → (𝜒 ↔ [𝑣 / 𝑥]𝜓))
57	56	equcoms 2016	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑣 → (𝜒 ↔ [𝑣 / 𝑥]𝜓))
58	57	imbi2d 340	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑣 → (((𝜑 ∧ ⦋𝑣 / 𝑥⦌𝑅 ⊆ 𝑇) → 𝜒) ↔ ((𝜑 ∧ ⦋𝑣 / 𝑥⦌𝑅 ⊆ 𝑇) → [𝑣 / 𝑥]𝜓)))
59	53, 58	imbi12d 344	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑣 → ((𝑆 = ⦋𝑣 / 𝑥⦌𝑅 → ((𝜑 ∧ ⦋𝑣 / 𝑥⦌𝑅 ⊆ 𝑇) → 𝜒)) ↔ (⦋𝑣 / 𝑥⦌𝑅 = ⦋𝑣 / 𝑥⦌𝑅 → ((𝜑 ∧ ⦋𝑣 / 𝑥⦌𝑅 ⊆ 𝑇) → [𝑣 / 𝑥]𝜓))))
60	59	spvv 1993	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑦(𝑆 = ⦋𝑣 / 𝑥⦌𝑅 → ((𝜑 ∧ ⦋𝑣 / 𝑥⦌𝑅 ⊆ 𝑇) → 𝜒)) → (⦋𝑣 / 𝑥⦌𝑅 = ⦋𝑣 / 𝑥⦌𝑅 → ((𝜑 ∧ ⦋𝑣 / 𝑥⦌𝑅 ⊆ 𝑇) → [𝑣 / 𝑥]𝜓)))
61	46, 47, 60	sylc 65	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) ∧ ⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅) → ((𝜑 ∧ ⦋𝑣 / 𝑥⦌𝑅 ⊆ 𝑇) → [𝑣 / 𝑥]𝜓))
62	30, 38, 61	mp2and 698	. . . . . . . . . . . . . . 15 ⊢ ((((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) ∧ ⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅) → [𝑣 / 𝑥]𝜓)
63	62	ex 412	. . . . . . . . . . . . . 14 ⊢ (((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) → (⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅 → [𝑣 / 𝑥]𝜓))
64	63	alrimiv 1923	. . . . . . . . . . . . 13 ⊢ (((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) → ∀𝑣(⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅 → [𝑣 / 𝑥]𝜓))
65	50	eleq1d 2814	. . . . . . . . . . . . . . 15 ⊢ (𝑣 = 𝑦 → (⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅 ↔ 𝑆 ∈ 𝑅))
66	65, 55	imbi12d 344	. . . . . . . . . . . . . 14 ⊢ (𝑣 = 𝑦 → ((⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅 → [𝑣 / 𝑥]𝜓) ↔ (𝑆 ∈ 𝑅 → 𝜒)))
67	66	cbvalvw 2032	. . . . . . . . . . . . 13 ⊢ (∀𝑣(⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅 → [𝑣 / 𝑥]𝜓) ↔ ∀𝑦(𝑆 ∈ 𝑅 → 𝜒))
68	64, 67	sylib 217	. . . . . . . . . . . 12 ⊢ (((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) → ∀𝑦(𝑆 ∈ 𝑅 → 𝜒))
69		tfisi.c	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑅 ∈ On ∧ 𝑅 ⊆ 𝑇) ∧ ∀𝑦(𝑆 ∈ 𝑅 → 𝜒)) → 𝜓)
70	24, 27, 29, 68, 69	syl121anc 1373	. . . . . . . . . . 11 ⊢ (((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) → 𝜓)
71	70	3exp 1117	. . . . . . . . . 10 ⊢ ((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) → (𝑅 = 𝑧 → ((𝜑 ∧ 𝑧 ⊆ 𝑇) → 𝜓)))
72	71	alrimiv 1923	. . . . . . . . 9 ⊢ ((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) → ∀𝑥(𝑅 = 𝑧 → ((𝜑 ∧ 𝑧 ⊆ 𝑇) → 𝜓)))
73	72	ex 412	. . . . . . . 8 ⊢ (𝑧 ∈ On → (∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒)) → ∀𝑥(𝑅 = 𝑧 → ((𝜑 ∧ 𝑧 ⊆ 𝑇) → 𝜓))))
74	17, 23, 73	tfis3 7862	. . . . . . 7 ⊢ (𝑇 ∈ On → ∀𝑥(𝑅 = 𝑇 → ((𝜑 ∧ 𝑇 ⊆ 𝑇) → 𝜓)))
75	4, 74	syl 17	. . . . . 6 ⊢ (𝜑 → ∀𝑥(𝑅 = 𝑇 → ((𝜑 ∧ 𝑇 ⊆ 𝑇) → 𝜓)))
76		tfisi.g	. . . . . . . . 9 ⊢ (𝑥 = 𝐴 → 𝑅 = 𝑇)
77	76	eqeq1d 2730	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → (𝑅 = 𝑇 ↔ 𝑇 = 𝑇))
78		tfisi.e	. . . . . . . . 9 ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃))
79	78	imbi2d 340	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → (((𝜑 ∧ 𝑇 ⊆ 𝑇) → 𝜓) ↔ ((𝜑 ∧ 𝑇 ⊆ 𝑇) → 𝜃)))
80	77, 79	imbi12d 344	. . . . . . 7 ⊢ (𝑥 = 𝐴 → ((𝑅 = 𝑇 → ((𝜑 ∧ 𝑇 ⊆ 𝑇) → 𝜓)) ↔ (𝑇 = 𝑇 → ((𝜑 ∧ 𝑇 ⊆ 𝑇) → 𝜃))))
81	80	spcgv 3583	. . . . . 6 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑅 = 𝑇 → ((𝜑 ∧ 𝑇 ⊆ 𝑇) → 𝜓)) → (𝑇 = 𝑇 → ((𝜑 ∧ 𝑇 ⊆ 𝑇) → 𝜃))))
82	3, 75, 81	sylc 65	. . . . 5 ⊢ (𝜑 → (𝑇 = 𝑇 → ((𝜑 ∧ 𝑇 ⊆ 𝑇) → 𝜃)))
83	2, 82	mpi 20	. . . 4 ⊢ (𝜑 → ((𝜑 ∧ 𝑇 ⊆ 𝑇) → 𝜃))
84	83	expd 415	. . 3 ⊢ (𝜑 → (𝜑 → (𝑇 ⊆ 𝑇 → 𝜃)))
85	84	pm2.43i 52	. 2 ⊢ (𝜑 → (𝑇 ⊆ 𝑇 → 𝜃))
86	1, 85	mpi 20	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1085  ∀wal 1532   = wceq 1534  [wsb 2060   ∈ wcel 2099  ∀wral 3058  ⦋csb 3892   ⊆ wss 3947  Oncon0 6369

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699  ax-sep 5299  ax-nul 5306  ax-pr 5429

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3430  df-v 3473  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-br 5149  df-opab 5211  df-tr 5266  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5633  df-we 5635  df-ord 6372  df-on 6373

This theorem is referenced by:  indcardi  10065