Theorem tfisi 7705

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 3943	. 2 ⊢ 𝑇 ⊆ 𝑇
2		eqid 2738	. . . . 5 ⊢ 𝑇 = 𝑇
3		tfisi.a	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
4		tfisi.b	. . . . . . 7 ⊢ (𝜑 → 𝑇 ∈ On)
5		eqeq2 2750	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑤 → (𝑅 = 𝑧 ↔ 𝑅 = 𝑤))
6		sseq1 3946	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑤 → (𝑧 ⊆ 𝑇 ↔ 𝑤 ⊆ 𝑇))
7	6	anbi2d 629	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑤 → ((𝜑 ∧ 𝑧 ⊆ 𝑇) ↔ (𝜑 ∧ 𝑤 ⊆ 𝑇)))
8	7	imbi1d 342	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑤 → (((𝜑 ∧ 𝑧 ⊆ 𝑇) → 𝜓) ↔ ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜓)))
9	5, 8	imbi12d 345	. . . . . . . . . 10 ⊢ (𝑧 = 𝑤 → ((𝑅 = 𝑧 → ((𝜑 ∧ 𝑧 ⊆ 𝑇) → 𝜓)) ↔ (𝑅 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜓))))
10	9	albidv 1923	. . . . . . . . 9 ⊢ (𝑧 = 𝑤 → (∀𝑥(𝑅 = 𝑧 → ((𝜑 ∧ 𝑧 ⊆ 𝑇) → 𝜓)) ↔ ∀𝑥(𝑅 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜓))))
11		tfisi.f	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → 𝑅 = 𝑆)
12	11	eqeq1d 2740	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (𝑅 = 𝑤 ↔ 𝑆 = 𝑤))
13		tfisi.d	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))
14	13	imbi2d 341	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜓) ↔ ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒)))
15	12, 14	imbi12d 345	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → ((𝑅 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜓)) ↔ (𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))))
16	15	cbvalvw 2039	. . . . . . . . 9 ⊢ (∀𝑥(𝑅 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜓)) ↔ ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒)))
17	10, 16	bitrdi 287	. . . . . . . 8 ⊢ (𝑧 = 𝑤 → (∀𝑥(𝑅 = 𝑧 → ((𝜑 ∧ 𝑧 ⊆ 𝑇) → 𝜓)) ↔ ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))))
18		eqeq2 2750	. . . . . . . . . 10 ⊢ (𝑧 = 𝑇 → (𝑅 = 𝑧 ↔ 𝑅 = 𝑇))
19		sseq1 3946	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑇 → (𝑧 ⊆ 𝑇 ↔ 𝑇 ⊆ 𝑇))
20	19	anbi2d 629	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑇 → ((𝜑 ∧ 𝑧 ⊆ 𝑇) ↔ (𝜑 ∧ 𝑇 ⊆ 𝑇)))
21	20	imbi1d 342	. . . . . . . . . 10 ⊢ (𝑧 = 𝑇 → (((𝜑 ∧ 𝑧 ⊆ 𝑇) → 𝜓) ↔ ((𝜑 ∧ 𝑇 ⊆ 𝑇) → 𝜓)))
22	18, 21	imbi12d 345	. . . . . . . . 9 ⊢ (𝑧 = 𝑇 → ((𝑅 = 𝑧 → ((𝜑 ∧ 𝑧 ⊆ 𝑇) → 𝜓)) ↔ (𝑅 = 𝑇 → ((𝜑 ∧ 𝑇 ⊆ 𝑇) → 𝜓))))
23	22	albidv 1923	. . . . . . . 8 ⊢ (𝑧 = 𝑇 → (∀𝑥(𝑅 = 𝑧 → ((𝜑 ∧ 𝑧 ⊆ 𝑇) → 𝜓)) ↔ ∀𝑥(𝑅 = 𝑇 → ((𝜑 ∧ 𝑇 ⊆ 𝑇) → 𝜓))))
24		simp3l 1200	. . . . . . . . . . . 12 ⊢ (((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) → 𝜑)
25		simp2 1136	. . . . . . . . . . . . 13 ⊢ (((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) → 𝑅 = 𝑧)
26		simp1l 1196	. . . . . . . . . . . . 13 ⊢ (((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) → 𝑧 ∈ On)
27	25, 26	eqeltrd 2839	. . . . . . . . . . . 12 ⊢ (((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) → 𝑅 ∈ On)
28		simp3r 1201	. . . . . . . . . . . . 13 ⊢ (((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) → 𝑧 ⊆ 𝑇)
29	25, 28	eqsstrd 3959	. . . . . . . . . . . 12 ⊢ (((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) → 𝑅 ⊆ 𝑇)
30		simpl3l 1227	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) ∧ ⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅) → 𝜑)
31		simpl1l 1223	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) ∧ ⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅) → 𝑧 ∈ On)
32		simpr 485	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) ∧ ⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅) → ⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅)
33		simpl2 1191	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) ∧ ⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅) → 𝑅 = 𝑧)
34	32, 33	eleqtrd 2841	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) ∧ ⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅) → ⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑧)
35		onelss 6308	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ On → (⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑧 → ⦋𝑣 / 𝑥⦌𝑅 ⊆ 𝑧))
36	31, 34, 35	sylc 65	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) ∧ ⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅) → ⦋𝑣 / 𝑥⦌𝑅 ⊆ 𝑧)
37		simpl3r 1228	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) ∧ ⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅) → 𝑧 ⊆ 𝑇)
38	36, 37	sstrd 3931	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) ∧ ⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅) → ⦋𝑣 / 𝑥⦌𝑅 ⊆ 𝑇)
39		eqeq2 2750	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = ⦋𝑣 / 𝑥⦌𝑅 → (𝑆 = 𝑤 ↔ 𝑆 = ⦋𝑣 / 𝑥⦌𝑅))
40		sseq1 3946	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 = ⦋𝑣 / 𝑥⦌𝑅 → (𝑤 ⊆ 𝑇 ↔ ⦋𝑣 / 𝑥⦌𝑅 ⊆ 𝑇))
41	40	anbi2d 629	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = ⦋𝑣 / 𝑥⦌𝑅 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) ↔ (𝜑 ∧ ⦋𝑣 / 𝑥⦌𝑅 ⊆ 𝑇)))
42	41	imbi1d 342	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = ⦋𝑣 / 𝑥⦌𝑅 → (((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒) ↔ ((𝜑 ∧ ⦋𝑣 / 𝑥⦌𝑅 ⊆ 𝑇) → 𝜒)))
43	39, 42	imbi12d 345	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = ⦋𝑣 / 𝑥⦌𝑅 → ((𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒)) ↔ (𝑆 = ⦋𝑣 / 𝑥⦌𝑅 → ((𝜑 ∧ ⦋𝑣 / 𝑥⦌𝑅 ⊆ 𝑇) → 𝜒))))
44	43	albidv 1923	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 = ⦋𝑣 / 𝑥⦌𝑅 → (∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒)) ↔ ∀𝑦(𝑆 = ⦋𝑣 / 𝑥⦌𝑅 → ((𝜑 ∧ ⦋𝑣 / 𝑥⦌𝑅 ⊆ 𝑇) → 𝜒))))
45		simpl1r 1224	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) ∧ ⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅) → ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒)))
46	44, 45, 34	rspcdva 3562	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) ∧ ⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅) → ∀𝑦(𝑆 = ⦋𝑣 / 𝑥⦌𝑅 → ((𝜑 ∧ ⦋𝑣 / 𝑥⦌𝑅 ⊆ 𝑇) → 𝜒)))
47		eqidd 2739	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) ∧ ⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅) → ⦋𝑣 / 𝑥⦌𝑅 = ⦋𝑣 / 𝑥⦌𝑅)
48		nfcv 2907	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑥𝑦
49		nfcv 2907	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑥𝑆
50	48, 49, 11	csbhypf 3861	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 = 𝑦 → ⦋𝑣 / 𝑥⦌𝑅 = 𝑆)
51	50	eqcomd 2744	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 = 𝑦 → 𝑆 = ⦋𝑣 / 𝑥⦌𝑅)
52	51	equcoms 2023	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑣 → 𝑆 = ⦋𝑣 / 𝑥⦌𝑅)
53	52	eqeq1d 2740	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑣 → (𝑆 = ⦋𝑣 / 𝑥⦌𝑅 ↔ ⦋𝑣 / 𝑥⦌𝑅 = ⦋𝑣 / 𝑥⦌𝑅))
54		nfv 1917	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑥𝜒
55	54, 13	sbhypf 3491	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 = 𝑦 → ([𝑣 / 𝑥]𝜓 ↔ 𝜒))
56	55	bicomd 222	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 = 𝑦 → (𝜒 ↔ [𝑣 / 𝑥]𝜓))
57	56	equcoms 2023	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑣 → (𝜒 ↔ [𝑣 / 𝑥]𝜓))
58	57	imbi2d 341	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑣 → (((𝜑 ∧ ⦋𝑣 / 𝑥⦌𝑅 ⊆ 𝑇) → 𝜒) ↔ ((𝜑 ∧ ⦋𝑣 / 𝑥⦌𝑅 ⊆ 𝑇) → [𝑣 / 𝑥]𝜓)))
59	53, 58	imbi12d 345	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑣 → ((𝑆 = ⦋𝑣 / 𝑥⦌𝑅 → ((𝜑 ∧ ⦋𝑣 / 𝑥⦌𝑅 ⊆ 𝑇) → 𝜒)) ↔ (⦋𝑣 / 𝑥⦌𝑅 = ⦋𝑣 / 𝑥⦌𝑅 → ((𝜑 ∧ ⦋𝑣 / 𝑥⦌𝑅 ⊆ 𝑇) → [𝑣 / 𝑥]𝜓))))
60	59	spvv 2000	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑦(𝑆 = ⦋𝑣 / 𝑥⦌𝑅 → ((𝜑 ∧ ⦋𝑣 / 𝑥⦌𝑅 ⊆ 𝑇) → 𝜒)) → (⦋𝑣 / 𝑥⦌𝑅 = ⦋𝑣 / 𝑥⦌𝑅 → ((𝜑 ∧ ⦋𝑣 / 𝑥⦌𝑅 ⊆ 𝑇) → [𝑣 / 𝑥]𝜓)))
61	46, 47, 60	sylc 65	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) ∧ ⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅) → ((𝜑 ∧ ⦋𝑣 / 𝑥⦌𝑅 ⊆ 𝑇) → [𝑣 / 𝑥]𝜓))
62	30, 38, 61	mp2and 696	. . . . . . . . . . . . . . 15 ⊢ ((((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) ∧ ⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅) → [𝑣 / 𝑥]𝜓)
63	62	ex 413	. . . . . . . . . . . . . 14 ⊢ (((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) → (⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅 → [𝑣 / 𝑥]𝜓))
64	63	alrimiv 1930	. . . . . . . . . . . . 13 ⊢ (((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) → ∀𝑣(⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅 → [𝑣 / 𝑥]𝜓))
65	50	eleq1d 2823	. . . . . . . . . . . . . . 15 ⊢ (𝑣 = 𝑦 → (⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅 ↔ 𝑆 ∈ 𝑅))
66	65, 55	imbi12d 345	. . . . . . . . . . . . . 14 ⊢ (𝑣 = 𝑦 → ((⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅 → [𝑣 / 𝑥]𝜓) ↔ (𝑆 ∈ 𝑅 → 𝜒)))
67	66	cbvalvw 2039	. . . . . . . . . . . . 13 ⊢ (∀𝑣(⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅 → [𝑣 / 𝑥]𝜓) ↔ ∀𝑦(𝑆 ∈ 𝑅 → 𝜒))
68	64, 67	sylib 217	. . . . . . . . . . . 12 ⊢ (((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) → ∀𝑦(𝑆 ∈ 𝑅 → 𝜒))
69		tfisi.c	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑅 ∈ On ∧ 𝑅 ⊆ 𝑇) ∧ ∀𝑦(𝑆 ∈ 𝑅 → 𝜒)) → 𝜓)
70	24, 27, 29, 68, 69	syl121anc 1374	. . . . . . . . . . 11 ⊢ (((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) → 𝜓)
71	70	3exp 1118	. . . . . . . . . 10 ⊢ ((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) → (𝑅 = 𝑧 → ((𝜑 ∧ 𝑧 ⊆ 𝑇) → 𝜓)))
72	71	alrimiv 1930	. . . . . . . . 9 ⊢ ((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) → ∀𝑥(𝑅 = 𝑧 → ((𝜑 ∧ 𝑧 ⊆ 𝑇) → 𝜓)))
73	72	ex 413	. . . . . . . 8 ⊢ (𝑧 ∈ On → (∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒)) → ∀𝑥(𝑅 = 𝑧 → ((𝜑 ∧ 𝑧 ⊆ 𝑇) → 𝜓))))
74	17, 23, 73	tfis3 7704	. . . . . . 7 ⊢ (𝑇 ∈ On → ∀𝑥(𝑅 = 𝑇 → ((𝜑 ∧ 𝑇 ⊆ 𝑇) → 𝜓)))
75	4, 74	syl 17	. . . . . 6 ⊢ (𝜑 → ∀𝑥(𝑅 = 𝑇 → ((𝜑 ∧ 𝑇 ⊆ 𝑇) → 𝜓)))
76		tfisi.g	. . . . . . . . 9 ⊢ (𝑥 = 𝐴 → 𝑅 = 𝑇)
77	76	eqeq1d 2740	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → (𝑅 = 𝑇 ↔ 𝑇 = 𝑇))
78		tfisi.e	. . . . . . . . 9 ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃))
79	78	imbi2d 341	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → (((𝜑 ∧ 𝑇 ⊆ 𝑇) → 𝜓) ↔ ((𝜑 ∧ 𝑇 ⊆ 𝑇) → 𝜃)))
80	77, 79	imbi12d 345	. . . . . . 7 ⊢ (𝑥 = 𝐴 → ((𝑅 = 𝑇 → ((𝜑 ∧ 𝑇 ⊆ 𝑇) → 𝜓)) ↔ (𝑇 = 𝑇 → ((𝜑 ∧ 𝑇 ⊆ 𝑇) → 𝜃))))
81	80	spcgv 3535	. . . . . 6 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑅 = 𝑇 → ((𝜑 ∧ 𝑇 ⊆ 𝑇) → 𝜓)) → (𝑇 = 𝑇 → ((𝜑 ∧ 𝑇 ⊆ 𝑇) → 𝜃))))
82	3, 75, 81	sylc 65	. . . . 5 ⊢ (𝜑 → (𝑇 = 𝑇 → ((𝜑 ∧ 𝑇 ⊆ 𝑇) → 𝜃)))
83	2, 82	mpi 20	. . . 4 ⊢ (𝜑 → ((𝜑 ∧ 𝑇 ⊆ 𝑇) → 𝜃))
84	83	expd 416	. . 3 ⊢ (𝜑 → (𝜑 → (𝑇 ⊆ 𝑇 → 𝜃)))
85	84	pm2.43i 52	. 2 ⊢ (𝜑 → (𝑇 ⊆ 𝑇 → 𝜃))
86	1, 85	mpi 20	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1086  ∀wal 1537   = wceq 1539  [wsb 2067   ∈ wcel 2106  ∀wral 3064  ⦋csb 3832   ⊆ wss 3887  Oncon0 6266

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-pss 3906  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-tr 5192  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-we 5546  df-ord 6269  df-on 6270

This theorem is referenced by:  indcardi  9797