Theorem tfisi 4253

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	|- (ph -> A e. V)
tfisi.b	|- (ph -> T e. On)
tfisi.c	|- ((ph /\ ( R e. On /\ R C_ T) /\ A.y( S e. R -> ch)) -> ps)
tfisi.d	|- (x = y -> (ps <-> ch))
tfisi.e	|- (x = A -> (ps <-> th))
tfisi.f	|- (x = y -> R = S)
tfisi.g	|- (x = A -> R = T)

Assertion

Ref	Expression
tfisi	|- (ph -> th)

Distinct variable groups:   x,y, T   y, R   x, S   ch,x   ph,x,y   ps,y   x,A   th,x

Allowed substitution hints:   ps(x)   ch(y)   th(y)   A(y)   R(x)   S(y)   V(x,y)

Proof of Theorem tfisi

Dummy variables v w z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ssid 2958	. 2 |- T C_ T
2		eqid 2037	. . . . 5 |- T = T
3		tfisi.a	. . . . . 6 |- (ph -> A e. V)
4		tfisi.b	. . . . . . 7 |- (ph -> T e. On)
5		eqeq2 2046	. . . . . . . . . . 11 |- (z = w -> ( R = z <-> R = w))
6		sseq1 2960	. . . . . . . . . . . . 13 |- (z = w -> (z C_ T <-> w C_ T))
7	6	anbi2d 437	. . . . . . . . . . . 12 |- (z = w -> ((ph /\ z C_ T) <-> (ph /\ w C_ T)))
8	7	imbi1d 220	. . . . . . . . . . 11 |- (z = w -> (((ph /\ z C_ T) -> ps) <-> ((ph /\ w C_ T) -> ps)))
9	5, 8	imbi12d 223	. . . . . . . . . 10 |- (z = w -> (( R = z -> ((ph /\ z C_ T) -> ps)) <-> ( R = w -> ((ph /\ w C_ T) -> ps))))
10	9	albidv 1702	. . . . . . . . 9 |- (z = w -> (A.x( R = z -> ((ph /\ z C_ T) -> ps)) <-> A.x( R = w -> ((ph /\ w C_ T) -> ps))))
11		tfisi.f	. . . . . . . . . . . 12 |- (x = y -> R = S)
12	11	eqeq1d 2045	. . . . . . . . . . 11 |- (x = y -> ( R = w <-> S = w))
13		tfisi.d	. . . . . . . . . . . 12 |- (x = y -> (ps <-> ch))
14	13	imbi2d 219	. . . . . . . . . . 11 |- (x = y -> (((ph /\ w C_ T) -> ps) <-> ((ph /\ w C_ T) -> ch)))
15	12, 14	imbi12d 223	. . . . . . . . . 10 |- (x = y -> (( R = w -> ((ph /\ w C_ T) -> ps)) <-> ( S = w -> ((ph /\ w C_ T) -> ch))))
16	15	cbvalv 1791	. . . . . . . . 9 |- (A.x( R = w -> ((ph /\ w C_ T) -> ps)) <-> A.y( S = w -> ((ph /\ w C_ T) -> ch)))
17	10, 16	syl6bb 185	. . . . . . . 8 |- (z = w -> (A.x( R = z -> ((ph /\ z C_ T) -> ps)) <-> A.y( S = w -> ((ph /\ w C_ T) -> ch))))
18		eqeq2 2046	. . . . . . . . . 10 |- (z = T -> ( R = z <-> R = T))
19		sseq1 2960	. . . . . . . . . . . 12 |- (z = T -> (z C_ T <-> T C_ T))
20	19	anbi2d 437	. . . . . . . . . . 11 |- (z = T -> ((ph /\ z C_ T) <-> (ph /\ T C_ T)))
21	20	imbi1d 220	. . . . . . . . . 10 |- (z = T -> (((ph /\ z C_ T) -> ps) <-> ((ph /\ T C_ T) -> ps)))
22	18, 21	imbi12d 223	. . . . . . . . 9 |- (z = T -> (( R = z -> ((ph /\ z C_ T) -> ps)) <-> ( R = T -> ((ph /\ T C_ T) -> ps))))
23	22	albidv 1702	. . . . . . . 8 |- (z = T -> (A.x( R = z -> ((ph /\ z C_ T) -> ps)) <-> A.x( R = T -> ((ph /\ T C_ T) -> ps))))
24		simp3l 931	. . . . . . . . . . . 12 |- (((z e. On /\ A.w e. z A.y( S = w -> ((ph /\ w C_ T) -> ch))) /\ R = z /\ (ph /\ z C_ T)) -> ph)
25		simp2 904	. . . . . . . . . . . . 13 |- (((z e. On /\ A.w e. z A.y( S = w -> ((ph /\ w C_ T) -> ch))) /\ R = z /\ (ph /\ z C_ T)) -> R = z)
26		simp1l 927	. . . . . . . . . . . . 13 |- (((z e. On /\ A.w e. z A.y( S = w -> ((ph /\ w C_ T) -> ch))) /\ R = z /\ (ph /\ z C_ T)) -> z e. On)
27	25, 26	eqeltrd 2111	. . . . . . . . . . . 12 |- (((z e. On /\ A.w e. z A.y( S = w -> ((ph /\ w C_ T) -> ch))) /\ R = z /\ (ph /\ z C_ T)) -> R e. On)
28		simp3r 932	. . . . . . . . . . . . 13 |- (((z e. On /\ A.w e. z A.y( S = w -> ((ph /\ w C_ T) -> ch))) /\ R = z /\ (ph /\ z C_ T)) -> z C_ T)
29	25, 28	eqsstrd 2973	. . . . . . . . . . . 12 |- (((z e. On /\ A.w e. z A.y( S = w -> ((ph /\ w C_ T) -> ch))) /\ R = z /\ (ph /\ z C_ T)) -> R C_ T)
30		simpl3l 958	. . . . . . . . . . . . . . . 16 |- ((((z e. On /\ A.w e. z A.y( S = w -> ((ph /\ w C_ T) -> ch))) /\ R = z /\ (ph /\ z C_ T)) /\ [_v / x ]_ R e. R) -> ph)
31		simpl1l 954	. . . . . . . . . . . . . . . . . 18 |- ((((z e. On /\ A.w e. z A.y( S = w -> ((ph /\ w C_ T) -> ch))) /\ R = z /\ (ph /\ z C_ T)) /\ [_v / x ]_ R e. R) -> z e. On)
32		simpr 103	. . . . . . . . . . . . . . . . . . 19 |- ((((z e. On /\ A.w e. z A.y( S = w -> ((ph /\ w C_ T) -> ch))) /\ R = z /\ (ph /\ z C_ T)) /\ [_v / x ]_ R e. R) -> [_v / x ]_ R e. R)
33		simpl2 907	. . . . . . . . . . . . . . . . . . 19 |- ((((z e. On /\ A.w e. z A.y( S = w -> ((ph /\ w C_ T) -> ch))) /\ R = z /\ (ph /\ z C_ T)) /\ [_v / x ]_ R e. R) -> R = z)
34	32, 33	eleqtrd 2113	. . . . . . . . . . . . . . . . . 18 |- ((((z e. On /\ A.w e. z A.y( S = w -> ((ph /\ w C_ T) -> ch))) /\ R = z /\ (ph /\ z C_ T)) /\ [_v / x ]_ R e. R) -> [_v / x ]_ R e. z)
35		onelss 4090	. . . . . . . . . . . . . . . . . 18 |- (z e. On -> ( [_v / x ]_ R e. z -> [_v / x ]_ R C_ z))
36	31, 34, 35	sylc 56	. . . . . . . . . . . . . . . . 17 |- ((((z e. On /\ A.w e. z A.y( S = w -> ((ph /\ w C_ T) -> ch))) /\ R = z /\ (ph /\ z C_ T)) /\ [_v / x ]_ R e. R) -> [_v / x ]_ R C_ z)
37		simpl3r 959	. . . . . . . . . . . . . . . . 17 |- ((((z e. On /\ A.w e. z A.y( S = w -> ((ph /\ w C_ T) -> ch))) /\ R = z /\ (ph /\ z C_ T)) /\ [_v / x ]_ R e. R) -> z C_ T)
38	36, 37	sstrd 2949	. . . . . . . . . . . . . . . 16 |- ((((z e. On /\ A.w e. z A.y( S = w -> ((ph /\ w C_ T) -> ch))) /\ R = z /\ (ph /\ z C_ T)) /\ [_v / x ]_ R e. R) -> [_v / x ]_ R C_ T)
39		simpl1r 955	. . . . . . . . . . . . . . . . . 18 |- ((((z e. On /\ A.w e. z A.y( S = w -> ((ph /\ w C_ T) -> ch))) /\ R = z /\ (ph /\ z C_ T)) /\ [_v / x ]_ R e. R) -> A.w e. z A.y( S = w -> ((ph /\ w C_ T) -> ch)))
40		eqeq2 2046	. . . . . . . . . . . . . . . . . . . . 21 |- (w = [_v / x ]_ R -> ( S = w <-> S = [_v / x ]_ R))
41		sseq1 2960	. . . . . . . . . . . . . . . . . . . . . . 23 |- (w = [_v / x ]_ R -> (w C_ T <-> [_v / x ]_ R C_ T))
42	41	anbi2d 437	. . . . . . . . . . . . . . . . . . . . . 22 |- (w = [_v / x ]_ R -> ((ph /\ w C_ T) <-> (ph /\ [_v / x ]_ R C_ T)))
43	42	imbi1d 220	. . . . . . . . . . . . . . . . . . . . 21 |- (w = [_v / x ]_ R -> (((ph /\ w C_ T) -> ch) <-> ((ph /\ [_v / x ]_ R C_ T) -> ch)))
44	40, 43	imbi12d 223	. . . . . . . . . . . . . . . . . . . 20 |- (w = [_v / x ]_ R -> (( S = w -> ((ph /\ w C_ T) -> ch)) <-> ( S = [_v / x ]_ R -> ((ph /\ [_v / x ]_ R C_ T) -> ch))))
45	44	albidv 1702	. . . . . . . . . . . . . . . . . . 19 |- (w = [_v / x ]_ R -> (A.y( S = w -> ((ph /\ w C_ T) -> ch)) <-> A.y( S = [_v / x ]_ R -> ((ph /\ [_v / x ]_ R C_ T) -> ch))))
46	45	rspcva 2648	. . . . . . . . . . . . . . . . . 18 |- (( [_v / x ]_ R e. z /\ A.w e. z A.y( S = w -> ((ph /\ w C_ T) -> ch))) -> A.y( S = [_v / x ]_ R -> ((ph /\ [_v / x ]_ R C_ T) -> ch)))
47	34, 39, 46	syl2anc 391	. . . . . . . . . . . . . . . . 17 |- ((((z e. On /\ A.w e. z A.y( S = w -> ((ph /\ w C_ T) -> ch))) /\ R = z /\ (ph /\ z C_ T)) /\ [_v / x ]_ R e. R) -> A.y( S = [_v / x ]_ R -> ((ph /\ [_v / x ]_ R C_ T) -> ch)))
48		eqidd 2038	. . . . . . . . . . . . . . . . 17 |- ((((z e. On /\ A.w e. z A.y( S = w -> ((ph /\ w C_ T) -> ch))) /\ R = z /\ (ph /\ z C_ T)) /\ [_v / x ]_ R e. R) -> [_v / x ]_ R = [_v / x ]_ R)
49		nfcv 2175	. . . . . . . . . . . . . . . . . . . . . . 23 |- F/_xy
50		nfcv 2175	. . . . . . . . . . . . . . . . . . . . . . 23 |- F/_x S
51	49, 50, 11	csbhypf 2879	. . . . . . . . . . . . . . . . . . . . . 22 |- (v = y -> [_v / x ]_ R = S)
52	51	eqcomd 2042	. . . . . . . . . . . . . . . . . . . . 21 |- (v = y -> S = [_v / x ]_ R)
53	52	equcoms 1591	. . . . . . . . . . . . . . . . . . . 20 |- (y = v -> S = [_v / x ]_ R)
54	53	eqeq1d 2045	. . . . . . . . . . . . . . . . . . 19 |- (y = v -> ( S = [_v / x ]_ R <-> [_v / x ]_ R = [_v / x ]_ R))
55		nfv 1418	. . . . . . . . . . . . . . . . . . . . . . 23 |- F/xch
56	55, 13	sbhypf 2597	. . . . . . . . . . . . . . . . . . . . . 22 |- (v = y -> ([v / x]ps <-> ch))
57	56	bicomd 129	. . . . . . . . . . . . . . . . . . . . 21 |- (v = y -> (ch <-> [v / x]ps))
58	57	equcoms 1591	. . . . . . . . . . . . . . . . . . . 20 |- (y = v -> (ch <-> [v / x]ps))
59	58	imbi2d 219	. . . . . . . . . . . . . . . . . . 19 |- (y = v -> (((ph /\ [_v / x ]_ R C_ T) -> ch) <-> ((ph /\ [_v / x ]_ R C_ T) -> [v / x]ps)))
60	54, 59	imbi12d 223	. . . . . . . . . . . . . . . . . 18 |- (y = v -> (( S = [_v / x ]_ R -> ((ph /\ [_v / x ]_ R C_ T) -> ch)) <-> ( [_v / x ]_ R = [_v / x ]_ R -> ((ph /\ [_v / x ]_ R C_ T) -> [v / x]ps))))
61	60	spv 1737	. . . . . . . . . . . . . . . . 17 |- (A.y( S = [_v / x ]_ R -> ((ph /\ [_v / x ]_ R C_ T) -> ch)) -> ( [_v / x ]_ R = [_v / x ]_ R -> ((ph /\ [_v / x ]_ R C_ T) -> [v / x]ps)))
62	47, 48, 61	sylc 56	. . . . . . . . . . . . . . . 16 |- ((((z e. On /\ A.w e. z A.y( S = w -> ((ph /\ w C_ T) -> ch))) /\ R = z /\ (ph /\ z C_ T)) /\ [_v / x ]_ R e. R) -> ((ph /\ [_v / x ]_ R C_ T) -> [v / x]ps))
63	30, 38, 62	mp2and 409	. . . . . . . . . . . . . . 15 |- ((((z e. On /\ A.w e. z A.y( S = w -> ((ph /\ w C_ T) -> ch))) /\ R = z /\ (ph /\ z C_ T)) /\ [_v / x ]_ R e. R) -> [v / x]ps)
64	63	ex 108	. . . . . . . . . . . . . 14 |- (((z e. On /\ A.w e. z A.y( S = w -> ((ph /\ w C_ T) -> ch))) /\ R = z /\ (ph /\ z C_ T)) -> ( [_v / x ]_ R e. R -> [v / x]ps))
65	64	alrimiv 1751	. . . . . . . . . . . . 13 |- (((z e. On /\ A.w e. z A.y( S = w -> ((ph /\ w C_ T) -> ch))) /\ R = z /\ (ph /\ z C_ T)) -> A.v( [_v / x ]_ R e. R -> [v / x]ps))
66	51	eleq1d 2103	. . . . . . . . . . . . . . 15 |- (v = y -> ( [_v / x ]_ R e. R <-> S e. R))
67	66, 56	imbi12d 223	. . . . . . . . . . . . . 14 |- (v = y -> (( [_v / x ]_ R e. R -> [v / x]ps) <-> ( S e. R -> ch)))
68	67	cbvalv 1791	. . . . . . . . . . . . 13 |- (A.v( [_v / x ]_ R e. R -> [v / x]ps) <-> A.y( S e. R -> ch))
69	65, 68	sylib 127	. . . . . . . . . . . 12 |- (((z e. On /\ A.w e. z A.y( S = w -> ((ph /\ w C_ T) -> ch))) /\ R = z /\ (ph /\ z C_ T)) -> A.y( S e. R -> ch))
70		tfisi.c	. . . . . . . . . . . 12 |- ((ph /\ ( R e. On /\ R C_ T) /\ A.y( S e. R -> ch)) -> ps)
71	24, 27, 29, 69, 70	syl121anc 1139	. . . . . . . . . . 11 |- (((z e. On /\ A.w e. z A.y( S = w -> ((ph /\ w C_ T) -> ch))) /\ R = z /\ (ph /\ z C_ T)) -> ps)
72	71	3exp 1102	. . . . . . . . . 10 |- ((z e. On /\ A.w e. z A.y( S = w -> ((ph /\ w C_ T) -> ch))) -> ( R = z -> ((ph /\ z C_ T) -> ps)))
73	72	alrimiv 1751	. . . . . . . . 9 |- ((z e. On /\ A.w e. z A.y( S = w -> ((ph /\ w C_ T) -> ch))) -> A.x( R = z -> ((ph /\ z C_ T) -> ps)))
74	73	ex 108	. . . . . . . 8 |- (z e. On -> (A.w e. z A.y( S = w -> ((ph /\ w C_ T) -> ch)) -> A.x( R = z -> ((ph /\ z C_ T) -> ps))))
75	17, 23, 74	tfis3 4252	. . . . . . 7 |- ( T e. On -> A.x( R = T -> ((ph /\ T C_ T) -> ps)))
76	4, 75	syl 14	. . . . . 6 |- (ph -> A.x( R = T -> ((ph /\ T C_ T) -> ps)))
77		tfisi.g	. . . . . . . . 9 |- (x = A -> R = T)
78	77	eqeq1d 2045	. . . . . . . 8 |- (x = A -> ( R = T <-> T = T))
79		tfisi.e	. . . . . . . . 9 |- (x = A -> (ps <-> th))
80	79	imbi2d 219	. . . . . . . 8 |- (x = A -> (((ph /\ T C_ T) -> ps) <-> ((ph /\ T C_ T) -> th)))
81	78, 80	imbi12d 223	. . . . . . 7 |- (x = A -> (( R = T -> ((ph /\ T C_ T) -> ps)) <-> ( T = T -> ((ph /\ T C_ T) -> th))))
82	81	spcgv 2634	. . . . . 6 |- (A e. V -> (A.x( R = T -> ((ph /\ T C_ T) -> ps)) -> ( T = T -> ((ph /\ T C_ T) -> th))))
83	3, 76, 82	sylc 56	. . . . 5 |- (ph -> ( T = T -> ((ph /\ T C_ T) -> th)))
84	2, 83	mpi 15	. . . 4 |- (ph -> ((ph /\ T C_ T) -> th))
85	84	expd 245	. . 3 |- (ph -> (ph -> ( T C_ T -> th)))
86	85	pm2.43i 43	. 2 |- (ph -> ( T C_ T -> th))
87	1, 86	mpi 15	1 |- (ph -> th)

Syntax hints:   -> wi 4   /\ wa 97   <-> wb 98   /\ w3a 884  A.wal 1240   = wceq 1242   e. wcel 1390  [wsb 1642  A.wral 2300   [_csb 2846   C_ wss 2911   Oncon0 4066

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-setind 4220

This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-rab 2309  df-v 2553  df-sbc 2759  df-csb 2847  df-in 2918  df-ss 2925  df-uni 3572  df-tr 3846  df-iord 4069  df-on 4071

This theorem is referenced by: (None)