Theorem tfisi 7553

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 3937	. 2 ⊢ 𝑇 ⊆ 𝑇
2		eqid 2798	. . . . 5 ⊢ 𝑇 = 𝑇
3		tfisi.a	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
4		tfisi.b	. . . . . . 7 ⊢ (𝜑 → 𝑇 ∈ On)
5		eqeq2 2810	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑤 → (𝑅 = 𝑧 ↔ 𝑅 = 𝑤))
6		sseq1 3940	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑤 → (𝑧 ⊆ 𝑇 ↔ 𝑤 ⊆ 𝑇))
7	6	anbi2d 631	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑤 → ((𝜑 ∧ 𝑧 ⊆ 𝑇) ↔ (𝜑 ∧ 𝑤 ⊆ 𝑇)))
8	7	imbi1d 345	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑤 → (((𝜑 ∧ 𝑧 ⊆ 𝑇) → 𝜓) ↔ ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜓)))
9	5, 8	imbi12d 348	. . . . . . . . . 10 ⊢ (𝑧 = 𝑤 → ((𝑅 = 𝑧 → ((𝜑 ∧ 𝑧 ⊆ 𝑇) → 𝜓)) ↔ (𝑅 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜓))))
10	9	albidv 1921	. . . . . . . . 9 ⊢ (𝑧 = 𝑤 → (∀𝑥(𝑅 = 𝑧 → ((𝜑 ∧ 𝑧 ⊆ 𝑇) → 𝜓)) ↔ ∀𝑥(𝑅 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜓))))
11		tfisi.f	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → 𝑅 = 𝑆)
12	11	eqeq1d 2800	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (𝑅 = 𝑤 ↔ 𝑆 = 𝑤))
13		tfisi.d	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))
14	13	imbi2d 344	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜓) ↔ ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒)))
15	12, 14	imbi12d 348	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → ((𝑅 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜓)) ↔ (𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))))
16	15	cbvalvw 2043	. . . . . . . . 9 ⊢ (∀𝑥(𝑅 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜓)) ↔ ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒)))
17	10, 16	syl6bb 290	. . . . . . . 8 ⊢ (𝑧 = 𝑤 → (∀𝑥(𝑅 = 𝑧 → ((𝜑 ∧ 𝑧 ⊆ 𝑇) → 𝜓)) ↔ ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))))
18		eqeq2 2810	. . . . . . . . . 10 ⊢ (𝑧 = 𝑇 → (𝑅 = 𝑧 ↔ 𝑅 = 𝑇))
19		sseq1 3940	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑇 → (𝑧 ⊆ 𝑇 ↔ 𝑇 ⊆ 𝑇))
20	19	anbi2d 631	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑇 → ((𝜑 ∧ 𝑧 ⊆ 𝑇) ↔ (𝜑 ∧ 𝑇 ⊆ 𝑇)))
21	20	imbi1d 345	. . . . . . . . . 10 ⊢ (𝑧 = 𝑇 → (((𝜑 ∧ 𝑧 ⊆ 𝑇) → 𝜓) ↔ ((𝜑 ∧ 𝑇 ⊆ 𝑇) → 𝜓)))
22	18, 21	imbi12d 348	. . . . . . . . 9 ⊢ (𝑧 = 𝑇 → ((𝑅 = 𝑧 → ((𝜑 ∧ 𝑧 ⊆ 𝑇) → 𝜓)) ↔ (𝑅 = 𝑇 → ((𝜑 ∧ 𝑇 ⊆ 𝑇) → 𝜓))))
23	22	albidv 1921	. . . . . . . 8 ⊢ (𝑧 = 𝑇 → (∀𝑥(𝑅 = 𝑧 → ((𝜑 ∧ 𝑧 ⊆ 𝑇) → 𝜓)) ↔ ∀𝑥(𝑅 = 𝑇 → ((𝜑 ∧ 𝑇 ⊆ 𝑇) → 𝜓))))
24		simp3l 1198	. . . . . . . . . . . 12 ⊢ (((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) → 𝜑)
25		simp2 1134	. . . . . . . . . . . . 13 ⊢ (((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) → 𝑅 = 𝑧)
26		simp1l 1194	. . . . . . . . . . . . 13 ⊢ (((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) → 𝑧 ∈ On)
27	25, 26	eqeltrd 2890	. . . . . . . . . . . 12 ⊢ (((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) → 𝑅 ∈ On)
28		simp3r 1199	. . . . . . . . . . . . 13 ⊢ (((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) → 𝑧 ⊆ 𝑇)
29	25, 28	eqsstrd 3953	. . . . . . . . . . . 12 ⊢ (((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) → 𝑅 ⊆ 𝑇)
30		simpl3l 1225	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) ∧ ⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅) → 𝜑)
31		simpl1l 1221	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) ∧ ⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅) → 𝑧 ∈ On)
32		simpr 488	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) ∧ ⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅) → ⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅)
33		simpl2 1189	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) ∧ ⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅) → 𝑅 = 𝑧)
34	32, 33	eleqtrd 2892	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) ∧ ⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅) → ⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑧)
35		onelss 6201	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ On → (⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑧 → ⦋𝑣 / 𝑥⦌𝑅 ⊆ 𝑧))
36	31, 34, 35	sylc 65	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) ∧ ⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅) → ⦋𝑣 / 𝑥⦌𝑅 ⊆ 𝑧)
37		simpl3r 1226	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) ∧ ⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅) → 𝑧 ⊆ 𝑇)
38	36, 37	sstrd 3925	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) ∧ ⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅) → ⦋𝑣 / 𝑥⦌𝑅 ⊆ 𝑇)
39		eqeq2 2810	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = ⦋𝑣 / 𝑥⦌𝑅 → (𝑆 = 𝑤 ↔ 𝑆 = ⦋𝑣 / 𝑥⦌𝑅))
40		sseq1 3940	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 = ⦋𝑣 / 𝑥⦌𝑅 → (𝑤 ⊆ 𝑇 ↔ ⦋𝑣 / 𝑥⦌𝑅 ⊆ 𝑇))
41	40	anbi2d 631	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = ⦋𝑣 / 𝑥⦌𝑅 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) ↔ (𝜑 ∧ ⦋𝑣 / 𝑥⦌𝑅 ⊆ 𝑇)))
42	41	imbi1d 345	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = ⦋𝑣 / 𝑥⦌𝑅 → (((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒) ↔ ((𝜑 ∧ ⦋𝑣 / 𝑥⦌𝑅 ⊆ 𝑇) → 𝜒)))
43	39, 42	imbi12d 348	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = ⦋𝑣 / 𝑥⦌𝑅 → ((𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒)) ↔ (𝑆 = ⦋𝑣 / 𝑥⦌𝑅 → ((𝜑 ∧ ⦋𝑣 / 𝑥⦌𝑅 ⊆ 𝑇) → 𝜒))))
44	43	albidv 1921	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 = ⦋𝑣 / 𝑥⦌𝑅 → (∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒)) ↔ ∀𝑦(𝑆 = ⦋𝑣 / 𝑥⦌𝑅 → ((𝜑 ∧ ⦋𝑣 / 𝑥⦌𝑅 ⊆ 𝑇) → 𝜒))))
45		simpl1r 1222	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) ∧ ⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅) → ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒)))
46	44, 45, 34	rspcdva 3573	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) ∧ ⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅) → ∀𝑦(𝑆 = ⦋𝑣 / 𝑥⦌𝑅 → ((𝜑 ∧ ⦋𝑣 / 𝑥⦌𝑅 ⊆ 𝑇) → 𝜒)))
47		eqidd 2799	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) ∧ ⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅) → ⦋𝑣 / 𝑥⦌𝑅 = ⦋𝑣 / 𝑥⦌𝑅)
48		nfcv 2955	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑥𝑦
49		nfcv 2955	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑥𝑆
50	48, 49, 11	csbhypf 3856	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 = 𝑦 → ⦋𝑣 / 𝑥⦌𝑅 = 𝑆)
51	50	eqcomd 2804	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 = 𝑦 → 𝑆 = ⦋𝑣 / 𝑥⦌𝑅)
52	51	equcoms 2027	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑣 → 𝑆 = ⦋𝑣 / 𝑥⦌𝑅)
53	52	eqeq1d 2800	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑣 → (𝑆 = ⦋𝑣 / 𝑥⦌𝑅 ↔ ⦋𝑣 / 𝑥⦌𝑅 = ⦋𝑣 / 𝑥⦌𝑅))
54		nfv 1915	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑥𝜒
55	54, 13	sbhypf 3500	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 = 𝑦 → ([𝑣 / 𝑥]𝜓 ↔ 𝜒))
56	55	bicomd 226	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 = 𝑦 → (𝜒 ↔ [𝑣 / 𝑥]𝜓))
57	56	equcoms 2027	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑣 → (𝜒 ↔ [𝑣 / 𝑥]𝜓))
58	57	imbi2d 344	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑣 → (((𝜑 ∧ ⦋𝑣 / 𝑥⦌𝑅 ⊆ 𝑇) → 𝜒) ↔ ((𝜑 ∧ ⦋𝑣 / 𝑥⦌𝑅 ⊆ 𝑇) → [𝑣 / 𝑥]𝜓)))
59	53, 58	imbi12d 348	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑣 → ((𝑆 = ⦋𝑣 / 𝑥⦌𝑅 → ((𝜑 ∧ ⦋𝑣 / 𝑥⦌𝑅 ⊆ 𝑇) → 𝜒)) ↔ (⦋𝑣 / 𝑥⦌𝑅 = ⦋𝑣 / 𝑥⦌𝑅 → ((𝜑 ∧ ⦋𝑣 / 𝑥⦌𝑅 ⊆ 𝑇) → [𝑣 / 𝑥]𝜓))))
60	59	spvv 2003	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑦(𝑆 = ⦋𝑣 / 𝑥⦌𝑅 → ((𝜑 ∧ ⦋𝑣 / 𝑥⦌𝑅 ⊆ 𝑇) → 𝜒)) → (⦋𝑣 / 𝑥⦌𝑅 = ⦋𝑣 / 𝑥⦌𝑅 → ((𝜑 ∧ ⦋𝑣 / 𝑥⦌𝑅 ⊆ 𝑇) → [𝑣 / 𝑥]𝜓)))
61	46, 47, 60	sylc 65	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) ∧ ⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅) → ((𝜑 ∧ ⦋𝑣 / 𝑥⦌𝑅 ⊆ 𝑇) → [𝑣 / 𝑥]𝜓))
62	30, 38, 61	mp2and 698	. . . . . . . . . . . . . . 15 ⊢ ((((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) ∧ ⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅) → [𝑣 / 𝑥]𝜓)
63	62	ex 416	. . . . . . . . . . . . . 14 ⊢ (((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) → (⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅 → [𝑣 / 𝑥]𝜓))
64	63	alrimiv 1928	. . . . . . . . . . . . 13 ⊢ (((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) → ∀𝑣(⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅 → [𝑣 / 𝑥]𝜓))
65	50	eleq1d 2874	. . . . . . . . . . . . . . 15 ⊢ (𝑣 = 𝑦 → (⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅 ↔ 𝑆 ∈ 𝑅))
66	65, 55	imbi12d 348	. . . . . . . . . . . . . 14 ⊢ (𝑣 = 𝑦 → ((⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅 → [𝑣 / 𝑥]𝜓) ↔ (𝑆 ∈ 𝑅 → 𝜒)))
67	66	cbvalvw 2043	. . . . . . . . . . . . 13 ⊢ (∀𝑣(⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅 → [𝑣 / 𝑥]𝜓) ↔ ∀𝑦(𝑆 ∈ 𝑅 → 𝜒))
68	64, 67	sylib 221	. . . . . . . . . . . 12 ⊢ (((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) → ∀𝑦(𝑆 ∈ 𝑅 → 𝜒))
69		tfisi.c	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑅 ∈ On ∧ 𝑅 ⊆ 𝑇) ∧ ∀𝑦(𝑆 ∈ 𝑅 → 𝜒)) → 𝜓)
70	24, 27, 29, 68, 69	syl121anc 1372	. . . . . . . . . . 11 ⊢ (((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) → 𝜓)
71	70	3exp 1116	. . . . . . . . . 10 ⊢ ((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) → (𝑅 = 𝑧 → ((𝜑 ∧ 𝑧 ⊆ 𝑇) → 𝜓)))
72	71	alrimiv 1928	. . . . . . . . 9 ⊢ ((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) → ∀𝑥(𝑅 = 𝑧 → ((𝜑 ∧ 𝑧 ⊆ 𝑇) → 𝜓)))
73	72	ex 416	. . . . . . . 8 ⊢ (𝑧 ∈ On → (∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒)) → ∀𝑥(𝑅 = 𝑧 → ((𝜑 ∧ 𝑧 ⊆ 𝑇) → 𝜓))))
74	17, 23, 73	tfis3 7552	. . . . . . 7 ⊢ (𝑇 ∈ On → ∀𝑥(𝑅 = 𝑇 → ((𝜑 ∧ 𝑇 ⊆ 𝑇) → 𝜓)))
75	4, 74	syl 17	. . . . . 6 ⊢ (𝜑 → ∀𝑥(𝑅 = 𝑇 → ((𝜑 ∧ 𝑇 ⊆ 𝑇) → 𝜓)))
76		tfisi.g	. . . . . . . . 9 ⊢ (𝑥 = 𝐴 → 𝑅 = 𝑇)
77	76	eqeq1d 2800	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → (𝑅 = 𝑇 ↔ 𝑇 = 𝑇))
78		tfisi.e	. . . . . . . . 9 ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃))
79	78	imbi2d 344	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → (((𝜑 ∧ 𝑇 ⊆ 𝑇) → 𝜓) ↔ ((𝜑 ∧ 𝑇 ⊆ 𝑇) → 𝜃)))
80	77, 79	imbi12d 348	. . . . . . 7 ⊢ (𝑥 = 𝐴 → ((𝑅 = 𝑇 → ((𝜑 ∧ 𝑇 ⊆ 𝑇) → 𝜓)) ↔ (𝑇 = 𝑇 → ((𝜑 ∧ 𝑇 ⊆ 𝑇) → 𝜃))))
81	80	spcgv 3543	. . . . . 6 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑅 = 𝑇 → ((𝜑 ∧ 𝑇 ⊆ 𝑇) → 𝜓)) → (𝑇 = 𝑇 → ((𝜑 ∧ 𝑇 ⊆ 𝑇) → 𝜃))))
82	3, 75, 81	sylc 65	. . . . 5 ⊢ (𝜑 → (𝑇 = 𝑇 → ((𝜑 ∧ 𝑇 ⊆ 𝑇) → 𝜃)))
83	2, 82	mpi 20	. . . 4 ⊢ (𝜑 → ((𝜑 ∧ 𝑇 ⊆ 𝑇) → 𝜃))
84	83	expd 419	. . 3 ⊢ (𝜑 → (𝜑 → (𝑇 ⊆ 𝑇 → 𝜃)))
85	84	pm2.43i 52	. 2 ⊢ (𝜑 → (𝑇 ⊆ 𝑇 → 𝜃))
86	1, 85	mpi 20	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084  ∀wal 1536   = wceq 1538  [wsb 2069   ∈ wcel 2111  ∀wral 3106  ⦋csb 3828   ⊆ wss 3881  Oncon0 6159

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pr 5295  ax-un 7441

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4801  df-br 5031  df-opab 5093  df-tr 5137  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-we 5480  df-ord 6162  df-on 6163

This theorem is referenced by:  indcardi  9452