Theorem tfisi 7680

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 3939	. 2 ⊢ 𝑇 ⊆ 𝑇
2		eqid 2738	. . . . 5 ⊢ 𝑇 = 𝑇
3		tfisi.a	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
4		tfisi.b	. . . . . . 7 ⊢ (𝜑 → 𝑇 ∈ On)
5		eqeq2 2750	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑤 → (𝑅 = 𝑧 ↔ 𝑅 = 𝑤))
6		sseq1 3942	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑤 → (𝑧 ⊆ 𝑇 ↔ 𝑤 ⊆ 𝑇))
7	6	anbi2d 628	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑤 → ((𝜑 ∧ 𝑧 ⊆ 𝑇) ↔ (𝜑 ∧ 𝑤 ⊆ 𝑇)))
8	7	imbi1d 341	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑤 → (((𝜑 ∧ 𝑧 ⊆ 𝑇) → 𝜓) ↔ ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜓)))
9	5, 8	imbi12d 344	. . . . . . . . . 10 ⊢ (𝑧 = 𝑤 → ((𝑅 = 𝑧 → ((𝜑 ∧ 𝑧 ⊆ 𝑇) → 𝜓)) ↔ (𝑅 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜓))))
10	9	albidv 1924	. . . . . . . . 9 ⊢ (𝑧 = 𝑤 → (∀𝑥(𝑅 = 𝑧 → ((𝜑 ∧ 𝑧 ⊆ 𝑇) → 𝜓)) ↔ ∀𝑥(𝑅 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜓))))
11		tfisi.f	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → 𝑅 = 𝑆)
12	11	eqeq1d 2740	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (𝑅 = 𝑤 ↔ 𝑆 = 𝑤))
13		tfisi.d	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))
14	13	imbi2d 340	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜓) ↔ ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒)))
15	12, 14	imbi12d 344	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → ((𝑅 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜓)) ↔ (𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))))
16	15	cbvalvw 2040	. . . . . . . . 9 ⊢ (∀𝑥(𝑅 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜓)) ↔ ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒)))
17	10, 16	bitrdi 286	. . . . . . . 8 ⊢ (𝑧 = 𝑤 → (∀𝑥(𝑅 = 𝑧 → ((𝜑 ∧ 𝑧 ⊆ 𝑇) → 𝜓)) ↔ ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))))
18		eqeq2 2750	. . . . . . . . . 10 ⊢ (𝑧 = 𝑇 → (𝑅 = 𝑧 ↔ 𝑅 = 𝑇))
19		sseq1 3942	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑇 → (𝑧 ⊆ 𝑇 ↔ 𝑇 ⊆ 𝑇))
20	19	anbi2d 628	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑇 → ((𝜑 ∧ 𝑧 ⊆ 𝑇) ↔ (𝜑 ∧ 𝑇 ⊆ 𝑇)))
21	20	imbi1d 341	. . . . . . . . . 10 ⊢ (𝑧 = 𝑇 → (((𝜑 ∧ 𝑧 ⊆ 𝑇) → 𝜓) ↔ ((𝜑 ∧ 𝑇 ⊆ 𝑇) → 𝜓)))
22	18, 21	imbi12d 344	. . . . . . . . 9 ⊢ (𝑧 = 𝑇 → ((𝑅 = 𝑧 → ((𝜑 ∧ 𝑧 ⊆ 𝑇) → 𝜓)) ↔ (𝑅 = 𝑇 → ((𝜑 ∧ 𝑇 ⊆ 𝑇) → 𝜓))))
23	22	albidv 1924	. . . . . . . 8 ⊢ (𝑧 = 𝑇 → (∀𝑥(𝑅 = 𝑧 → ((𝜑 ∧ 𝑧 ⊆ 𝑇) → 𝜓)) ↔ ∀𝑥(𝑅 = 𝑇 → ((𝜑 ∧ 𝑇 ⊆ 𝑇) → 𝜓))))
24		simp3l 1199	. . . . . . . . . . . 12 ⊢ (((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) → 𝜑)
25		simp2 1135	. . . . . . . . . . . . 13 ⊢ (((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) → 𝑅 = 𝑧)
26		simp1l 1195	. . . . . . . . . . . . 13 ⊢ (((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) → 𝑧 ∈ On)
27	25, 26	eqeltrd 2839	. . . . . . . . . . . 12 ⊢ (((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) → 𝑅 ∈ On)
28		simp3r 1200	. . . . . . . . . . . . 13 ⊢ (((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) → 𝑧 ⊆ 𝑇)
29	25, 28	eqsstrd 3955	. . . . . . . . . . . 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 2841	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) ∧ ⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅) → ⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑧)
35		onelss 6293	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ On → (⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑧 → ⦋𝑣 / 𝑥⦌𝑅 ⊆ 𝑧))
36	31, 34, 35	sylc 65	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) ∧ ⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅) → ⦋𝑣 / 𝑥⦌𝑅 ⊆ 𝑧)
37		simpl3r 1227	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) ∧ ⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅) → 𝑧 ⊆ 𝑇)
38	36, 37	sstrd 3927	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) ∧ ⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅) → ⦋𝑣 / 𝑥⦌𝑅 ⊆ 𝑇)
39		eqeq2 2750	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = ⦋𝑣 / 𝑥⦌𝑅 → (𝑆 = 𝑤 ↔ 𝑆 = ⦋𝑣 / 𝑥⦌𝑅))
40		sseq1 3942	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 = ⦋𝑣 / 𝑥⦌𝑅 → (𝑤 ⊆ 𝑇 ↔ ⦋𝑣 / 𝑥⦌𝑅 ⊆ 𝑇))
41	40	anbi2d 628	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = ⦋𝑣 / 𝑥⦌𝑅 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) ↔ (𝜑 ∧ ⦋𝑣 / 𝑥⦌𝑅 ⊆ 𝑇)))
42	41	imbi1d 341	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = ⦋𝑣 / 𝑥⦌𝑅 → (((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒) ↔ ((𝜑 ∧ ⦋𝑣 / 𝑥⦌𝑅 ⊆ 𝑇) → 𝜒)))
43	39, 42	imbi12d 344	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = ⦋𝑣 / 𝑥⦌𝑅 → ((𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒)) ↔ (𝑆 = ⦋𝑣 / 𝑥⦌𝑅 → ((𝜑 ∧ ⦋𝑣 / 𝑥⦌𝑅 ⊆ 𝑇) → 𝜒))))
44	43	albidv 1924	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 = ⦋𝑣 / 𝑥⦌𝑅 → (∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒)) ↔ ∀𝑦(𝑆 = ⦋𝑣 / 𝑥⦌𝑅 → ((𝜑 ∧ ⦋𝑣 / 𝑥⦌𝑅 ⊆ 𝑇) → 𝜒))))
45		simpl1r 1223	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) ∧ ⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅) → ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒)))
46	44, 45, 34	rspcdva 3554	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) ∧ ⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅) → ∀𝑦(𝑆 = ⦋𝑣 / 𝑥⦌𝑅 → ((𝜑 ∧ ⦋𝑣 / 𝑥⦌𝑅 ⊆ 𝑇) → 𝜒)))
47		eqidd 2739	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) ∧ ⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅) → ⦋𝑣 / 𝑥⦌𝑅 = ⦋𝑣 / 𝑥⦌𝑅)
48		nfcv 2906	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑥𝑦
49		nfcv 2906	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑥𝑆
50	48, 49, 11	csbhypf 3857	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 = 𝑦 → ⦋𝑣 / 𝑥⦌𝑅 = 𝑆)
51	50	eqcomd 2744	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 = 𝑦 → 𝑆 = ⦋𝑣 / 𝑥⦌𝑅)
52	51	equcoms 2024	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑣 → 𝑆 = ⦋𝑣 / 𝑥⦌𝑅)
53	52	eqeq1d 2740	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑣 → (𝑆 = ⦋𝑣 / 𝑥⦌𝑅 ↔ ⦋𝑣 / 𝑥⦌𝑅 = ⦋𝑣 / 𝑥⦌𝑅))
54		nfv 1918	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑥𝜒
55	54, 13	sbhypf 3481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 = 𝑦 → ([𝑣 / 𝑥]𝜓 ↔ 𝜒))
56	55	bicomd 222	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 = 𝑦 → (𝜒 ↔ [𝑣 / 𝑥]𝜓))
57	56	equcoms 2024	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑣 → (𝜒 ↔ [𝑣 / 𝑥]𝜓))
58	57	imbi2d 340	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑣 → (((𝜑 ∧ ⦋𝑣 / 𝑥⦌𝑅 ⊆ 𝑇) → 𝜒) ↔ ((𝜑 ∧ ⦋𝑣 / 𝑥⦌𝑅 ⊆ 𝑇) → [𝑣 / 𝑥]𝜓)))
59	53, 58	imbi12d 344	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑣 → ((𝑆 = ⦋𝑣 / 𝑥⦌𝑅 → ((𝜑 ∧ ⦋𝑣 / 𝑥⦌𝑅 ⊆ 𝑇) → 𝜒)) ↔ (⦋𝑣 / 𝑥⦌𝑅 = ⦋𝑣 / 𝑥⦌𝑅 → ((𝜑 ∧ ⦋𝑣 / 𝑥⦌𝑅 ⊆ 𝑇) → [𝑣 / 𝑥]𝜓))))
60	59	spvv 2001	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑦(𝑆 = ⦋𝑣 / 𝑥⦌𝑅 → ((𝜑 ∧ ⦋𝑣 / 𝑥⦌𝑅 ⊆ 𝑇) → 𝜒)) → (⦋𝑣 / 𝑥⦌𝑅 = ⦋𝑣 / 𝑥⦌𝑅 → ((𝜑 ∧ ⦋𝑣 / 𝑥⦌𝑅 ⊆ 𝑇) → [𝑣 / 𝑥]𝜓)))
61	46, 47, 60	sylc 65	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) ∧ ⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅) → ((𝜑 ∧ ⦋𝑣 / 𝑥⦌𝑅 ⊆ 𝑇) → [𝑣 / 𝑥]𝜓))
62	30, 38, 61	mp2and 695	. . . . . . . . . . . . . . 15 ⊢ ((((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) ∧ ⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅) → [𝑣 / 𝑥]𝜓)
63	62	ex 412	. . . . . . . . . . . . . 14 ⊢ (((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) → (⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅 → [𝑣 / 𝑥]𝜓))
64	63	alrimiv 1931	. . . . . . . . . . . . 13 ⊢ (((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) → ∀𝑣(⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅 → [𝑣 / 𝑥]𝜓))
65	50	eleq1d 2823	. . . . . . . . . . . . . . 15 ⊢ (𝑣 = 𝑦 → (⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅 ↔ 𝑆 ∈ 𝑅))
66	65, 55	imbi12d 344	. . . . . . . . . . . . . 14 ⊢ (𝑣 = 𝑦 → ((⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅 → [𝑣 / 𝑥]𝜓) ↔ (𝑆 ∈ 𝑅 → 𝜒)))
67	66	cbvalvw 2040	. . . . . . . . . . . . 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 1931	. . . . . . . . 9 ⊢ ((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) → ∀𝑥(𝑅 = 𝑧 → ((𝜑 ∧ 𝑧 ⊆ 𝑇) → 𝜓)))
73	72	ex 412	. . . . . . . 8 ⊢ (𝑧 ∈ On → (∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒)) → ∀𝑥(𝑅 = 𝑧 → ((𝜑 ∧ 𝑧 ⊆ 𝑇) → 𝜓))))
74	17, 23, 73	tfis3 7679	. . . . . . 7 ⊢ (𝑇 ∈ On → ∀𝑥(𝑅 = 𝑇 → ((𝜑 ∧ 𝑇 ⊆ 𝑇) → 𝜓)))
75	4, 74	syl 17	. . . . . 6 ⊢ (𝜑 → ∀𝑥(𝑅 = 𝑇 → ((𝜑 ∧ 𝑇 ⊆ 𝑇) → 𝜓)))
76		tfisi.g	. . . . . . . . 9 ⊢ (𝑥 = 𝐴 → 𝑅 = 𝑇)
77	76	eqeq1d 2740	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → (𝑅 = 𝑇 ↔ 𝑇 = 𝑇))
78		tfisi.e	. . . . . . . . 9 ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃))
79	78	imbi2d 340	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → (((𝜑 ∧ 𝑇 ⊆ 𝑇) → 𝜓) ↔ ((𝜑 ∧ 𝑇 ⊆ 𝑇) → 𝜃)))
80	77, 79	imbi12d 344	. . . . . . 7 ⊢ (𝑥 = 𝐴 → ((𝑅 = 𝑇 → ((𝜑 ∧ 𝑇 ⊆ 𝑇) → 𝜓)) ↔ (𝑇 = 𝑇 → ((𝜑 ∧ 𝑇 ⊆ 𝑇) → 𝜃))))
81	80	spcgv 3525	. . . . . 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 1537   = wceq 1539  [wsb 2068   ∈ wcel 2108  ∀wral 3063  ⦋csb 3828   ⊆ wss 3883  Oncon0 6251

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347  ax-un 7566

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-tr 5188  df-eprel 5486  df-po 5494  df-so 5495  df-fr 5535  df-we 5537  df-ord 6254  df-on 6255

This theorem is referenced by:  indcardi  9728