Theorem tz9.12lem3 5772

Description: Lemma for tz9.12 5773.

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		funfvima 4828	. . . . . . . . . 10 |- ((Fun F /\ x e. dom F) -> (x e. A -> (F` x) e. (F"A)))
2		funopabeq 4456	. . . . . . . . . . 11 |- Fun {<.z, w>. | w = |^|{v e. On | z e. (R1` v)}}
3		tz9.12lem.2	. . . . . . . . . . . 12 |- F = {<.z, w>. | w = |^|{v e. On | z e. (R1` v)}}
4		funeq 4441	. . . . . . . . . . . 12 |- (F = {<.z, w>. | w = |^|{v e. On | z e. (R1` v)}} -> (Fun F <-> Fun {<.z, w>. | w = |^|{v e. On | z e. (R1` v)}}))
5	3, 4	ax-mp 7	. . . . . . . . . . 11 |- (Fun F <-> Fun {<.z, w>. | w = |^|{v e. On | z e. (R1` v)}})
6	2, 5	mpbir 207	. . . . . . . . . 10 |- Fun F
7		fveq2 4681	. . . . . . . . . . . . . 14 |- (v = y -> (R1` v) = (R1` y))
8	7	eleq2d 1964	. . . . . . . . . . . . 13 |- (v = y -> (x e. (R1` v) <-> x e. (R1` y)))
9	8	rcla4ev 2381	. . . . . . . . . . . 12 |- ((y e. On /\ x e. (R1` y)) -> E.v e. On x e. (R1` v))
10		rabn0 2893	. . . . . . . . . . . 12 |- ({v e. On | x e. (R1` v)} =/= (/) <-> E.v e. On x e. (R1` v))
11	9, 10	sylibr 217	. . . . . . . . . . 11 |- ((y e. On /\ x e. (R1` y)) -> {v e. On | x e. (R1` v)} =/= (/))
12	3	eleq2i 1961	. . . . . . . . . . . . . . 15 |- (<.x, y>. e. F <-> <.x, y>. e. {<.z, w>. | w = |^|{v e. On | z e. (R1` v)}})
13		visset 2295	. . . . . . . . . . . . . . . 16 |- x e. _V
14		visset 2295	. . . . . . . . . . . . . . . 16 |- y e. _V
15		eleq1 1957	. . . . . . . . . . . . . . . . . . 19 |- (z = x -> (z e. (R1` v) <-> x e. (R1` v)))
16	15	rabbidv 2287	. . . . . . . . . . . . . . . . . 18 |- (z = x -> {v e. On | z e. (R1` v)} = {v e. On | x e. (R1` v)})
17	16	inteqd 3219	. . . . . . . . . . . . . . . . 17 |- (z = x -> |^|{v e. On | z e. (R1` v)} = |^|{v e. On | x e. (R1` v)})
18	17	eqeq2d 1895	. . . . . . . . . . . . . . . 16 |- (z = x -> (w = |^|{v e. On | z e. (R1` v)} <-> w = |^|{v e. On | x e. (R1` v)}))
19		eqeq1 1890	. . . . . . . . . . . . . . . 16 |- (w = y -> (w = |^|{v e. On | x e. (R1` v)} <-> y = |^|{v e. On | x e. (R1` v)}))
20	13, 14, 18, 19	opelopab 3570	. . . . . . . . . . . . . . 15 |- (<.x, y>. e. {<.z, w>. | w = |^|{v e. On | z e. (R1` v)}} <-> y = |^|{v e. On | x e. (R1` v)})
21	12, 20	bitri 190	. . . . . . . . . . . . . 14 |- (<.x, y>. e. F <-> y = |^|{v e. On | x e. (R1` v)})
22	21	exbii 1398	. . . . . . . . . . . . 13 |- (E.y<.x, y>. e. F <-> E.y y = |^|{v e. On | x e. (R1` v)})
23	13	eldm2 4154	. . . . . . . . . . . . 13 |- (x e. dom F <-> E.y<.x, y>. e. F)
24		isset 2296	. . . . . . . . . . . . 13 |- (|^|{v e. On | x e. (R1` v)} e. _V <-> E.y y = |^|{v e. On | x e. (R1` v)})
25	22, 23, 24	3bitr4i 200	. . . . . . . . . . . 12 |- (x e. dom F <-> |^|{v e. On | x e. (R1` v)} e. _V)
26		intex 3465	. . . . . . . . . . . 12 |- ({v e. On | x e. (R1` v)} =/= (/) <-> |^|{v e. On | x e. (R1` v)} e. _V)
27	25, 26	bitr4i 193	. . . . . . . . . . 11 |- (x e. dom F <-> {v e. On | x e. (R1` v)} =/= (/))
28	11, 27	sylibr 217	. . . . . . . . . 10 |- ((y e. On /\ x e. (R1` y)) -> x e. dom F)
29	1, 6, 28	sylancr 526	. . . . . . . . 9 |- ((y e. On /\ x e. (R1` y)) -> (x e. A -> (F` x) e. (F"A)))
30		tz9.12lem.1	. . . . . . . . . . . . 13 |- A e. _V
31	30, 3	tz9.12lem1 5770	. . . . . . . . . . . 12 |- (F"A) C_ On
32		onsucuni 3907	. . . . . . . . . . . 12 |- ((F"A) C_ On -> (F"A) C_ suc U.(F"A))
33	31, 32	ax-mp 7	. . . . . . . . . . 11 |- (F"A) C_ suc U.(F"A)
34	33	sseli 2617	. . . . . . . . . 10 |- ((F` x) e. (F"A) -> (F` x) e. suc U.(F"A))
35	30, 3	tz9.12lem2 5771	. . . . . . . . . . 11 |- suc U.(F"A) e. On
36		r1ord2 5767	. . . . . . . . . . 11 |- (suc U.(F"A) e. On -> ((F` x) e. suc U.(F"A) -> (R1` (F` x)) C_ (R1` suc U.(F"A))))
37	35, 36	ax-mp 7	. . . . . . . . . 10 |- ((F` x) e. suc U.(F"A) -> (R1` (F` x)) C_ (R1` suc U.(F"A)))
38	34, 37	syl 12	. . . . . . . . 9 |- ((F` x) e. (F"A) -> (R1` (F` x)) C_ (R1` suc U.(F"A)))
39	29, 38	syl6 25	. . . . . . . 8 |- ((y e. On /\ x e. (R1` y)) -> (x e. A -> (R1` (F` x)) C_ (R1` suc U.(F"A))))
40	39	imp 377	. . . . . . 7 |- (((y e. On /\ x e. (R1` y)) /\ x e. A) -> (R1` (F` x)) C_ (R1` suc U.(F"A)))
41	17	fvopabg 4748	. . . . . . . . . . . . 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)})
42	13, 41	mpan 759	. . . . . . . . . . . 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)})
43	3	fveq1i 4682	. . . . . . . . . . . 12 |- (F` x) = ({<.z, w>. | w = |^|{v e. On | z e. (R1` v)}}` x)
44	42, 43	syl5eq 1940	. . . . . . . . . . 11 |- (|^|{v e. On | x e. (R1` v)} e. _V -> (F` x) = |^|{v e. On | x e. (R1` v)})
45	26, 44	sylbi 216	. . . . . . . . . 10 |- ({v e. On | x e. (R1` v)} =/= (/) -> (F` x) = |^|{v e. On | x e. (R1` v)})
46		ssrab2 2692	. . . . . . . . . . 11 |- {v e. On | x e. (R1` v)} C_ On
47		onint 3876	. . . . . . . . . . 11 |- (({v e. On | x e. (R1` v)} C_ On /\ {v e. On | x e. (R1` v)} =/= (/)) -> |^|{v e. On | x e. (R1` v)} e. {v e. On | x e. (R1` v)})
48	46, 47	mpan 759	. . . . . . . . . 10 |- ({v e. On | x e. (R1` v)} =/= (/) -> |^|{v e. On | x e. (R1` v)} e. {v e. On | x e. (R1` v)})
49	45, 48	eqeltrd 1971	. . . . . . . . 9 |- ({v e. On | x e. (R1` v)} =/= (/) -> (F` x) e. {v e. On | x e. (R1` v)})
50		hbrab1 2257	. . . . . . . . . . . . . . . 16 |- (w e. {v e. On | z e. (R1` v)} -> A.v w e. {v e. On | z e. (R1` v)})
51	50	hbint 3225	. . . . . . . . . . . . . . 15 |- (w e. |^|{v e. On | z e. (R1` v)} -> A.v w e. |^|{v e. On | z e. (R1` v)})
52	51	hbeleq 1997	. . . . . . . . . . . . . 14 |- (w = |^|{v e. On | z e. (R1` v)} -> A.v w = |^|{v e. On | z e. (R1` v)})
53	52	hbopab 3560	. . . . . . . . . . . . 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)}})
54	3, 53	hbxfr 1992	. . . . . . . . . . . 12 |- (y e. F -> A.v y e. F)
55		ax-17 1317	. . . . . . . . . . . 12 |- (y e. x -> A.v y e. x)
56	54, 55	hbfv 4686	. . . . . . . . . . 11 |- (y e. (F` x) -> A.v y e. (F` x))
57		ax-17 1317	. . . . . . . . . . 11 |- (y e. On -> A.v y e. On)
58		ax-17 1317	. . . . . . . . . . . . 13 |- (y e. R1 -> A.v y e. R1)
59	58, 56	hbfv 4686	. . . . . . . . . . . 12 |- (y e. (R1` (F` x)) -> A.v y e. (R1` (F` x)))
60	55, 59	hbel 1996	. . . . . . . . . . 11 |- (x e. (R1` (F` x)) -> A.v x e. (R1` (F` x)))
61		fveq2 4681	. . . . . . . . . . . 12 |- (v = (F` x) -> (R1` v) = (R1` (F` x)))
62	61	eleq2d 1964	. . . . . . . . . . 11 |- (v = (F` x) -> (x e. (R1` v) <-> x e. (R1` (F` x))))
63	56, 57, 60, 62	elrabf 2413	. . . . . . . . . 10 |- ((F` x) e. {v e. On | x e. (R1` v)} <-> ((F` x) e. On /\ x e. (R1` (F` x))))
64	63	simprbi 353	. . . . . . . . 9 |- ((F` x) e. {v e. On | x e. (R1` v)} -> x e. (R1` (F` x)))
65	11, 49, 64	3syl 24	. . . . . . . 8 |- ((y e. On /\ x e. (R1` y)) -> x e. (R1` (F` x)))
66	65	adantr 425	. . . . . . 7 |- (((y e. On /\ x e. (R1` y)) /\ x e. A) -> x e. (R1` (F` x)))
67	40, 66	sseldd 2620	. . . . . 6 |- (((y e. On /\ x e. (R1` y)) /\ x e. A) -> x e. (R1` suc U.(F"A)))
68	67	exp31 407	. . . . 5 |- (y e. On -> (x e. (R1` y) -> (x e. A -> x e. (R1` suc U.(F"A)))))
69	68	com3r 39	. . . 4 |- (x e. A -> (y e. On -> (x e. (R1` y) -> x e. (R1` suc U.(F"A)))))
70	69	r19.23adv 2215	. . 3 |- (x e. A -> (E.y e. On x e. (R1` y) -> x e. (R1` suc U.(F"A))))
71	70	ralimia 2166	. 2 |- (A.x e. A E.y e. On x e. (R1` y) -> A.x e. A x e. (R1` suc U.(F"A)))
72		r1suc 5763	. . . . 5 |- (suc U.(F"A) e. On -> (R1` suc suc U.(F"A)) = ~P(R1` suc U.(F"A)))
73	35, 72	ax-mp 7	. . . 4 |- (R1` suc suc U.(F"A)) = ~P(R1` suc U.(F"A))
74	73	eleq2i 1961	. . 3 |- (A e. (R1` suc suc U.(F"A)) <-> A e. ~P(R1` suc U.(F"A)))
75	30	elpw 3037	. . 3 |- (A e. ~P(R1` suc U.(F"A)) <-> A C_ (R1` suc U.(F"A)))
76		dfss3 2611	. . 3 |- (A C_ (R1` suc U.(F"A)) <-> A.x e. A x e. (R1` suc U.(F"A)))
77	74, 75, 76	3bitri 194	. 2 |- (A e. (R1` suc suc U.(F"A)) <-> A.x e. A x e. (R1` suc U.(F"A)))
78	71, 77	sylibr 217	1 |- (A.x e. A E.y e. On x e. (R1` y) -> A e. (R1` suc suc U.(F"A)))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   = wceq 1298   e. wcel 1300  E.wex 1326   =/= wne 2017  A.wral 2105  E.wrex 2106  {crab 2108  _Vcvv 2292   C_ wss 2593  (/)c0 2875  ~Pcpw 3032  <.cop 3046  U.cuni 3177  |^|cint 3214  {copab 3395  Oncon0 3657  suc csuc 3659  dom cdm 3986  "cima 3989  Fun wfun 3992  ` cfv 3998  R1cr1 5748

This theorem is referenced by:  tz9.12 5773

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3or 859  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-rab 2112  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-pss 2607  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-tp 3052  df-op 3053  df-uni 3178  df-int 3215  df-iun 3257  df-br 3339  df-opab 3396  df-tr 3412  df-eprel 3583  df-id 3586  df-po 3591  df-so 3604  df-fr 3625  df-we 3644  df-ord 3660  df-on 3661  df-lim 3662  df-suc 3663  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-fv 4014  df-rdg 5140  df-r1 5750

Copyright terms: Public domain