Theorem tfrlem8 2956

Description: Lemma for transfinite recursion. The domain of F is ordinal.

Hypotheses

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

Assertion

Ref	Expression
tfrlem8	|- Ord dom F

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

Proof of Theorem tfrlem8

Step	Hyp	Ref	Expression
1		dftr2 2043	. . 3 |- (Tr dom F <-> A.vA.w((v e. w /\ w e. dom F) -> v e. dom F))
2		visset 1350	. . . . . . . . . 10 |- w e. V
3	2	eldm2 2528	. . . . . . . . 9 |- (w e. dom F <-> E.z<.w, z>. e. F)
4		tfrlem.2	. . . . . . . . . . . . 13 |- F = U.A
5		tfrlem.1	. . . . . . . . . . . . . 14 |- A = {f | E.x e. On (f Fn x /\ A.y e. x (f` y) = (G` (f |` y)))}
6	5	unieqi 1928	. . . . . . . . . . . . 13 |- U.A = U.{f | E.x e. On (f Fn x /\ A.y e. x (f` y) = (G` (f |` y)))}
7	4, 6	eqtr 1119	. . . . . . . . . . . 12 |- F = U.{f | E.x e. On (f Fn x /\ A.y e. x (f` y) = (G` (f |` y)))}
8	7	eleq2i 1153	. . . . . . . . . . 11 |- (<.w, z>. e. F <-> <.w, z>. e. U.{f | E.x e. On (f Fn x /\ A.y e. x (f` y) = (G` (f |` y)))})
9		eluniab 1926	. . . . . . . . . . 11 |- (<.w, z>. e. U.{f | E.x e. On (f Fn x /\ A.y e. x (f` y) = (G` (f |` y)))} <-> E.f(<.w, z>. e. f /\ E.x e. On (f Fn x /\ A.y e. x (f` y) = (G` (f |` y)))))
10	8, 9	bitr 151	. . . . . . . . . 10 |- (<.w, z>. e. F <-> E.f(<.w, z>. e. f /\ E.x e. On (f Fn x /\ A.y e. x (f` y) = (G` (f |` y)))))
11	10	biex 733	. . . . . . . . 9 |- (E.z<.w, z>. e. F <-> E.zE.f(<.w, z>. e. f /\ E.x e. On (f Fn x /\ A.y e. x (f` y) = (G` (f |` y)))))
12	3, 11	bitr 151	. . . . . . . 8 |- (w e. dom F <-> E.zE.f(<.w, z>. e. f /\ E.x e. On (f Fn x /\ A.y e. x (f` y) = (G` (f |` y)))))
13		r19.42v 1303	. . . . . . . . . 10 |- (E.x e. On (<.w, z>. e. f /\ (f Fn x /\ A.y e. x (f` y) = (G` (f |` y)))) <-> (<.w, z>. e. f /\ E.x e. On (f Fn x /\ A.y e. x (f` y) = (G` (f |` y)))))
14		visset 1350	. . . . . . . . . . . . . . . . 17 |- z e. V
15	2, 14	fnop 2727	. . . . . . . . . . . . . . . 16 |- ((f Fn x /\ <.w, z>. e. f) -> w e. x)
16	15	ancoms 334	. . . . . . . . . . . . . . 15 |- ((<.w, z>. e. f /\ f Fn x) -> w e. x)
17	16	adantrr 312	. . . . . . . . . . . . . 14 |- ((<.w, z>. e. f /\ (f Fn x /\ A.y e. x (f` y) = (G` (f |` y)))) -> w e. x)
18	17	adantl 305	. . . . . . . . . . . . 13 |- ((x e. On /\ (<.w, z>. e. f /\ (f Fn x /\ A.y e. x (f` y) = (G` (f |` y))))) -> w e. x)
19		ra4e 1244	. . . . . . . . . . . . . . . 16 |- ((x e. On /\ (f Fn x /\ A.y e. x (f` y) = (G` (f |` y)))) -> E.x e. On (f Fn x /\ A.y e. x (f` y) = (G` (f |` y))))
20	5	cleqabi 1176	. . . . . . . . . . . . . . . . 17 |- (f e. A <-> E.x e. On (f Fn x /\ A.y e. x (f` y) = (G` (f |` y))))
21		elssuni 1940	. . . . . . . . . . . . . . . . . 18 |- (f e. A -> f (_ U.A)
22	4	sseq2i 1525	. . . . . . . . . . . . . . . . . . 19 |- (f (_ F <-> f (_ U.A)
23		dmss 2530	. . . . . . . . . . . . . . . . . . 19 |- (f (_ F -> dom f (_ dom F)
24	22, 23	sylbir 176	. . . . . . . . . . . . . . . . . 18 |- (f (_ U.A -> dom f (_ dom F)
25	21, 24	syl 12	. . . . . . . . . . . . . . . . 17 |- (f e. A -> dom f (_ dom F)
26	20, 25	sylbir 176	. . . . . . . . . . . . . . . 16 |- (E.x e. On (f Fn x /\ A.y e. x (f` y) = (G` (f |` y))) -> dom f (_ dom F)
27	19, 26	syl 12	. . . . . . . . . . . . . . 15 |- ((x e. On /\ (f Fn x /\ A.y e. x (f` y) = (G` (f |` y)))) -> dom f (_ dom F)
28		fndm 2723	. . . . . . . . . . . . . . . . 17 |- (f Fn x -> dom f = x)
29	28	sseq1d 1527	. . . . . . . . . . . . . . . 16 |- (f Fn x -> (dom f (_ dom F <-> x (_ dom F))
30	29	ad2antrl 322	. . . . . . . . . . . . . . 15 |- ((x e. On /\ (f Fn x /\ A.y e. x (f` y) = (G` (f |` y)))) -> (dom f (_ dom F <-> x (_ dom F))
31	27, 30	mpbid 170	. . . . . . . . . . . . . 14 |- ((x e. On /\ (f Fn x /\ A.y e. x (f` y) = (G` (f |` y)))) -> x (_ dom F)
32	31	adantrl 311	. . . . . . . . . . . . 13 |- ((x e. On /\ (<.w, z>. e. f /\ (f Fn x /\ A.y e. x (f` y) = (G` (f |` y))))) -> x (_ dom F)
33	18, 32	jca 236	. . . . . . . . . . . 12 |- ((x e. On /\ (<.w, z>. e. f /\ (f Fn x /\ A.y e. x (f` y) = (G` (f |` y))))) -> (w e. x /\ x (_ dom F))
34	33	exp 291	. . . . . . . . . . 11 |- (x e. On -> ((<.w, z>. e. f /\ (f Fn x /\ A.y e. x (f` y) = (G` (f |` y)))) -> (w e. x /\ x (_ dom F)))
35	34	r19.22i 1273	. . . . . . . . . 10 |- (E.x e. On (<.w, z>. e. f /\ (f Fn x /\ A.y e. x (f` y) = (G` (f |` y)))) -> E.x e. On (w e. x /\ x (_ dom F))
36	13, 35	sylbir 176	. . . . . . . . 9 |- ((<.w, z>. e. f /\ E.x e. On (f Fn x /\ A.y e. x (f` y) = (G` (f |` y)))) -> E.x e. On (w e. x /\ x (_ dom F))
37	36	19.23aivv 953	. . . . . . . 8 |- (E.zE.f(<.w, z>. e. f /\ E.x e. On (f Fn x /\ A.y e. x (f` y) = (G` (f |` y)))) -> E.x e. On (w e. x /\ x (_ dom F))
38	12, 37	sylbi 174	. . . . . . 7 |- (w e. dom F -> E.x e. On (w e. x /\ x (_ dom F))
39	38	anim2i 270	. . . . . 6 |- ((v e. w /\ w e. dom F) -> (v e. w /\ E.x e. On (w e. x /\ x (_ dom F)))
40		r19.42v 1303	. . . . . 6 |- (E.x e. On (v e. w /\ (w e. x /\ x (_ dom F)) <-> (v e. w /\ E.x e. On (w e. x /\ x (_ dom F)))
41	39, 40	sylibr 175	. . . . 5 |- ((v e. w /\ w e. dom F) -> E.x e. On (v e. w /\ (w e. x /\ x (_ dom F)))
42		ontr1 2258	. . . . . . . . . 10 |- (x e. On -> ((v e. w /\ w e. x) -> v e. x))
43		ssel 1502	. . . . . . . . . 10 |- (x (_ dom F -> (v e. x -> v e. dom F))
44	42, 43	sylan9r 360	. . . . . . . . 9 |- ((x (_ dom F /\ x e. On) -> ((v e. w /\ w e. x) -> v e. dom F))
45	44	exp4b 296	. . . . . . . 8 |- (x (_ dom F -> (x e. On -> (v e. w -> (w e. x -> v e. dom F))))
46	45	com4l 39	. . . . . . 7 |- (x e. On -> (v e. w -> (w e. x -> (x (_ dom F -> v e. dom F))))
47	46	imp4d 285	. . . . . 6 |- (x e. On -> ((v e. w /\ (w e. x /\ x (_ dom F)) -> v e. dom F))
48	47	r19.23aiv 1284	. . . . 5 |- (E.x e. On (v e. w /\ (w e. x /\ x (_ dom F)) -> v e. dom F)
49	41, 48	syl 12	. . . 4 |- ((v e. w /\ w e. dom F) -> v e. dom F)
50	49	ax-gen 677	. . 3 |- A.w((v e. w /\ w e. dom F) -> v e. dom F)
51	1, 50	mpgbir 686	. 2 |- Tr dom F
52		onelon 2223	. . . . . . . . . . . . . 14 |- ((x e. On /\ w e. x) -> w e. On)
53	52, 15	sylan2 346	. . . . . . . . . . . . 13 |- ((x e. On /\ (f Fn x /\ <.w, z>. e. f)) -> w e. On)
54	53	exp32 294	. . . . . . . . . . . 12 |- (x e. On -> (f Fn x -> (<.w, z>. e. f -> w e. On)))
55	54	com12 13	. . . . . . . . . . 11 |- (f Fn x -> (x e. On -> (<.w, z>. e. f -> w e. On)))
56	55	adantr 306	. . . . . . . . . 10 |- ((f Fn x /\ A.y e. x (f` y) = (G` (f |` y))) -> (x e. On -> (<.w, z>. e. f -> w e. On)))
57	56	com13 33	. . . . . . . . 9 |- (<.w, z>. e. f -> (x e. On -> ((f Fn x /\ A.y e. x (f` y) = (G` (f |` y))) -> w e. On)))
58	57	r19.23adv 1286	. . . . . . . 8 |- (<.w, z>. e. f -> (E.x e. On (f Fn x /\ A.y e. x (f` y) = (G` (f |` y))) -> w e. On))
59	58	imp 277	. . . . . . 7 |- ((<.w, z>. e. f /\ E.x e. On (f Fn x /\ A.y e. x (f` y) = (G` (f |` y)