Theorem tz9.12lem3 4648

Description: Lemma for tz9.12 4649.

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 groups:   x,y,z,w,v,A   x,F,y

Proof of Theorem tz9.12lem3

Step	Hyp	Ref	Expression
1		fveq2 3721	. . . . . . . . . . . . . 14 |- (v = y -> (R1` v) = (R1` y))
2	1	eleq2d 1540	. . . . . . . . . . . . 13 |- (v = y -> (x e. (R1` v) <-> x e. (R1` y)))
3	2	rcla4ev 1875	. . . . . . . . . . . 12 |- ((y e. On /\ x e. (R1` y)) -> E.v e. On x e. (R1` v))
4		rabn0 2290	. . . . . . . . . . . 12 |- ({v e. On | x e. (R1` v)} =/= (/) <-> E.v e. On x e. (R1` v))
5	3, 4	sylibr 200	. . . . . . . . . . 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 1537	. . . . . . . . . . . . . . 15 |- (<.x, y>. e. F <-> <.x, y>. e. {<.z, w>. | w = |^|{v e. On | z e. (R1` v)}})
8		visset 1811	. . . . . . . . . . . . . . . 16 |- x e. V
9		visset 1811	. . . . . . . . . . . . . . . 16 |- y e. V
10		eleq1 1533	. . . . . . . . . . . . . . . . . . 19 |- (z = x -> (z e. (R1` v) <-> x e. (R1` v)))
11	10	rabbisdv 1805	. . . . . . . . . . . . . . . . . 18 |- (z = x -> {v e. On | z e. (R1` v)} = {v e. On | x e. (R1` v)})
12	11	inteqd 2535	. . . . . . . . . . . . . . . . 17 |- (z = x -> |^|{v e. On | z e. (R1` v)} = |^|{v e. On | x e. (R1` v)})
13	12	eqeq2d 1485	. . . . . . . . . . . . . . . 16 |- (z = x -> (w = |^|{v e. On | z e. (R1` v)} <-> w = |^|{v e. On | x e. (R1` v)}))
14		eqeq1 1480	. . . . . . . . . . . . . . . 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 2817	. . . . . . . . . . . . . . 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 173	. . . . . . . . . . . . . 14 |- (<.x, y>. e. F <-> y = |^|{v e. On | x e. (R1` v)})
17	16	exbii 1050	. . . . . . . . . . . . 13 |- (E.y<.x, y>. e. F <-> E.y y = |^|{v e. On | x e. (R1` v)})
18	8	eldm2 3305	. . . . . . . . . . . . 13 |- (x e. dom F <-> E.y<.x, y>. e. F)
19		isset 1812	. . . . . . . . . . . . 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 183	. . . . . . . . . . . 12 |- (x e. dom F <-> |^|{v e. On | x e. (R1` v)} e. V)
21		intex 2726	. . . . . . . . . . . 12 |- ({v e. On | x e. (R1` v)} =/= (/) <-> |^|{v e. On | x e. (R1` v)} e. V)
22	20, 21	bitr4 176	. . . . . . . . . . 11 |- (x e. dom F <-> {v e. On | x e. (R1` v)} =/= (/))
23	5, 22	sylibr 200	. . . . . . . . . 10 |- ((y e. On /\ x e. (R1` y)) -> x e. dom F)
24		funopabeq 3546	. . . . . . . . . . . 12 |- Fun {<.z, w>. | w = |^|{v e. On | z e. (R1` v)}}
25		funeq 3532	. . . . . . . . . . . . 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 7	. . . . . . . . . . . 12 |- (Fun F <-> Fun {<.z, w>. | w = |^|{v e. On | z e. (R1` v)}})
27	24, 26	mpbir 190	. . . . . . . . . . 11 |- Fun F
28		funfvima 3849	. . . . . . . . . . 11 |- ((Fun F /\ x e. dom F) -> (x e. A -> (F` x) e. (F"A)))
29	27, 28	mpan 694	. . . . . . . . . 10 |- (x e. dom F -> (x e. A -> (F` x) e. (F"A)))
30	23, 29	syl 10	. . . . . . . . 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 4646	. . . . . . . . . . . 12 |- (F"A) (_ On
33		onsucuni 3082	. . . . . . . . . . . 12 |- ((F"A) (_ On -> (F"A) (_ suc U.(F"A))
34	32, 33	ax-mp 7	. . . . . . . . . . 11 |- (F"A) (_ suc U.(F"A)
35	34	sseli 2063	. . . . . . . . . 10 |- ((F` x) e. (F"A) -> (F` x) e. suc U.(F"A))
36	31, 6	tz9.12lem2 4647	. . . . . . . . . . 11 |- suc U.(F"A) e. On
37		r1ord2 4643	. . . . . . . . . . 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 7	. . . . . . . . . 10 |- ((F` x) e. suc U.(F"A) -> (R1` (F` x)) (_ (R1` suc U.(F"A)))
39	35, 38	syl 10	. . . . . . . . 9 |- ((F` x) e. (F"A) -> (R1` (F` x)) (_ (R1` suc U.(F"A)))
40	30, 39	syl6 22	. . . . . . . 8 |- ((y e. On /\ x e. (R1` y)) -> (x e. A -> (R1` (F` x)) (_ (R1` suc U.(F"A))))
41	40	imp 350	. . . . . . 7 |- (((y e. On /\ x e. (R1` y)) /\ x e. A) -> (R1` (F` x)) (_ (R1` suc U.(F"A)))
42	12	fvopabg 3782	. . . . . . . . . . . . 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 694	. . . . . . . . . . . 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 3722	. . . . . . . . . . . 12 |- (F` x) = ({<.z, w>. | w = |^|{v e. On | z e. (R1` v)}}` x)
45	43, 44	syl5eq 1518	. . . . . . . . . . 11 |- (|^|{v e. On | x e. (R1` v)} e. V -> (F` x) = |^|{v e. On | x e. (R1` v)})
46	21, 45	sylbi 199	. . . . . . . . . 10 |- ({v e. On | x e. (R1` v)} =/= (/) -> (F` x) = |^|{v e. On | x e. (R1` v)})
47		ssrab2 2129	. . . . . . . . . . 11 |- {v e. On | x e. (R1` v)} (_ On
48		onint 3003	. . . . . . . . . . 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 694	. . . . . . . . . 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 1547	. . . . . . . . 9 |- ({v e. On | x e. (R1` v)} =/= (/) -> (F` x) e. {v e. On | x e. (R1` v)})
51		hbrab1 1771	. . . . . . . . . . . . . . . 16 |- (w e. {v e. On | z e. (R1` v)} -> A.v w e. {v e. On | z e. (R1` v)})
52	51	hbint 2540	. . . . . . . . . . . . . . 15 |- (w e. |^|{v e. On | z e. (R1` v)} -> A.v w e. |^|{v e. On | z e. (R1` v)})
53	52	hbeleq 1566	. . . . . . . . . . . . . 14 |- (w = |^|{v e. On | z e. (R1` v)} -> A.v w = |^|{v e. On | z e. (R1` v)})
54	53	hbopab 2809	. . . . . . . . . . . . 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, 54	hbxfr 1562	. . . . . . . . . . . 12 |- (y e. F -> A.v y e. F)
56		ax-17 970	. . . . . . . . . . . 12 |- (y e. x -> A.v y e. x)
57	55, 56	hbfv 3726	. . . . . . . . . . 11 |- (y e. (F` x) -> A.v y e. (F` x))
58		ax-17 970	. . . . . . . . . . 11 |- (y e. On -> A.v y e. On)
59		ax-17 970	. . . . . . . . . . . . 13 |- (y e. R1 -> A.v y e. R1)
60	59, 57	hbfv 3726	. . . . . . . . . . . 12 |- (y e. (R1` (F` x)) -> A.v y e. (R1` (F` x)))
61	56, 60	hbel 1565	. . . . . . . . . . 11 |- (x e. (R1` (F` x)) -> A.v x e. (R1` (F` x)))
62		fveq2 3721	. . . . . . . . . . . 12 |- (v = (F` x) -> (R1` v) = (R1` (F`