Theorem tfrlem2 3918

Description: Lemma for transfinite recursion. This provides some messy details needed to link tfrlem1 3917 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 groups:   w,A   w,B   w,F   w,G   x,w   y,w

Proof of Theorem tfrlem2

Step	Hyp	Ref	Expression
1		tfrlem1 3917	. . . . . . . . . . 11 |- (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))))
2	1	com12 11	. . . . . . . . . 10 |- ((F Fn A /\ G Fn A) -> (A e. On -> (A.w e. A ((F` w) = (B` (F |` w)) /\ (G` w) = (B` (G |` w))) -> A.w e. A (F` w) = (G` w))))
3	2	imp3a 361	. . . . . . . . 9 |- ((F Fn A /\ G Fn A) -> ((A e. On /\ A.w e. A ((F` w) = (B` (F |` w)) /\ (G` w) = (B` (G |` w)))) -> A.w e. A (F` w) = (G` w)))
4	3	adantr 391	. . . . . . . 8 |- (((F Fn A /\ G Fn A) /\ <.x, y>. e. F) -> ((A e. On /\ A.w e. A ((F` w) = (B` (F |` w)) /\ (G` w) = (B` (G |` w)))) -> A.w e. A (F` w) = (G` w)))
5		fnop 3597	. . . . . . . . . 10 |- ((F Fn A /\ <.x, y>. e. F) -> x e. A)
6	5	adantlr 395	. . . . . . . . 9 |- (((F Fn A /\ G Fn A) /\ <.x, y>. e. F) -> x e. A)
7		fveq2 3730	. . . . . . . . . . 11 |- (w = x -> (F` w) = (F` x))
8		fveq2 3730	. . . . . . . . . . 11 |- (w = x -> (G` w) = (G` x))
9	7, 8	eqeq12d 1492	. . . . . . . . . 10 |- (w = x -> ((F` w) = (G` w) <-> (F` x) = (G` x)))
10	9	rcla4v 1876	. . . . . . . . 9 |- (x e. A -> (A.w e. A (F` w) = (G` w) -> (F` x) = (G` x)))
11	6, 10	syl 10	. . . . . . . 8 |- (((F Fn A /\ G Fn A) /\ <.x, y>. e. F) -> (A.w e. A (F` w) = (G` w) -> (F` x) = (G` x)))
12	4, 11	syld 27	. . . . . . 7 |- (((F Fn A /\ G Fn A) /\ <.x, y>. e. F) -> ((A e. On /\ A.w e. A ((F` w) = (B` (F |` w)) /\ (G` w) = (B` (G |` w)))) -> (F` x) = (G` x)))
13	12	imp 350	. . . . . 6 |- ((((F Fn A /\ G Fn A) /\ <.x, y>. e. F) /\ (A e. On /\ A.w e. A ((F` w) = (B` (F |` w)) /\ (G` w) = (B` (G |` w))))) -> (F` x) = (G` x))
14	13	adantlrr 401	. . . . 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))
15		df-ral 1652	. . . . . 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)))))
16	15	anbi2i 482	. . . . 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))))))
17	14, 16	sylan2br 455	. . . 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))
18		visset 1816	. . . . . . . . . . 11 |- y e. V
19	18	funopfv 3757	. . . . . . . . . 10 |- (Fun F -> (<.x, y>. e. F -> (F` x) = y))
20	19	imp 350	. . . . . . . . 9 |- ((Fun F /\ <.x, y>. e. F) -> (F` x) = y)
21		visset 1816	. . . . . . . . . . 11 |- z e. V
22	21	funopfv 3757	. . . . . . . . . 10 |- (Fun G -> (<.x, z>. e. G -> (G` x) = z))
23	22	imp 350	. . . . . . . . 9 |- ((Fun G /\ <.x, z>. e. G) -> (G` x) = z)
24	20, 23	anim12i 333	. . . . . . . 8 |- (((Fun F /\ <.x, y>. e. F) /\ (Fun G /\ <.x, z>. e. G)) -> ((F` x) = y /\ (G` x) = z))
25	24	an4s 510	. . . . . . 7 |- (((Fun F /\ Fun G) /\ (<.x, y>. e. F /\ <.x, z>. e. G)) -> ((F` x) = y /\ (G` x) = z))
26		fnfun 3591	. . . . . . . 8 |- (F Fn A -> Fun F)
27		fnfun 3591	. . . . . . . 8 |- (G Fn A -> Fun G)
28	26, 27	anim12i 333	. . . . . . 7 |- ((F Fn A /\ G Fn A) -> (Fun F /\ Fun G))
29	25, 28	sylan 450	. . . . . 6 |- (((F Fn A /\ G Fn A) /\ (<.x, y>. e. F /\ <.x, z>. e. G)) -> ((F` x) = y /\ (G` x) = z))
30		eqeq12 1490	. . . . . 6 |- (((F` x) = y /\ (G` x) = z) -> ((F` x) = (G` x) <-> y = z))
31	29, 30	syl 10	. . . . 5 |- (((F Fn A /\ G Fn A) /\ (<.x, y>. e. F /\ <.x, z>. e. G)) -> ((F` x) = (G` x) <-> y = z))
32	31	adantr 391	. . . 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))
33	17, 32	mpbid 195	. . 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)
34		abai 481	. . . . 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)))))))
35	34	albii 1001	. . . 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)))))))
36		19.28v 1301	. . . 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 |` w))))))
37		19.28v 1301	. . . 4 |- (A.w(A e. On /\ (A e. On -> (w e. A -> ((F` w) = (B` (F |` w)) /\ (G` w) = (B` (G |` w)))))) <-> (A e. On /\ A.w(A e. On -> (w e. A -> ((F` w) = (B` (F |` w)) /\ (G` w) = (B` (G |` w))))