Theorem tfrlem5 5287

Description: Lemma for transfinite recursion. The values of two acceptable functions are the same within their domains.

Hypothesis

Ref	Expression
tfrlem.1	|- A = {f | E.x e. On (f Fn x /\ A.y e. x (f` y) = (G` (f |` y)))}

Assertion

Ref	Expression
tfrlem5	|- ((g e. A /\ h e. A) -> ((<.x, u>. e. g /\ <.x, v>. e. h) -> u = v))

Distinct variable groups:   x,f,y,g,G,h   u,f,v   g,h,u,v,x,y

Proof of Theorem tfrlem5

Step	Hyp	Ref	Expression
1		tfrlem.1	. . . . . 6 |- A = {f | E.x e. On (f Fn x /\ A.y e. x (f` y) = (G` (f |` y)))}
2	1	tfrlem3 5284	. . . . 5 |- A = {g | E.z e. On (g Fn z /\ A.y e. z (g` y) = (G` (g |` y)))}
3	2	abeq2i 2250	. . . 4 |- (g e. A <-> E.z e. On (g Fn z /\ A.y e. z (g` y) = (G` (g |` y))))
4	1	tfrlem3 5284	. . . . 5 |- A = {h | E.w e. On (h Fn w /\ A.y e. w (h` y) = (G` (h |` y)))}
5	4	abeq2i 2250	. . . 4 |- (h e. A <-> E.w e. On (h Fn w /\ A.y e. w (h` y) = (G` (h |` y))))
6	3, 5	anbi12i 710	. . 3 |- ((g e. A /\ h e. A) <-> (E.z e. On (g Fn z /\ A.y e. z (g` y) = (G` (g |` y))) /\ E.w e. On (h Fn w /\ A.y e. w (h` y) = (G` (h |` y)))))
7		reeanv 2493	. . 3 |- (E.z e. On E.w e. On ((g Fn z /\ A.y e. z (g` y) = (G` (g |` y))) /\ (h Fn w /\ A.y e. w (h` y) = (G` (h |` y)))) <-> (E.z e. On (g Fn z /\ A.y e. z (g` y) = (G` (g |` y))) /\ E.w e. On (h Fn w /\ A.y e. w (h` y) = (G` (h |` y)))))
8	6, 7	bitr4i 283	. 2 |- ((g e. A /\ h e. A) <-> E.z e. On E.w e. On ((g Fn z /\ A.y e. z (g` y) = (G` (g |` y))) /\ (h Fn w /\ A.y e. w (h` y) = (G` (h |` y)))))
9		onin 3842	. . . . 5 |- ((z e. On /\ w e. On) -> (z i^i w) e. On)
10		r19.26m 2469	. . . . . . . 8 |- (A.y((y e. z -> (g` y) = (G` (g |` y))) /\ (y e. w -> (h` y) = (G` (h |` y)))) <-> (A.y e. z (g` y) = (G` (g |` y)) /\ A.y e. w (h` y) = (G` (h |` y))))
11		simpr 442	. . . . . . . . . . . . 13 |- (((z i^i w) e. On /\ y e. (z i^i w)) -> y e. (z i^i w))
12		elin 2999	. . . . . . . . . . . . 13 |- (y e. (z i^i w) <-> (y e. z /\ y e. w))
13	11, 12	sylib 242	. . . . . . . . . . . 12 |- (((z i^i w) e. On /\ y e. (z i^i w)) -> (y e. z /\ y e. w))
14		prth 541	. . . . . . . . . . . 12 |- (((y e. z -> (g` y) = (G` (g |` y))) /\ (y e. w -> (h` y) = (G` (h |` y)))) -> ((y e. z /\ y e. w) -> ((g` y) = (G` (g |` y)) /\ (h` y) = (G` (h |` y)))))
15	13, 14	syl5 35	. . . . . . . . . . 11 |- (((y e. z -> (g` y) = (G` (g |` y))) /\ (y e. w -> (h` y) = (G` (h |` y)))) -> (((z i^i w) e. On /\ y e. (z i^i w)) -> ((g` y) = (G` (g |` y)) /\ (h` y) = (G` (h |` y)))))
16		onelss 3853	. . . . . . . . . . . . . 14 |- ((z i^i w) e. On -> (y e. (z i^i w) -> y C_ (z i^i w)))
17	16	impac 593	. . . . . . . . . . . . 13 |- (((z i^i w) e. On /\ y e. (z i^i w)) -> (y C_ (z i^i w) /\ y e. (z i^i w)))
18		fvres 4780	. . . . . . . . . . . . . . 15 |- (y e. (z i^i w) -> ((g |` (z i^i w))` y) = (g` y))
19		resabs1 4364	. . . . . . . . . . . . . . . 16 |- (y C_ (z i^i w) -> ((g |` (z i^i w)) |` y) = (g |` y))
20	19	fveq2d 4769	. . . . . . . . . . . . . . 15 |- (y C_ (z i^i w) -> (G` ((g |` (z i^i w)) |` y)) = (G` (g |` y)))
21	18, 20	eqeqan12rd 2157	. . . . . . . . . . . . . 14 |- ((y C_ (z i^i w) /\ y e. (z i^i w)) -> (((g |` (z i^i w))` y) = (G` ((g |` (z i^i w)) |` y)) <-> (g` y) = (G` (g |` y))))
22		fvres 4780	. . . . . . . . . . . . . . 15 |- (y e. (z i^i w) -> ((h |` (z i^i w))` y) = (h` y))
23		resabs1 4364	. . . . . . . . . . . . . . . 16 |- (y C_ (z i^i w) -> ((h |` (z i^i w)) |` y) = (h |` y))
24	23	fveq2d 4769	. . . . . . . . . . . . . . 15 |- (y C_ (z i^i w) -> (G` ((h |` (z i^i w)) |` y)) = (G` (h |` y)))
25	22, 24	eqeqan12rd 2157	. . . . . . . . . . . . . 14 |- ((y C_ (z i^i w) /\ y e. (z i^i w)) -> (((h |` (z i^i w))` y) = (G` ((h |` (z i^i w)) |` y)) <-> (h` y) = (G` (h |` y))))
26	21, 25	anbi12d 763	. . . . . . . . . . . . 13 |- ((y C_ (z i^i w) /\ y e. (z i^i w)) -> ((((g |` (z i^i w))` y) = (G` ((g |` (z i^i w)) |` y)) /\ ((h |` (z i^i w))` y) = (G` ((h |` (z i^i w)) |` y))) <-> ((g` y) = (G` (g |` y)) /\ (h` y) = (G` (h |` y)))))
27	17, 26	syl 13	. . . . . . . . . . . 12 |- (((z i^i w) e. On /\ y e. (z i^i w)) -> ((((g |` (z i^i w))` y) = (G` ((g |` (z i^i w)) |` y)) /\ ((h |` (z i^i w))` y) = (G` ((h |` (z i^i w)) |` y))) <-> ((g` y) = (G` (g |` y)) /\ (h` y) = (G` (h |` y)))))
28	27	bicomd 271	. . . . . . . . . . 11 |- (((z i^i w) e. On /\ y e. (z i^i w)) -> (((g` y) = (G` (g |` y)) /\ (h` y) = (G` (h |` y))) <-> (((g |` (z i^i w))` y) = (G` ((g |` (z i^i w)) |` y)) /\ ((h |` (z i^i w))` y) = (G` ((h |` (z i^i w)) |` y)))))
29	15, 28	mpbidi 922	. . . . . . . . . 10 |- (((y e. z -> (g` y) = (G` (g |` y))) /\ (y e. w -> (h` y) = (G` (h |` y)))) -> (((z i^i w) e. On /\ y e. (z i^i w)) -> (((g |` (z i^i w))` y) = (G` ((g |` (z i^i w)) |` y)) /\ ((h |` (z i^i w))` y) = (G` ((h |` (z i^i w)) |` y)))))
30	29	exp3a 400	. . . . . . . . 9 |- (((y e. z -> (g` y) = (G` (g |` y))) /\ (y e. w -> (h` y) = (G` (h |` y)))) -> ((z i^i w) e. On -> (y e. (z i^i w) -> (((g |` (z i^i w))` y) = (G` ((g |` (z i^i w)) |` y)) /\ ((h |` (z i^i w))` y) = (G` ((h |` (z i^i w)) |` y))))))
31	30	alimi 1627	. . . . . . . 8 |- (A.y((y e. z -> (g` y) = (G` (g |` y))) /\ (y e. w -> (h` y) = (G` (h |` y)))) -> A.y((z i^i w) e. On -> (y e. (z i^i w) -> (((g |` (z i^i w))` y) = (G` ((g |` (z i^i w)) |` y)) /\ ((h |` (z i^i w))` y) = (G` ((h |` (z i^i w)) |` y))))))
32	10, 31	sylbir 244	. . . . . . 7 |- ((A.y e. z (g` y) = (G` (g |` y)) /\ A.y e. w (h` y) = (G` (h |` y))) -> A.y((z i^i w) e. On -> (y e. (z i^i w) -> (((g |` (z i^i w))` y) = (G` ((g |` (z i^i w)) |` y)) /\ ((h |` (z i^i w))` y) = (G` ((h |` (z i^i w)) |` y))))))
33	32	anim2i 539	. . . . . 6 |- (((g Fn z /\ h Fn w) /\ (A.y e. z (g` y) = (G` (g |` y)) /\ A.y e. w (h` y) = (G` (h |` y)))) -> ((g Fn z /\ h Fn w) /\ A.y((z i^i w) e. On -> (y e. (z i^i w) -> (((g |` (z i^i w))` y) = (G` ((g |` (z i^i w)) |` y)) /\ ((h |` (z i^i w))` y) = (G` ((h |` (z i^i w)) |` y)))))))
34	33	an4s 884	. . . . 5 |- (((g Fn z /\ A.y e. z (g` y) = (G` (g |` y))) /\ (h Fn w /\ A.y e. w (h` y) = (G` (h |` y)))) -> ((g Fn z /\ h Fn w) /\ A.y((z i^i w) e. On -> (y e. (z i^i w) -> (((g |` (z i^i w))` y) = (G` ((g |` (z i^i w)) |` y)) /\ ((h |` (z i^i w))` y) = (G` ((h |` (z i^i w)) |` y)))))))
35		2elresin 4623	. . . . . . . . 9 |- ((g Fn z /\ h Fn w) -> ((<.x, u>. e. g /\ <.x, v>. e. h) <-> (<.x, u>. e. (g |` (z i^i w)) /\ <.x, v>. e. (h |` (z i^i w)))))
36		fnresin1 4626	. . . . . . . . . 10 |- (g Fn z -> (g |` (z i^i w)) Fn (z i^i w))
37		fnresin2 4627	. . . . . . . . . 10 |- (h Fn w -> (h |` (z i^i w)) Fn (z i^i w))
38		tfrlem2 5283	. . . . . . . . . 10 |- (((g |` (z i^i w)) Fn (z i^i w) /\ (h |` (z i^i w)) Fn (z i^i w)) -> ((<.x, u>. e. (g |` (z i^i w)) /\ <.x, v>. e. (h |` (z i^i w))) -> ((z i^i w) e. On -> (A.y((z i^i w) e. On -> (y e. (z i^i w) -> (((g |` (z i^i w))` y) = (G` ((g |` (z i^i w)) |` y)) /\ ((h |` (z i^i w))` y) = (G` ((h |` (z i^i w)) |` y))))) -> u = v))))
39	36, 37, 38	syl2an 603	. . . . . . . . 9 |- ((g Fn z /\ h Fn w) -> ((<.x, u>. e. (g |` (z i^i w)) /\ <.x, v>. e. (h |` (z i^i w))) -> ((z i^i w) e. On -> (A.y((z i^i w) e. On -> (y e. (z i^i w) -> (((g |` (z i^i w))` y) = (G` ((g |` (z i^i w)) |` y)) /\ ((h |` (z i^i w))` y) = (G` ((h |` (z i^i w)) |` y))))) -> u = v))))
40	35, 39	sylbid 246	. . . . . . . 8 |- ((g Fn z /\ h Fn w) -> ((<.x, u>. e. g /\ <.x, v>. e. h) -> ((z i^i w) e. On -> (A.y((z i^i w) e. On -> (y e. (z i^i w) -> (((g |` (z i^i w))` y) = (G` ((g |` (z i^i w)) |` y)) /\ ((h |` (z i^i w))` y) = (G` ((h |` (z i^i w)) |` y))))) -> u = v))))
41	40	com24 79	. . . . . . 7 |- ((g Fn z /\ h Fn w) -> (A.y((z i^i w) e. On -> (y e. (z i^i w) -> (((g |` (z i^i w))` y) = (G` ((g |` (z i^i w)) |` y)) /\ ((h |` (z i^i w))` y) = (G` ((h |` (z i^i w)) |` y))))) -> ((z i^i w) e. On -> ((<.x, u>. e. g /\ <.x, v>. e. h) -> u = v))))
42	41	com3r 66	. . . . . 6 |- ((z i^i w) e. On -> ((g Fn z /\ h Fn w) -> (A.y((z i^i w) e. On -> (y e. (z i^i w) -> (((g |` (z i^i w))` y) = (G` ((g |` (z i^i w)) |` y)) /\ ((h |` (z i^i w))` y) = (G` ((h |` (z i^i w)) |` y))))) -> ((<.x, u>. e. g /\ <.x, v>. e. h) -> u = v))))
43	42	imp32 397	. . . . 5 |- (((z i^i w) e. On /\ ((g Fn z /\ h Fn w) /\ A.y((z i^i w) e. On -> (y e. (z i^i w) -> (((g |` (z i^i w))` y) = (G` ((g |` (z i^i w)) |` y)) /\ ((h |` (z i^i w))` y) = (G` ((h |` (z i^i w)) |` y))))))) -> ((<.x, u>. e. g /\ <.x, v>. e. h) -> u = v))
44	9, 34, 43	syl2an 603	. . . 4 |- (((z e. On /\ w e. On) /\ ((g Fn z /\ A.y e. z (g` y) = (G` (g |` y))) /\ (h Fn w /\ A.y e. w (h` y) = (G` (h |` y))))) -> ((<.x, u>. e. g /\ <.x, v>. e. h) -> u = v))
45	44	ex 398	. . 3 |- ((z e. On /\ w e. On) -> (((g Fn z /\ A.y e. z (g` y) = (G` (g |` y))) /\ (h Fn w /\ A.y e. w (h` y) = (G` (h |` y)))) -> ((<.x, u>. e. g /\ <.x, v>. e. h) -> u = v)))
46	45	r19.23aivv 2465	. 2 |- (E.z e. On E.w e. On ((g Fn z /\ A.y e. z (g` y) = (G` (g |` y))) /\ (h Fn w /\ A.y e. w (h` y) = (G` (h |` y)))) -> ((<.x, u>. e. g /\ <.x, v>. e. h) -> u = v))
47	8, 46	sylbi 225	1 |- ((g e. A /\ h e. A) -> ((<.x, u>. e. g /\ <.x, v>. e. h) -> u = v))

Syntax hints:   -> wi 3   <-> wb 219   /\ wa 337  A.wal 1584   = wceq 1586   e. wcel 1588  {cab 2128  A.wral 2355  E.wrex 2356   i^i cin 2826   C_ wss 2827  <.cop 3240  Oncon0 3811   |` cres 4121   Fn wfn 4126  ` cfv 4131

This theorem is referenced by:  tfrlem7 5289

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1592  ax-gen 1593  ax-8 1594  ax-9 1595  ax-10 1596  ax-11 1597  ax-12 1598  ax-13 1599  ax-14 1600  ax-17 1605  ax-4 1608  ax-5o 1610  ax-6o 1613  ax-9o 1763  ax-10o 1781  ax-16 1854  ax-11o 1864  ax-ext 2123  ax-sep 3606  ax-nul 3613  ax-pow 3649  ax-pr 3687  ax-un 3929

This theorem depends on definitions:  df-bi 220  df-or 338  df-an 339  df-3or 1103  df-3an 1104  df-ex 1616  df-sb 1816  df-eu 2041  df-mo 2042  df-clab 2129  df-cleq 2134  df-clel 2137  df-ne 2268  df-ral 2359  df-rex 2360  df-rab 2362  df-v 2540  df-sbc 2700  df-dif 2830  df-un 2832  df-in 2834  df-ss 2836  df-pss 2838  df-nul 3083  df-pw 3229  df-sn 3242  df-pr 3243  df-tp 3245  df-op 3246  df-uni 3367  df-br 3508  df-opab 3566  df-tr 3580  df-eprel 3744  df-id 3747  df-po 3752  df-so 3764  df-fr 3782  df-we 3798  df-ord 3814  df-on 3815  df-xp 4133  df-rel 4134  df-cnv 4135  df-co 4136  df-dm 4137  df-rn 4138  df-res 4139  df-ima 4140  df-fun 4141  df-fn 4142  df-fv 4147

Copyright terms: Public domain