Theorem tfrlem2 2950

Description: Lemma for transfinite recursion. This provides some messy details needed to link tfrlem1 2949 into the main proof.

Assertion

Ref	Expression
tfrlem2	|- ((F Fn A /\ G Fn A) -> ((<.x, y>. e. F /\ <.x, z>. e. G) -> (A e. On -> (A.w(A e. On -> (w e. A -> ((F` w) = (B` (F |` w)) /\ (G` w) = (B` (G |` w))))) -> y = z))))

Distinct variable group(s):   w,A   w,B   w,F   w,G   x,w   y,w

Proof of Theorem tfrlem2

Step	Hyp	Ref	Expression
1		visset 1350	. . . . . . . . . . . . 13 |- x e. V
2		visset 1350	. . . . . . . . . . . . 13 |- y e. V
3	1, 2	fnop 2727	. . . . . . . . . . . 12 |- ((F Fn A /\ <.x, y>. e. F) -> x e. A)
4	3	adantr 306	. . . . . . . . . . 11 |- (((F Fn A /\ <.x, y>. e. F) /\ (G Fn A /\ <.x, z>. e. G)) -> x e. A)
5	4	an4s 390	. . . . . . . . . 10 |- (((F Fn A /\ G Fn A) /\ (<.x, y>. e. F /\ <.x, z>. e. G)) -> x e. A)
6		tfrlem1 2949	. . . . . . . . . . . 12 |- (A e. On -> ((F Fn A /\ G Fn A) -> (A.w e. A ((F` w) = (B` (F |` w)) /\ (G` w) = (B` (G |` w))) -> A.w e. A (F` w) = (G` w))))
7		fveq2 2832	. . . . . . . . . . . . . 14 |- (w = x -> (F` w) = (F` x))
8		fveq2 2832	. . . . . . . . . . . . . 14 |- (w = x -> (G` w) = (G` x))
9	7, 8	cleq12d 1115	. . . . . . . . . . . . 13 |- (w = x -> ((F` w) = (G` w) <-> (F` x) = (G` x)))
10	9	rcla4v 1402	. . . . . . . . . . . 12 |- (A.w e. A (F` w) = (G` w) -> (x e. A -> (F` x) = (G` x)))
11	6, 10	syl8 25	. . . . . . . . . . 11 |- (A e. On -> ((F Fn A /\ G Fn A) -> (A.w e. A ((F` w) = (B` (F |` w)) /\ (G` w) = (B` (G |` w))) -> (x e. A -> (F` x) = (G` x)))))
12	11	com4r 41	. . . . . . . . . 10 |- (x e. A -> (A e. On -> ((F Fn A /\ G Fn A) -> (A.w e. A ((F` w) = (B` (F |` w)) /\ (G` w) = (B` (G |` w))) -> (F` x) = (G` x)))))
13	5, 12	syl 12	. . . . . . . . 9 |- (((F Fn A /\ G Fn A) /\ (<.x, y>. e. F /\ <.x, z>. e. G)) -> (A e. On -> ((F Fn A /\ G Fn A) -> (A.w e. A ((F` w) = (B` (F |` w)) /\ (G` w) = (B` (G |` w))) -> (F` x) = (G` x)))))
14	13	exp 291	. . . . . . . 8 |- ((F Fn A /\ G Fn A) -> ((<.x, y>. e. F /\ <.x, z>. e. G) -> (A e. On -> ((F Fn A /\ G Fn A) -> (A.w e. A ((F` w) = (B` (F |` w)) /\ (G` w) = (B` (G |` w))) -> (F` x) = (G` x))))))
15	14	com4r 41	. . . . . . 7 |- ((F Fn A /\ G Fn A) -> ((F Fn A /\ G Fn A) -> ((<.x, y>. e. F /\ <.x, z>. e. G) -> (A e. On -> (A.w e. A ((F` w) = (B` (F |` w)) /\ (G` w) = (B` (G |` w))) -> (F` x) = (G` x))))))
16	15	pm2.43i 58	. . . . . 6 |- ((F Fn A /\ G Fn A) -> ((<.x, y>. e. F /\ <.x, z>. e. G) -> (A e. On -> (A.w e. A ((F` w) = (B` (F |` w)) /\ (G` w) = (B` (G |` w))) -> (F` x) = (G` x)))))
17	16	imp43 288	. . . . 5 |- ((((F Fn A /\ G Fn A) /\ (<.x, y>. e. F /\ <.x, z>. e. G)) /\ (A e. On /\ A.w e. A ((F` w) = (B` (F |` w)) /\ (G` w) = (B` (G |` w))))) -> (F` x) = (G` x))
18		df-ral 1205	. . . . . 6 |- (A.w e. A ((F` w) = (B` (F |` w)) /\ (G` w) = (B` (G |` w))) <-> A.w(w e. A -> ((F` w) = (B` (F |` w)) /\ (G` w) = (B` (G |` w)))))
19	18	anbi2i 367	. . . . 5 |- ((A e. On /\ A.w e. A ((F` w) = (B` (F |` w)) /\ (G` w) = (B` (G |` w)))) <-> (A e. On /\ A.w(w e. A -> ((F` w) = (B` (F |` w)) /\ (G` w) = (B` (G |` w))))))
20	17, 19	sylan2br 348	. . . 4 |- ((((F Fn A /\ G Fn A) /\ (<.x, y>. e. F /\ <.x, z>. e. G)) /\ (A e. On /\ A.w(w e. A -> ((F` w) = (B` (F |` w)) /\ (G` w) = (B` (G |` w)))))) -> (F` x) = (G` x))
21	2	funfvopi 2853	. . . . . . . . . 10 |- (Fun F -> (<.x, y>. e. F -> (F` x) = y))
22	21	imp 277	. . . . . . . . 9 |- ((Fun F /\ <.x, y>. e. F) -> (F` x) = y)
23		visset 1350	. . . . . . . . . . 11 |- z e. V
24	23	funfvopi 2853	. . . . . . . . . 10 |- (Fun G -> (<.x, z>. e. G -> (G` x) = z))
25	24	imp 277	. . . . . . . . 9 |- ((Fun G /\ <.x, z>. e. G) -> (G` x) = z)
26	22, 25	anim12i 268	. . . . . . . 8 |- (((Fun F /\ <.x, y>. e. F) /\ (Fun G /\ <.x, z>. e. G)) -> ((F` x) = y /\ (G` x) = z))
27	26	an4s 390	. . . . . . 7 |- (((Fun F /\ Fun G) /\ (<.x, y>. e. F /\ <.x, z>. e. G)) -> ((F` x) = y /\ (G` x) = z))
28		fnfun 2721	. . . . . . . 8 |- (F Fn A -> Fun F)
29		fnfun 2721	. . . . . . . 8 |- (G Fn A -> Fun G)
30	28, 29	anim12i 268	. . . . . . 7 |- ((F Fn A /\ G Fn A) -> (Fun F /\ Fun G))
31	27, 30	sylan 343	. . . . . 6 |- (((F Fn A /\ G Fn A) /\ (<.x, y>. e. F /\ <.x, z>. e. G)) -> ((F` x) = y /\ (G` x) = z))
32		cleq12 1113	. . . . . 6 |- (((F` x) = y /\ (G` x) = z) -> ((F` x) = (G` x) <-> y = z))
33	31, 32	syl 12	. . . . 5 |- (((F Fn A /\ G Fn A) /\ (<.x, y>. e. F /\ <.x, z>. e. G)) -> ((F` x) = (G` x) <-> y = z))
34	33	adantr 306	. . . 4 |- ((((F Fn A /\ G Fn A) /\ (<.x, y>. e. F /\ <.x, z>. e. G)) /\ (A e. On /\ A.w(w e. A -> ((F` w) = (B` (F |` w)) /\ (G` w) = (B` (G |` w)))))) -> ((F` x) = (G` x) <-> y = z))
35	20, 34	mpbid 170	. . 3 |- ((((F Fn A /\ G Fn A) /\ (<.x, y>. e. F /\ <.x, z>. e. G)) /\ (A e. On /\ A.w(w e. A -> ((F` w) = (B` (F |` w)) /\ (G` w) = (B` (G |` w)))))) -> y = z)
36		abai 366	. . . . 5 |- ((A e. On /\ (w e. A -> ((F` w) = (B` (F |` w)) /\ (G` w) = (B` (G |` w))))) <-> (A e. On /\ (A e. On -> (w e. A -> ((F` w) = (B` (F |` w)) /\ (G` w) = (B` (G |` w)))))))
37	36	bial 695	. . . 4 |- (A.w(A e. On /\ (w e. A -> ((F` w) = (B` (F |` w)) /\ (G` w) = (B` (G |` w))))) <-> A.w(A e. On /\ (A e. On -> (w e. A -> ((F` w) = (B` (F |` w)) /\ (G` w) = (B` (G |` w)))))))
38		19.28v 957	. . . 4 |- (A.w(A e. On /\ (w e. A -> ((F` w) = (B` (F |` w)) /\ (G` w) = (B` (G |` w))))) <-> (A e. On /\ A.w(w e. A -> ((F` w) = (B` (F |` w)) /\ (G` w) = (B` (G |`