Theorem tfisi 4439

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 3067	. 2 ⊢ 𝑇 ⊆ 𝑇
2		eqid 2100	. . . . 5 ⊢ 𝑇 = 𝑇
3		tfisi.a	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
4		tfisi.b	. . . . . . 7 ⊢ (𝜑 → 𝑇 ∈ On)
5		eqeq2 2109	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑤 → (𝑅 = 𝑧 ↔ 𝑅 = 𝑤))
6		sseq1 3070	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑤 → (𝑧 ⊆ 𝑇 ↔ 𝑤 ⊆ 𝑇))
7	6	anbi2d 455	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑤 → ((𝜑 ∧ 𝑧 ⊆ 𝑇) ↔ (𝜑 ∧ 𝑤 ⊆ 𝑇)))
8	7	imbi1d 230	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑤 → (((𝜑 ∧ 𝑧 ⊆ 𝑇) → 𝜓) ↔ ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜓)))
9	5, 8	imbi12d 233	. . . . . . . . . 10 ⊢ (𝑧 = 𝑤 → ((𝑅 = 𝑧 → ((𝜑 ∧ 𝑧 ⊆ 𝑇) → 𝜓)) ↔ (𝑅 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜓))))
10	9	albidv 1763	. . . . . . . . 9 ⊢ (𝑧 = 𝑤 → (∀𝑥(𝑅 = 𝑧 → ((𝜑 ∧ 𝑧 ⊆ 𝑇) → 𝜓)) ↔ ∀𝑥(𝑅 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜓))))
11		tfisi.f	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → 𝑅 = 𝑆)
12	11	eqeq1d 2108	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (𝑅 = 𝑤 ↔ 𝑆 = 𝑤))
13		tfisi.d	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))
14	13	imbi2d 229	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜓) ↔ ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒)))
15	12, 14	imbi12d 233	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → ((𝑅 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜓)) ↔ (𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))))
16	15	cbvalv 1854	. . . . . . . . 9 ⊢ (∀𝑥(𝑅 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜓)) ↔ ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒)))
17	10, 16	syl6bb 195	. . . . . . . 8 ⊢ (𝑧 = 𝑤 → (∀𝑥(𝑅 = 𝑧 → ((𝜑 ∧ 𝑧 ⊆ 𝑇) → 𝜓)) ↔ ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))))
18		eqeq2 2109	. . . . . . . . . 10 ⊢ (𝑧 = 𝑇 → (𝑅 = 𝑧 ↔ 𝑅 = 𝑇))
19		sseq1 3070	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑇 → (𝑧 ⊆ 𝑇 ↔ 𝑇 ⊆ 𝑇))
20	19	anbi2d 455	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑇 → ((𝜑 ∧ 𝑧 ⊆ 𝑇) ↔ (𝜑 ∧ 𝑇 ⊆ 𝑇)))
21	20	imbi1d 230	. . . . . . . . . 10 ⊢ (𝑧 = 𝑇 → (((𝜑 ∧ 𝑧 ⊆ 𝑇) → 𝜓) ↔ ((𝜑 ∧ 𝑇 ⊆ 𝑇) → 𝜓)))
22	18, 21	imbi12d 233	. . . . . . . . 9 ⊢ (𝑧 = 𝑇 → ((𝑅 = 𝑧 → ((𝜑 ∧ 𝑧 ⊆ 𝑇) → 𝜓)) ↔ (𝑅 = 𝑇 → ((𝜑 ∧ 𝑇 ⊆ 𝑇) → 𝜓))))
23	22	albidv 1763	. . . . . . . 8 ⊢ (𝑧 = 𝑇 → (∀𝑥(𝑅 = 𝑧 → ((𝜑 ∧ 𝑧 ⊆ 𝑇) → 𝜓)) ↔ ∀𝑥(𝑅 = 𝑇 → ((𝜑 ∧ 𝑇 ⊆ 𝑇) → 𝜓))))
24		simp3l 977	. . . . . . . . . . . 12 ⊢ (((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) → 𝜑)
25		simp2 950	. . . . . . . . . . . . 13 ⊢ (((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) → 𝑅 = 𝑧)
26		simp1l 973	. . . . . . . . . . . . 13 ⊢ (((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) → 𝑧 ∈ On)
27	25, 26	eqeltrd 2176	. . . . . . . . . . . 12 ⊢ (((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) → 𝑅 ∈ On)
28		simp3r 978	. . . . . . . . . . . . 13 ⊢ (((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) → 𝑧 ⊆ 𝑇)
29	25, 28	eqsstrd 3083	. . . . . . . . . . . 12 ⊢ (((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) → 𝑅 ⊆ 𝑇)
30		simpl3l 1004	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) ∧ ⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅) → 𝜑)
31		simpl1l 1000	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) ∧ ⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅) → 𝑧 ∈ On)
32		simpr 109	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) ∧ ⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅) → ⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅)
33		simpl2 953	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) ∧ ⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅) → 𝑅 = 𝑧)
34	32, 33	eleqtrd 2178	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) ∧ ⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅) → ⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑧)
35		onelss 4247	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ On → (⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑧 → ⦋𝑣 / 𝑥⦌𝑅 ⊆ 𝑧))
36	31, 34, 35	sylc 62	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) ∧ ⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅) → ⦋𝑣 / 𝑥⦌𝑅 ⊆ 𝑧)
37		simpl3r 1005	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) ∧ ⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅) → 𝑧 ⊆ 𝑇)
38	36, 37	sstrd 3057	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) ∧ ⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅) → ⦋𝑣 / 𝑥⦌𝑅 ⊆ 𝑇)
39		eqeq2 2109	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = ⦋𝑣 / 𝑥⦌𝑅 → (𝑆 = 𝑤 ↔ 𝑆 = ⦋𝑣 / 𝑥⦌𝑅))
40		sseq1 3070	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 = ⦋𝑣 / 𝑥⦌𝑅 → (𝑤 ⊆ 𝑇 ↔ ⦋𝑣 / 𝑥⦌𝑅 ⊆ 𝑇))
41	40	anbi2d 455	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = ⦋𝑣 / 𝑥⦌𝑅 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) ↔ (𝜑 ∧ ⦋𝑣 / 𝑥⦌𝑅 ⊆ 𝑇)))
42	41	imbi1d 230	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = ⦋𝑣 / 𝑥⦌𝑅 → (((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒) ↔ ((𝜑 ∧ ⦋𝑣 / 𝑥⦌𝑅 ⊆ 𝑇) → 𝜒)))
43	39, 42	imbi12d 233	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = ⦋𝑣 / 𝑥⦌𝑅 → ((𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒)) ↔ (𝑆 = ⦋𝑣 / 𝑥⦌𝑅 → ((𝜑 ∧ ⦋𝑣 / 𝑥⦌𝑅 ⊆ 𝑇) → 𝜒))))
44	43	albidv 1763	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 = ⦋𝑣 / 𝑥⦌𝑅 → (∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒)) ↔ ∀𝑦(𝑆 = ⦋𝑣 / 𝑥⦌𝑅 → ((𝜑 ∧ ⦋𝑣 / 𝑥⦌𝑅 ⊆ 𝑇) → 𝜒))))
45		simpl1r 1001	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) ∧ ⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅) → ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒)))
46	44, 45, 34	rspcdva 2749	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) ∧ ⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅) → ∀𝑦(𝑆 = ⦋𝑣 / 𝑥⦌𝑅 → ((𝜑 ∧ ⦋𝑣 / 𝑥⦌𝑅 ⊆ 𝑇) → 𝜒)))
47		eqidd 2101	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) ∧ ⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅) → ⦋𝑣 / 𝑥⦌𝑅 = ⦋𝑣 / 𝑥⦌𝑅)
48		nfcv 2240	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑥𝑦
49		nfcv 2240	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑥𝑆
50	48, 49, 11	csbhypf 2988	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 = 𝑦 → ⦋𝑣 / 𝑥⦌𝑅 = 𝑆)
51	50	eqcomd 2105	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 = 𝑦 → 𝑆 = ⦋𝑣 / 𝑥⦌𝑅)
52	51	equcoms 1652	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑣 → 𝑆 = ⦋𝑣 / 𝑥⦌𝑅)
53	52	eqeq1d 2108	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑣 → (𝑆 = ⦋𝑣 / 𝑥⦌𝑅 ↔ ⦋𝑣 / 𝑥⦌𝑅 = ⦋𝑣 / 𝑥⦌𝑅))
54		nfv 1476	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑥𝜒
55	54, 13	sbhypf 2690	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 = 𝑦 → ([𝑣 / 𝑥]𝜓 ↔ 𝜒))
56	55	bicomd 140	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 = 𝑦 → (𝜒 ↔ [𝑣 / 𝑥]𝜓))
57	56	equcoms 1652	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑣 → (𝜒 ↔ [𝑣 / 𝑥]𝜓))
58	57	imbi2d 229	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑣 → (((𝜑 ∧ ⦋𝑣 / 𝑥⦌𝑅 ⊆ 𝑇) → 𝜒) ↔ ((𝜑 ∧ ⦋𝑣 / 𝑥⦌𝑅 ⊆ 𝑇) → [𝑣 / 𝑥]𝜓)))
59	53, 58	imbi12d 233	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑣 → ((𝑆 = ⦋𝑣 / 𝑥⦌𝑅 → ((𝜑 ∧ ⦋𝑣 / 𝑥⦌𝑅 ⊆ 𝑇) → 𝜒)) ↔ (⦋𝑣 / 𝑥⦌𝑅 = ⦋𝑣 / 𝑥⦌𝑅 → ((𝜑 ∧ ⦋𝑣 / 𝑥⦌𝑅 ⊆ 𝑇) → [𝑣 / 𝑥]𝜓))))
60	59	spv 1799	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑦(𝑆 = ⦋𝑣 / 𝑥⦌𝑅 → ((𝜑 ∧ ⦋𝑣 / 𝑥⦌𝑅 ⊆ 𝑇) → 𝜒)) → (⦋𝑣 / 𝑥⦌𝑅 = ⦋𝑣 / 𝑥⦌𝑅 → ((𝜑 ∧ ⦋𝑣 / 𝑥⦌𝑅 ⊆ 𝑇) → [𝑣 / 𝑥]𝜓)))
61	46, 47, 60	sylc 62	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) ∧ ⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅) → ((𝜑 ∧ ⦋𝑣 / 𝑥⦌𝑅 ⊆ 𝑇) → [𝑣 / 𝑥]𝜓))
62	30, 38, 61	mp2and 427	. . . . . . . . . . . . . . 15 ⊢ ((((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) ∧ ⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅) → [𝑣 / 𝑥]𝜓)
63	62	ex 114	. . . . . . . . . . . . . 14 ⊢ (((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) → (⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅 → [𝑣 / 𝑥]𝜓))
64	63	alrimiv 1813	. . . . . . . . . . . . 13 ⊢ (((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) → ∀𝑣(⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅 → [𝑣 / 𝑥]𝜓))
65	50	eleq1d 2168	. . . . . . . . . . . . . . 15 ⊢ (𝑣 = 𝑦 → (⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅 ↔ 𝑆 ∈ 𝑅))
66	65, 55	imbi12d 233	. . . . . . . . . . . . . 14 ⊢ (𝑣 = 𝑦 → ((⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅 → [𝑣 / 𝑥]𝜓) ↔ (𝑆 ∈ 𝑅 → 𝜒)))
67	66	cbvalv 1854	. . . . . . . . . . . . 13 ⊢ (∀𝑣(⦋𝑣 / 𝑥⦌𝑅 ∈ 𝑅 → [𝑣 / 𝑥]𝜓) ↔ ∀𝑦(𝑆 ∈ 𝑅 → 𝜒))
68	64, 67	sylib 121	. . . . . . . . . . . 12 ⊢ (((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) → ∀𝑦(𝑆 ∈ 𝑅 → 𝜒))
69		tfisi.c	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑅 ∈ On ∧ 𝑅 ⊆ 𝑇) ∧ ∀𝑦(𝑆 ∈ 𝑅 → 𝜒)) → 𝜓)
70	24, 27, 29, 68, 69	syl121anc 1189	. . . . . . . . . . 11 ⊢ (((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) ∧ 𝑅 = 𝑧 ∧ (𝜑 ∧ 𝑧 ⊆ 𝑇)) → 𝜓)
71	70	3exp 1148	. . . . . . . . . 10 ⊢ ((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) → (𝑅 = 𝑧 → ((𝜑 ∧ 𝑧 ⊆ 𝑇) → 𝜓)))
72	71	alrimiv 1813	. . . . . . . . 9 ⊢ ((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒))) → ∀𝑥(𝑅 = 𝑧 → ((𝜑 ∧ 𝑧 ⊆ 𝑇) → 𝜓)))
73	72	ex 114	. . . . . . . 8 ⊢ (𝑧 ∈ On → (∀𝑤 ∈ 𝑧 ∀𝑦(𝑆 = 𝑤 → ((𝜑 ∧ 𝑤 ⊆ 𝑇) → 𝜒)) → ∀𝑥(𝑅 = 𝑧 → ((𝜑 ∧ 𝑧 ⊆ 𝑇) → 𝜓))))
74	17, 23, 73	tfis3 4438	. . . . . . 7 ⊢ (𝑇 ∈ On → ∀𝑥(𝑅 = 𝑇 → ((𝜑 ∧ 𝑇 ⊆ 𝑇) → 𝜓)))
75	4, 74	syl 14	. . . . . 6 ⊢ (𝜑 → ∀𝑥(𝑅 = 𝑇 → ((𝜑 ∧ 𝑇 ⊆ 𝑇) → 𝜓)))
76		tfisi.g	. . . . . . . . 9 ⊢ (𝑥 = 𝐴 → 𝑅 = 𝑇)
77	76	eqeq1d 2108	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → (𝑅 = 𝑇 ↔ 𝑇 = 𝑇))
78		tfisi.e	. . . . . . . . 9 ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃))
79	78	imbi2d 229	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → (((𝜑 ∧ 𝑇 ⊆ 𝑇) → 𝜓) ↔ ((𝜑 ∧ 𝑇 ⊆ 𝑇) → 𝜃)))
80	77, 79	imbi12d 233	. . . . . . 7 ⊢ (𝑥 = 𝐴 → ((𝑅 = 𝑇 → ((𝜑 ∧ 𝑇 ⊆ 𝑇) → 𝜓)) ↔ (𝑇 = 𝑇 → ((𝜑 ∧ 𝑇 ⊆ 𝑇) → 𝜃))))
81	80	spcgv 2728	. . . . . 6 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑅 = 𝑇 → ((𝜑 ∧ 𝑇 ⊆ 𝑇) → 𝜓)) → (𝑇 = 𝑇 → ((𝜑 ∧ 𝑇 ⊆ 𝑇) → 𝜃))))
82	3, 75, 81	sylc 62	. . . . 5 ⊢ (𝜑 → (𝑇 = 𝑇 → ((𝜑 ∧ 𝑇 ⊆ 𝑇) → 𝜃)))
83	2, 82	mpi 15	. . . 4 ⊢ (𝜑 → ((𝜑 ∧ 𝑇 ⊆ 𝑇) → 𝜃))
84	83	expd 256	. . 3 ⊢ (𝜑 → (𝜑 → (𝑇 ⊆ 𝑇 → 𝜃)))
85	84	pm2.43i 49	. 2 ⊢ (𝜑 → (𝑇 ⊆ 𝑇 → 𝜃))
86	1, 85	mpi 15	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   ∧ w3a 930  ∀wal 1297   = wceq 1299   ∈ wcel 1448  [wsb 1703  ∀wral 2375  ⦋csb 2955   ⊆ wss 3021  Oncon0 4223

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 671  ax-5 1391  ax-7 1392  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-8 1450  ax-10 1451  ax-11 1452  ax-i12 1453  ax-bndl 1454  ax-4 1455  ax-17 1474  ax-i9 1478  ax-ial 1482  ax-i5r 1483  ax-ext 2082  ax-setind 4390

This theorem depends on definitions:  df-bi 116  df-3an 932  df-tru 1302  df-nf 1405  df-sb 1704  df-clab 2087  df-cleq 2093  df-clel 2096  df-nfc 2229  df-ral 2380  df-rex 2381  df-rab 2384  df-v 2643  df-sbc 2863  df-csb 2956  df-in 3027  df-ss 3034  df-uni 3684  df-tr 3967  df-iord 4226  df-on 4228

This theorem is referenced by: (None)