Theorem tfr3 2964

Description: Principle of Transfinite Recursion, part 3 of 3. Theorem 7.41(3) of [TakeutiZaring] p. 47. Finally we show that F is unique. We do this by showing that any class B with the same properties of F that we showed in parts 1 and 2 is identical to F.

Hypotheses

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

Assertion

Ref	Expression
tfr3	|- ((B Fn On /\ A.x e. On (B` x) = (G` (B |` x))) -> B = F)

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

Proof of Theorem tfr3

Step	Hyp	Ref	Expression
1		cleqid 1102	. . . 4 |- On = On
2		tfr.1	. . . . . . 7 |- A = {f | E.x e. On (f Fn x /\ A.y e. x (f` y) = (G` (f |` y)))}
3		tfr.2	. . . . . . 7 |- F = U.A
4	2, 3	tfr1 2962	. . . . . 6 |- F Fn On
5		cleqfv 2880	. . . . . 6 |- ((B Fn On /\ F Fn On) -> (B = F <-> (On = On /\ A.x e. On (B` x) = (F` x))))
6	4, 5	mpan2 519	. . . . 5 |- (B Fn On -> (B = F <-> (On = On /\ A.x e. On (B` x) = (F` x))))
7	6	biimpar 325	. . . 4 |- ((B Fn On /\ (On = On /\ A.x e. On (B` x) = (F` x))) -> B = F)
8	1, 7	mpan21 531	. . 3 |- ((B Fn On /\ A.x e. On (B` x) = (F` x)) -> B = F)
9		ax-17 925	. . . . 5 |- (B Fn On -> A.x B Fn On)
10		hbra1 1237	. . . . 5 |- (A.x e. On (B` x) = (G` (B |` x)) -> A.xA.x e. On (B` x) = (G` (B |` x)))
11	9, 10	hban 704	. . . 4 |- ((B Fn On /\ A.x e. On (B` x) = (G` (B |` x))) -> A.x(B Fn On /\ A.x e. On (B` x) = (G` (B |` x))))
12		ax-17 925	. . . . . . 7 |- ((B` y) = (F` y) -> A.x(B` y) = (F` y))
13	11, 12	hbim 702	. . . . . 6 |- (((B Fn On /\ A.x e. On (B` x) = (G` (B |` x))) -> (B` y) = (F` y)) -> A.x((B Fn On /\ A.x e. On (B` x) = (G` (B |` x))) -> (B` y) = (F` y)))
14		fveq2 2832	. . . . . . . 8 |- (x = y -> (B` x) = (B` y))
15		fveq2 2832	. . . . . . . 8 |- (x = y -> (F` x) = (F` y))
16	14, 15	cleq12d 1115	. . . . . . 7 |- (x = y -> ((B` x) = (F` x) <-> (B` y) = (F` y)))
17	16	imbi2d 464	. . . . . 6 |- (x = y -> (((B Fn On /\ A.x e. On (B` x) = (G` (B |` x))) -> (B` x) = (F` x)) <-> ((B Fn On /\ A.x e. On (B` x) = (G` (B |` x))) -> (B` y) = (F` y))))
18		ra4 1243	. . . . . . . . . . 11 |- (A.x e. On (B` x) = (G` (B |` x)) -> (x e. On -> (B` x) = (G` (B |` x))))
19		fvreseq 2882	. . . . . . . . . . . . . . . . . . . . . 22 |- (((B Fn On /\ F Fn On) /\ x (_ On) -> ((B |` x) = (F |` x) <-> A.y e. x (B` y) = (F` y)))
20	4, 19	mpan12 530	. . . . . . . . . . . . . . . . . . . . 21 |- ((B Fn On /\ x (_ On) -> ((B |` x) = (F |` x) <-> A.y e. x (B` y) = (F` y)))
21		fveq2 2832	. . . . . . . . . . . . . . . . . . . . 21 |- ((B |` x) = (F |` x) -> (G` (B |` x)) = (G` (F |` x)))
22	20, 21	syl6bir 188	. . . . . . . . . . . . . . . . . . . 20 |- ((B Fn On /\ x (_ On) -> (A.y e. x (B` y) = (F` y) -> (G` (B |` x)) = (G` (F |` x))))
23		onsst 2243	. . . . . . . . . . . . . . . . . . . 20 |- (x e. On -> x (_ On)
24	22, 23	sylan2 346	. . . . . . . . . . . . . . . . . . 19 |- ((B Fn On /\ x e. On) -> (A.y e. x (B` y) = (F` y) -> (G` (B |` x)) = (G` (F |` x))))
25	24	ancoms 334	. . . . . . . . . . . . . . . . . 18 |- ((x e. On /\ B Fn On) -> (A.y e. x (B` y) = (F` y) -> (G` (B |` x)) = (G` (F |` x))))
26	25	imp 277	. . . . . . . . . . . . . . . . 17 |- (((x e. On /\ B Fn On) /\ A.y e. x (B` y) = (F` y)) -> (G` (B |` x)) = (G` (F |` x)))
27	26	adantr 306	. . . . . . . . . . . . . . . 16 |- ((((x e. On /\ B Fn On) /\ A.y e. x (B` y) = (F` y)) /\ ((x e. On -> (B` x) = (G` (B |` x))) /\ x e. On)) -> (G` (B |` x)) = (G` (F |` x)))
28	2, 3	tfr2 2963	. . . . . . . . . . . . . . . . . . . . 21 |- (x e. On -> (F` x) = (G` (F |` x)))
29	28	jctr 239	. . . . . . . . . . . . . . . . . . . 20 |- ((x e. On -> (B` x) = (G` (B |` x))) -> ((x e. On -> (B` x) = (G` (B |` x))) /\ (x e. On -> (F` x) = (G` (F |` x)))))
30		jcab 454	. . . . . . . . . . . . . . . . . . . 20 |- ((x e. On -> ((B` x) = (G` (B |` x)) /\ (F` x) = (G` (F |` x)))) <-> ((x e. On -> (B` x) = (G` (B |` x))) /\ (x e. On -> (F` x) = (G` (F |` x)))))
31	29, 30	sylibr 175	. . . . . . . . . . . . . . . . . . 19 |- ((x e. On -> (B` x) = (G` (B |` x))) -> (x e. On -> ((B` x) = (G` (B |` x)) /\ (F` x) = (G` (F |` x)))))
32		cleq12 1113	. . . . . . . . . . . . . . . . . . 19 |- (((B` x) = (G` (B |` x)) /\ (F` x) = (G` (F |` x))) -> ((B` x) = (F` x) <-> (G` (B |` x)) = (G` (F |` x))))
33	31, 32	syl6 23	. . . . . . . . . . . . . . . . . 18 |- ((x e. On -> (B` x) = (G` (B |` x))) -> (x e. On -> ((B` x) = (F` x) <-> (G` (B |` x)) = (G` (F |` x)))))
34	33	imp 277	. . . . . . . . . . . . . . . . 17 |- (((x e. On -> (B` x) = (G` (B |` x))) /\ x e. On) -> ((B` x) = (F` x) <-> (G` (B |` x)) = (G` (F |` x))))
35	34	adantl 305	. . . . . . . . . . . . . . . 16 |- ((((x e. On /\ B Fn On) /\ A.y e. x (B` y) = (F` y)) /\ ((x e. On -> (B` x) = (G` (B |` x))) /\ x e. On)) -> ((B` x) = (F` x) <-> (G` (B |` x)) = (G` (F |` x))))
36	27, 35	mpbird 171	. . . . . . . . . . . . . . 15 |- ((((x e. On /\ B Fn On) /\ A.y e. x (B` y) = (F` y)) /\ ((x e. On -> (B` x) = (G` (B |` x))) /\ x e. On)) -> (B` x) = (F` x))
37	36	exp43 301	. . . . . . . . . . . . . 14 |- ((x e. On /\ B Fn On) -> (A.y e. x (B` y) = (F` y) -> ((x e. On -> (B` x) = (G` (B |` x))) -> (x e. On -> (B` x) = (F` x)))))
38	37	com4t 40	. . . . . . . . . . . . 13 |- ((x e. On -> (B` x) = (G` (B |` x))) -> (x e. On -> ((x e. On /\ B Fn On) -> (A.y e. x (B` y) = (F` y) -> (B` x) = (F` x)))))
39	38	exp4a 295	. . . . . . . . . . . 12 |- ((x e. On -> (B` x) = (G` (B |` x))) -> (x e. On -> (x e. On -> (B Fn On -> (A.y e. x (B` y) = (F` y) -> (B` x) = (F` x))))))
40	39	pm2.43d 59	. . . . . . . . . . 11 |- ((x e. On -> (B` x) = (G` (B |` x))) -> (x e. On -> (B Fn On -> (A.y e. x (B` y) = (F` y) -> (B` x) = (F` x)))))
41	18, 40	syl 12	. . . . . . . . . 10 |- (A.x e. On (B` x) = (G` (B |` x)) -> (x e. On -> (B Fn On -> (A.y e. x (B` y) = (F` y) -> (B` x) = (F` x)))))
42	41	com3l 34	. . . . . . . . 9 |- (x e. On -> (B Fn On -> (A.x e. On (B` x) = (G` (B |` x)) -> (A.y e. x (B` y) = (F` y) -> (B