Theorem tfrlem1 2949

Description: A technical lemma for transfinite recursion. Compare Lemma 1 of [TakeutiZaring] p. 47.

Assertion

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

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

Proof of Theorem tfrlem1

Step	Hyp	Ref	Expression
1		ssid 1519	. 2 |- A (_ A
2		sseq1 1521	. . . . 5 |- (y = A -> (y (_ A <-> A (_ A))
3		raleq 1324	. . . . . 6 |- (y = A -> (A.x e. y ((F` x) = (B` (F |` x)) /\ (G` x) = (B` (G |` x))) <-> A.x e. A ((F` x) = (B` (F |` x)) /\ (G` x) = (B` (G |` x)))))
4		raleq 1324	. . . . . 6 |- (y = A -> (A.x e. y (F` x) = (G` x) <-> A.x e. A (F` x) = (G` x)))
5	3, 4	imbi12d 474	. . . . 5 |- (y = A -> ((A.x e. y ((F` x) = (B` (F |` x)) /\ (G` x) = (B` (G |` x))) -> A.x e. y (F` x) = (G` x)) <-> (A.x e. A ((F` x) = (B` (F |` x)) /\ (G` x) = (B` (G |` x))) -> A.x e. A (F` x) = (G` x))))
6	2, 5	imbi12d 474	. . . 4 |- (y = A -> ((y (_ A -> (A.x e. y ((F` x) = (B` (F |` x)) /\ (G` x) = (B` (G |` x))) -> A.x e. y (F` x) = (G` x))) <-> (A (_ A -> (A.x e. A ((F` x) = (B` (F |` x)) /\ (G` x) = (B` (G |` x))) -> A.x e. A (F` x) = (G` x)))))
7	6	imbi2d 464	. . 3 |- (y = A -> (((F Fn A /\ G Fn A) -> (y (_ A -> (A.x e. y ((F` x) = (B` (F |` x)) /\ (G` x) = (B` (G |` x))) -> A.x e. y (F` x) = (G` x)))) <-> ((F Fn A /\ G Fn A) -> (A (_ A -> (A.x e. A ((F` x) = (B` (F |` x)) /\ (G` x) = (B` (G |` x))) -> A.x e. A (F` x) = (G` x))))))
8		sseq1 1521	. . . . . . . 8 |- (y = z -> (y (_ A <-> z (_ A))
9	8	anbi2d 468	. . . . . . 7 |- (y = z -> (((F Fn A /\ G Fn A) /\ y (_ A) <-> ((F Fn A /\ G Fn A) /\ z (_ A)))
10		raleq 1324	. . . . . . 7 |- (y = z -> (A.x e. y ((F` x) = (B` (F |` x)) /\ (G` x) = (B` (G |` x))) <-> A.x e. z ((F` x) = (B` (F |` x)) /\ (G` x) = (B` (G |` x)))))
11	9, 10	anbi12d 476	. . . . . 6 |- (y = z -> ((((F Fn A /\ G Fn A) /\ y (_ A) /\ A.x e. y ((F` x) = (B` (F |` x)) /\ (G` x) = (B` (G |` x)))) <-> (((F Fn A /\ G Fn A) /\ z (_ A) /\ A.x e. z ((F` x) = (B` (F |` x)) /\ (G` x) = (B` (G |` x))))))
12		raleq 1324	. . . . . 6 |- (y = z -> (A.x e. y (F` x) = (G` x) <-> A.x e. z (F` x) = (G` x)))
13	11, 12	imbi12d 474	. . . . 5 |- (y = z -> (((((F Fn A /\ G Fn A) /\ y (_ A) /\ A.x e. y ((F` x) = (B` (F |` x)) /\ (G` x) = (B` (G |` x)))) -> A.x e. y (F` x) = (G` x)) <-> ((((F Fn A /\ G Fn A) /\ z (_ A) /\ A.x e. z ((F` x) = (B` (F |` x)) /\ (G` x) = (B` (G |` x)))) -> A.x e. z (F` x) = (G` x))))
14		onelsst 2255	. . . . . . . . . . 11 |- (y e. On -> (z e. y -> z (_ y))
15		sstr2 1510	. . . . . . . . . . . . 13 |- (z (_ y -> (y (_ A -> z (_ A))
16	15	anim2d 433	. . . . . . . . . . . 12 |- (z (_ y -> (((F Fn A /\ G Fn A) /\ y (_ A) -> ((F Fn A /\ G Fn A) /\ z (_ A)))
17		ax-17 925	. . . . . . . . . . . . 13 |- (z (_ y -> A.x z (_ y)
18		hbra1 1237	. . . . . . . . . . . . 13 |- (A.x e. y ((F` x) = (B` (F |` x)) /\ (G` x) = (B` (G |` x))) -> A.xA.x e. y ((F` x) = (B` (F |` x)) /\ (G` x) = (B` (G |` x))))
19		ssel 1502	. . . . . . . . . . . . . 14 |- (z (_ y -> (x e. z -> x e. y))
20		ra4 1243	. . . . . . . . . . . . . 14 |- (A.x e. y ((F` x) = (B` (F |` x)) /\ (G` x) = (B` (G |` x))) -> (x e. y -> ((F` x) = (B` (F |` x)) /\ (G` x) = (B` (G |` x)))))
21	19, 20	syl9 55	. . . . . . . . . . . . 13 |- (z (_ y -> (A.x e. y ((F` x) = (B` (F |` x)) /\ (G` x) = (B` (G |` x))) -> (x e. z -> ((F` x) = (B` (F |` x)) /\ (G` x) = (B` (G |` x))))))
22	17, 18, 21	r19.21ad 1261	. . . . . . . . . . . 12 |- (z (_ y -> (A.x e. y ((F` x) = (B` (F |` x)) /\ (G` x) = (B` (G |` x))) -> A.x e. z ((F` x) = (B` (F |` x)) /\ (G` x) = (B` (G |` x)))))
23	16, 22	anim12d 431	. . . . . . . . . . 11 |- (z (_ y -> ((((F Fn A /\ G Fn A) /\ y (_ A) /\ A.x e. y ((F` x) = (B` (F |` x)) /\ (G` x) = (B` (G |` x)))) -> (((F Fn A /\ G Fn A) /\ z (_ A) /\ A.x e. z ((F` x) = (B` (F |` x)) /\ (G` x) = (B` (G |` x))))))
24	14, 23	syl6 23	. . . . . . . . . 10 |- (y e. On -> (z e. y -> ((((F Fn A /\ G Fn A) /\ y (_ A) /\ A.x e. y ((F` x) = (B` (F |` x)) /\ (G` x) = (B` (G |` x)))) -> (((F Fn A /\ G Fn A) /\ z (_ A) /\ A.x e. z ((F` x) = (B` (F |` x)) /\ (G` x) = (B` (G |` x)))))))
25	24	com23 32	. . . . . . . . 9 |- (y e. On -> ((((F Fn A /\ G Fn A) /\ y (_ A) /\ A.x e. y ((F` x) = (B` (F |` x)) /\ (G` x) = (B` (G |` x)))) -> (z e. y -> (((F Fn A /\ G Fn A) /\ z (_ A) /\ A.x e. z ((F` x) = (B` (F |` x)) /\ (G` x) = (B` (G |` x)))))))
26	25	r19.21adv 1262	. . . . . . . 8 |- (y e. On -> ((((F Fn A /\ G Fn A) /\ y (_ A) /\ A.x e. y ((F` x) = (B` (F |` x)) /\ (G` x) = (B` (G |` x)))) -> A.z e. y (((F Fn A /\ G Fn A) /\ z (_ A) /\ A.x e. z ((F` x) = (B` (F |` x)) /\ (G` x) = (B` (G |` x))))))
27		onelsst 2255	. . . . . . . . . . . . . . . . . 18 |- (y e. On -> (x e. y -> x (_ y))
28		sstr2 1510	. . . . . . . . . . . . . . . . . . 19 |- (x (_ y -> (y (_ A -> x (_ A))
29		cleq12 1113	. . . . . . . . . . . . . . . . . . . . . 22 |- (((F` x) = (B` (F |` x)) /\ (G` x) = (B` (G |` x))) -> ((F` x) = (G` x) <-> (B` (F |` x)) = (B` (G |` x))))
30		fvreseq 2882	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((F Fn A /\ G Fn A) /\ x (_ A) -> ((F |` x) = (G |` x) <-> A.w e. x (F` w) = (G` w))