Theorem tfrlem5 4216

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

Hypotheses

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

Assertion

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

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

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 4214	. . . . 5 |- A = {g | E.z e. On (g Fn z /\ A.y e. z (g` y) = (G` (g |` y)))}
3	2	abeq2i 1613	. . . 4 |- (g e. A <-> E.z e. On (g Fn z /\ A.y e. z (g` y) = (G` (g |` y))))
4	1	tfrlem3 4214	. . . . 5 |- A = {h | E.w e. On (h Fn w /\ A.y e. w (h` y) = (G` (h |` y)))}
5	4	abeq2i 1613	. . . 4 |- (h e. A <-> E.w e. On (h Fn w /\ A.y e. w (h` y) = (G` (h |` y))))
6	3, 5	anbi12i 485	. . 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 1824	. . 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 174	. 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		2elresin 3704	. . . . . . . . 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)))))
10		tfrlem2 4213	. . . . . . . . . 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))))
11		fnresin1 3707	. . . . . . . . . 10 |- (g Fn z -> (g |` (z i^i w)) Fn (z i^i w))
12		fnresin2 3708	. . . . . . . . . 10 |- (h Fn w -> (h |` (z i^i w)) Fn (z i^i w))
13	10, 11, 12	syl2an 456	. . . . . . . . 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))))
14	9, 13	sylbid 201	. . . . . . . 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))))
15	14	com24 37	. . . . . . 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))))
16	15	com3r 35	. . . . . 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))))
17	16	imp32 361	. . . . 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))
18		onin 3006	. . . . 5 |- ((z e. On /\ w e. On) -> (z i^i w) e. On)
19		r19.26m 1798	. . . . . . . 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))))
20		prth 559	. . . . . . . . . . . 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)))))
21		pm3.27 321	. . . . . . . . . . . . 13 |- (((z i^i w) e. On /\ y e. (z i^i w)) -> y e. (z i^i w))
22		elin 2259	. . . . . . . . . . . . 13 |- (y e. (z i^i w) <-> (y e. z /\ y e. w))
23	21, 22	sylib 196	. . . . . . . . . . . 12 |- (((z i^i w) e. On /\ y e. (z i^i w)) -> (y e. z /\ y e. w))
24	20, 23	syl5 21	. . . . . . . . . . 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)))))
25		onelss 3017	. . . . . . . . . . . . . 14 |- ((z i^i w) e. On -> (y e. (z i^i w) -> y (_ (z i^i w)))
26	25	impac 387	. . . . . . . . . . . . 13 |- (((z i^i w) e. On /\ y e. (z i^i w)) -> (y (_ (z i^i w) /\ y e. (z i^i w)))
27		fvres 3845	. . . . . . . . . . . . . . 15 |- (y e. (z i^i w) -> ((g |` (z i^i w))` y) = (g` y))
28		resabs1 3478	. . . . . . . . . . . . . . . 16 |- (y (_ (z i^i w) -> ((g |` (z i^i w)) |` y) = (g |` y))
29	28	fveq2d 3839	. . . . . . . . . . . . . . 15 |- (y (_ (z i^i w) -> (G` ((g |` (z i^i w)) |` y)) = (G` (g |` y)))
30	27, 29	eqeqan12rd 1534	. . . . . . . . . . . . . 14 |- ((y (_ (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))))
31		fvres 3845	. . . . . . . . . . . . . . 15 |- (y e. (z i^i w) -> ((h |` (z i^i w))` y) = (h` y))
32		resabs1 3478	. . . . . . . . . . . . . . . 16 |- (y (_ (z i^i w) -> ((h |` (z i^i w)) |` y) = (h |` y))
33	32	fveq2d 3839	. . . . . . . . . . . . . . 15 |- (y (_ (z i^i w) -> (G` ((h |` (z i^i w)) |` y)) = (G` (h |` y)))
34	31, 33	eqeqan12rd 1534	. . . . . . . . . . . . . 14 |- ((y (_ (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))))
35	30, 34	anbi12d 631	. . . . . . . . . . . . 13 |- ((y (_ (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)))))
36	26, 35	syl 10	. . . . . . . . . . . 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)))))
37	36	bicomd 524	. . . . . . . . . . 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)))))
38	24, 37	mpbidi 592	. . . . . . . . . 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)))))
39	38	exp3a 374	. . . . . . . . 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))))))
40	39	19.20i 1028	. . . . . . . 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))))))
41	19, 40	sylbir 199	. . . . . . 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))))))
42	41	anim2i 333	. . . . . 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)))))))
43	42	an4s 511	. . . . 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)))))))
44	17, 18, 43	syl2an 456	. . . 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 371	. . 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 1794	. 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 197	1 |- ((g e. A /\ h e. A) -> ((<.x, u>. e. g /\ <.x, v>. e. h) -> u = v))

Syntax hints:   -> wi 3   <-> wb 144   /\ wa 221  A.wal 990   = wceq 992   e. wcel 994  {cab 1505  A.wral 1691  E.wrex 1692   i^i cin 2098   (_ wss 2099  <.cop 2469  U.cuni 2569  Oncon0 2975   |` cres 3253   Fn wfn 3258  ` cfv 3263

This theorem is referenced by:  tfrlem7 4218

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-9 1001  ax-10 1002  ax-11 1003  ax-12 1004  ax-13 1005  ax-14 1006  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500  ax-sep 2777  ax-pow 2818  ax-pr 2855  ax-un 3089

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-3or 782  df-3an 783  df-ex 1017  df-sb 1209  df-eu 1421  df-mo 1422  df-clab 1506  df-cleq 1511  df-clel 1514  df-ne 1630  df-ral 1695  df-rex 1696  df-rab 1698  df-v 1858  df-sbc 1987  df-dif 2101  df-un 2102  df-in 2103  df-ss 2105  df-nul 2333  df-pw 2459  df-sn 2470  df-pr 2471  df-tp 2473  df-op 2474  df-uni 2570  df-br 2693  df-opab 2741  df-tr 2755  df-eprel 2910  df-id 2913  df-po 2918  df-so 2929  df-fr 2947  df-we 2962  df-ord 2978  df-on 2979  df-xp 3265  df-rel 3266  df-cnv 3267  df-co 3268  df-dm 3269  df-rn 3270  df-res 3271  df-ima 3272  df-fun 3273  df-fn 3274  df-fv 3279

Copyright terms: Public domain