Theorem tfrlem1 3911

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 groups:   x,A   x,B   x,F   x,G

Proof of Theorem tfrlem1

Step	Hyp	Ref	Expression
1		ssid 2080	. 2 |- A (_ A
2		sseq1 2082	. . . . 5 |- (y = A -> (y (_ A <-> A (_ A))
3		raleq1 1786	. . . . . 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		raleq1 1786	. . . . . 6 |- (y = A -> (A.x e. y (F` x) = (G` x) <-> A.x e. A (F` x) = (G` x)))
5	3, 4	imbi12d 626	. . . . 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 626	. . . 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 612	. . 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 2082	. . . . . . . 8 |- (y = z -> (y (_ A <-> z (_ A))
9	8	anbi2d 616	. . . . . . 7 |- (y = z -> (((F Fn A /\ G Fn A) /\ y (_ A) <-> ((F Fn A /\ G Fn A) /\ z (_ A)))
10		raleq1 1786	. . . . . . 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 628	. . . . . 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		raleq1 1786	. . . . . 6 |- (y = z -> (A.x e. y (F` x) = (G` x) <-> A.x e. z (F` x) = (G` x)))
13	11, 12	imbi12d 626	. . . . 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 3000	. . . . . . . . . . 11 |- (y e. On -> (z e. y -> z (_ y))
15		sstr2 2071	. . . . . . . . . . . . 13 |- (z (_ y -> (y (_ A -> z (_ A))
16	15	anim2d 561	. . . . . . . . . . . 12 |- (z (_ y -> (((F Fn A /\ G Fn A) /\ y (_ A) -> ((F Fn A /\ G Fn A) /\ z (_ A)))
17		ax-17 971	. . . . . . . . . . . . 13 |- (z (_ y -> A.x z (_ y)
18		hbra1 1687	. . . . . . . . . . . . 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 2063	. . . . . . . . . . . . . 14 |- (z (_ y -> (x e. z -> x e. y))
20		ra4 1694	. . . . . . . . . . . . . 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 57	. . . . . . . . . . . . 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 1717	. . . . . . . . . . . 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 558	. . . . . . . . . . 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 22	. . . . . . . . . 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 1718	. . . . . . . 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 3000	. . . . . . . . . . . . . . . . . 18 |- (y e. On -> (x e. y -> x (_ y))
28		sstr2 2071	. . . . . . . . . . . . . . . . . . 19 |- (x (_ y -> (y (_ A -> x (_ A))
29		eqeq12 1487	. . . . . . . . . . . . . . . . . . . . . 22 |- (((F` x) = (B` (F |` x)) /\ (G` x) = (B` (G |` x))) -> ((F` x) = (G` x) <-> (B` (F |` x)) = (B` (G |` x))))
30		fvreseq 3799	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((F Fn A /\ G