Theorem tz9.12lem3 3505

Description: Lemma for tz9.12 3506.

Hypotheses

Ref	Expression
tz9.12lem.1	|- A e. V
tz9.12lem.2	|- F = {<.z, w>. | w = |^|{v e. On | z e. (R1` v)}}

Assertion

Ref	Expression
tz9.12lem3	|- (A.x e. A E.y e. On x e. (R1` y) -> A e. (R1` suc suc U.(F"A)))

Distinct variable group(s):   x,y,z,w,v,A   x,F,y

Proof of Theorem tz9.12lem3

Step	Hyp	Ref	Expression
1		fveq2 2832	. . . . . . . . . . . . . 14 |- (v = y -> (R1` v) = (R1` y))
2	1	eleq2d 1156	. . . . . . . . . . . . 13 |- (v = y -> (x e. (R1` v) <-> x e. (R1` y)))
3	2	rcla4ev 1403	. . . . . . . . . . . 12 |- ((y e. On /\ x e. (R1` y)) -> E.v e. On x e. (R1` v))
4		rabn0 1716	. . . . . . . . . . . 12 |- (-. {v e. On | x e. (R1` v)} = (/) <-> E.v e. On x e. (R1` v))
5	3, 4	sylibr 175	. . . . . . . . . . 11 |- ((y e. On /\ x e. (R1` y)) -> -. {v e. On | x e. (R1` v)} = (/))
6		tz9.12lem.2	. . . . . . . . . . . . . . . 16 |- F = {<.z, w>. | w = |^|{v e. On | z e. (R1` v)}}
7	6	eleq2i 1153	. . . . . . . . . . . . . . 15 |- (<.x, y>. e. F <-> <.x, y>. e. {<.z, w>. | w = |^|{v e. On | z e. (R1` v)}})
8		visset 1350	. . . . . . . . . . . . . . . 16 |- x e. V
9		visset 1350	. . . . . . . . . . . . . . . 16 |- y e. V
10		eleq1 1149	. . . . . . . . . . . . . . . . . . 19 |- (z = x -> (z e. (R1` v) <-> x e. (R1` v)))
11	10	birabsdv 1344	. . . . . . . . . . . . . . . . . 18 |- (z = x -> {v e. On | z e. (R1` v)} = {v e. On | x e. (R1` v)})
12	11	inteqd 1970	. . . . . . . . . . . . . . . . 17 |- (z = x -> |^|{v e. On | z e. (R1` v)} = |^|{v e. On | x e. (R1` v)})
13	12	cleq2d 1112	. . . . . . . . . . . . . . . 16 |- (z = x -> (w = |^|{v e. On | z e. (R1` v)} <-> w = |^|{v e. On | x e. (R1` v)}))
14		cleq1 1107	. . . . . . . . . . . . . . . 16 |- (w = y -> (w = |^|{v e. On | x e. (R1` v)} <-> y = |^|{v e. On | x e. (R1` v)}))
15	8, 9, 13, 14	opelopab 2117	. . . . . . . . . . . . . . 15 |- (<.x, y>. e. {<.z, w>. | w = |^|{v e. On | z e. (R1` v)}} <-> y = |^|{v e. On | x e. (R1` v)})
16	7, 15	bitr 151	. . . . . . . . . . . . . 14 |- (<.x, y>. e. F <-> y = |^|{v e. On | x e. (R1` v)})
17	16	biex 733	. . . . . . . . . . . . 13 |- (E.y<.x, y>. e. F <-> E.y y = |^|{v e. On | x e. (R1` v)})
18	8	eldm2 2528	. . . . . . . . . . . . 13 |- (x e. dom F <-> E.y<.x, y>. e. F)
19		isset 1351	. . . . . . . . . . . . 13 |- (|^|{v e. On | x e. (R1` v)} e. V <-> E.y y = |^|{v e. On | x e. (R1` v)})
20	17, 18, 19	3bitr4 158	. . . . . . . . . . . 12 |- (x e. dom F <-> |^|{v e. On | x e. (R1` v)} e. V)
21		intex 1986	. . . . . . . . . . . 12 |- (-. {v e. On | x e. (R1` v)} = (/) <-> |^|{v e. On | x e. (R1` v)} e. V)
22	20, 21	bitr4 154	. . . . . . . . . . 11 |- (x e. dom F <-> -. {v e. On | x e. (R1` v)} = (/))
23	5, 22	sylibr 175	. . . . . . . . . 10 |- ((y e. On /\ x e. (R1` y)) -> x e. dom F)
24		funopabeq 2695	. . . . . . . . . . . 12 |- Fun {<.z, w>. | w = |^|{v e. On | z e. (R1` v)}}
25		funeq 2683	. . . . . . . . . . . . 13 |- (F = {<.z, w>. | w = |^|{v e. On | z e. (R1` v)}} -> (Fun F <-> Fun {<.z, w>. | w = |^|{v e. On | z e. (R1` v)}}))
26	6, 25	ax-mp 6	. . . . . . . . . . . 12 |- (Fun F <-> Fun {<.z, w>. | w = |^|{v e. On | z e. (R1` v)}})
27	24, 26	mpbir 165	. . . . . . . . . . 11 |- Fun F
28		funfvima 2904	. . . . . . . . . . 11 |- ((Fun F /\ x e. dom F) -> (x e. A -> (F` x) e. (F"A)))
29	27, 28	mpan 518	. . . . . . . . . 10 |- (x e. dom F -> (x e. A -> (F` x) e. (F"A)))
30	23, 29	syl 12	. . . . . . . . 9 |- ((y e. On /\ x e. (R1` y)) -> (x e. A -> (F` x) e. (F"A)))
31		tz9.12lem.1	. . . . . . . . . . . . 13 |- A e. V
32	31, 6	tz9.12lem1 3503	. . . . . . . . . . . 12 |- (F"A) (_ On
33		onsucuni 2335	. . . . . . . . . . . 12 |- ((F"A) (_ On -> (F"A) (_ suc U.(F"A))
34	32, 33	ax-mp 6	. . . . . . . . . . 11 |- (F"A) (_ suc U.(F"A)
35	34	sseli 1504	. . . . . . . . . 10 |- ((F` x) e. (F"A) -> (F` x) e. suc U.(F"A))
36	31, 6	tz9.12lem2 3504	. . . . . . . . . . 11 |- suc U.(F"A) e. On
37		r1ord2 3500	. . . . . . . . . . 11 |- (suc U.(F"A) e. On -> ((F` x) e. suc U.(F"A) -> (R1` (F` x)) (_ (R1` suc U.(F"A))))
38	36, 37	ax-mp 6	. . . . . . . . . 10 |- ((F` x) e. suc U.(F"A) -> (R1` (F` x)) (_ (R1` suc U.(F"A)))
39	35, 38	syl 12	. . . . . . . . 9 |- ((F` x) e. (F"A) -> (R1` (F` x)) (_ (R1` suc U.(F"A)))
40	30, 39	syl6 23	. . . . . . . 8 |- ((y e. On /\ x e. (R1` y)) -> (x e. A -> (R1` (F` x)) (_ (R1` suc U.(F"A))))
41	40	imp 277	. . . . . . 7 |- (((y e. On /\ x e. (R1` y)) /\ x e. A) -> (R1` (F` x)) (_ (R1` suc U.(F"A)))
42	12	fvopabg 2872	. . . . . . . . . . . . 13 |- ((x e. V /\ |^|{v e. On | x e. (R1` v)} e. V) -> ({<.z, w>. | w = |^|{v e. On | z e. (R1` v)}}` x) = |^|{v e. On | x e. (R1` v)})
43	8, 42	mpan 518	. . . . . . . . . . . 12 |- (|^|{v e. On | x e. (R1` v)} e. V -> ({<.z, w>. | w = |^|{v e. On | z e. (R1` v)}}` x) = |^|{v e. On | x e. (R1` v)})
44	6	fveq1i 2833	. . . . . . . . . . . 12 |- (F` x) = ({<.z, w>. | w = |^|{v e. On | z e. (R1` v)}}` x)
45	43, 44	syl5eq 1136	. . . . . . . . . . 11 |- (|^|{v e. On | x e. (R1` v)} e. V -> (F` x) = |^|{v e. On | x e. (R1` v)})
46	21, 45	sylbi 174	. . . . . . . . . 10 |- (-. {v e. On | x e. (R1` v)} = (/) -> (F` x) = |^|{v e. On | x e. (R1` v)})
47		ssrab 1556	. . . . . . . . . . 11 |- {v e. On | x e. (R1` v)} (_ On
48		onint 2261	. . . . . . . . . . 11 |- (({v e. On | x e. (R1` v)} (_ On /\ -. {v e. On | x e. (R1` v)} = (/)) -> |^|{v e. On | x e. (R1` v)} e. {v e. On | x e. (R1` v)})
49	47, 48	mpan 518	. . . . . . . . . 10 |- (-. {v e. On | x e. (R1` v)} = (/) -> |^|{v e. On | x e. (R1` v)} e. {v e. On | x e. (R1` v)})
50	46, 49	eqeltrd 1163	. . . . . . . . 9 |- (-. {v e. On | x e. (R1` v)} = (/) -> (F` x) e. {v e. On | x e. (R1` v)})
51		hbrab1 1310	. . . . . . . . . . . . . . . 16 |- (w e. {v e. On | z e. (R1` v)} -> A.v w e. {v e. On | z e. (R1` v)})
52	51	hbint 1975	. . . . . . . . . . . . . . 15 |- (w e. |^|{v e. On | z e. (R1` v)} -> A.v w e. |^|{v e. On | z e. (R1` v)})
53	52	hbeleq 1173	. . . . . . . . . . . . . 14 |- (w = |^|{v e. On | z e. (R1` v)} -> A.v w = |^|{v e. On | z e. (R1` v)})
54	53	hbopab 2111	. . . . . . . . . . . . 13 |- (y e. {<.z, w>. | w = |^|{v e. On | z e. (R1` v)}} -> A.v y e. {<.z, w>. | w = |^|{v e. On | z e. (R1` v)}})
55	6	eleq2i 1153	. . . . . . . . . . . . 13 |- (y e. F <-> y e. {<.z, w>. | w = |^|{v e. On | z e. (R1` v)}})
56	55	bial 695	. . . . . . . . . . . . 13 |- (A.v y e. F <-> A.v y e. {<.z, w>. | w = |^|{v e. On | z e. (R1` v)}})
57	54, 55, 56	3imtr4 192	. . . . . . . . . . . 12 |- (y e. F -> A.v y e. F)
58		ax-17 925	. . . . . . . . . . . 12 |- (y e. x -> A.v y e. x)
59	57, 58	hbfv 2837	. . . . . . . . . . 11 |- (y e. (F` x) -> A.v y e. (F` x))
60		ax-17 925	. . . . . . . . . . 11 |- (y e. On -> A.v y e. On)
61		ax-17 925	. . . . . . . . . . . . 13 |- (y e. R1 -> A.v y e. R1)
62	61, 59	hbfv 2837	. . . . . . . . . . . 12 |- (y e. (R1` (F` x)) -> A.v y e. (R1` (F` x)))
63	58, 62	hbel 1172	. . . . . . . . . . 11 |- (x e. (R1` (F` x)) -> A.v x e. (R1` (F` x)))
64		fveq2 2832	. . . . . . . . . . . 12 |- (v = (F` x) -> (R1`