Theorem ordtypelem4 5687

Description: Lemma for ordtype 5691. There is a smallest ordinal number whose image has no upper bounds in A.

Hypotheses

Ref	Expression
ordtypelem.1	|- A e. _V
ordtypelem.2	|- B = {h | E.b e. On (h Fn b /\ A.c e. b (h` c) = (G` (h |` c)))}
ordtypelem.3	|- F = U.B
ordtypelem.4	|- C = {w e. A | A.j e. ran h jRw}
ordtypelem.5	|- D = {w e. A | A.j e. (F"x)jRw}
ordtypelem.6	|- G = {<.h, c>. | c = U.{v e. C | A.u e. C -. uRv}}
ordtypelem.7	|- H = {w e. A | A.j e. (F"y)jRw}

Assertion

Ref	Expression
ordtypelem4	|- (R We A -> E.x e. On (D = (/) /\ A.y e. x H =/= (/)))

Distinct variable groups:   b,c,h,j,u,v,w,x,y,A   B,b,c,h,x,y   C,c,u   D,h,j,u,v,w,y   F,b,c,h,j,u,v,w,x,y   G,b,c,h   h,H,j,u,v,w,x   R,b,c,h,j,u,v,w,x,y

Proof of Theorem ordtypelem4

Step	Hyp	Ref	Expression
1		pm3.24 720	. . 3 |- -. (ran F e. _V /\ -. ran F e. _V)
2		ax-17 1317	. . . . . . . . . . 11 |- (R We A -> A.x R We A)
3		hba1 1350	. . . . . . . . . . 11 |- (A.x(x e. On -> D =/= (/)) -> A.xA.x(x e. On -> D =/= (/)))
4	2, 3	hban 1356	. . . . . . . . . 10 |- ((R We A /\ A.x(x e. On -> D =/= (/))) -> A.x(R We A /\ A.x(x e. On -> D =/= (/))))
5		ax-17 1317	. . . . . . . . . 10 |- (r e. A -> A.x r e. A)
6		eleq1 1957	. . . . . . . . . . . . . . . 16 |- ((F` x) = r -> ((F` x) e. A <-> r e. A))
7		ordtypelem.1	. . . . . . . . . . . . . . . . . . 19 |- A e. _V
8		ordtypelem.2	. . . . . . . . . . . . . . . . . . 19 |- B = {h | E.b e. On (h Fn b /\ A.c e. b (h` c) = (G` (h |` c)))}
9		ordtypelem.3	. . . . . . . . . . . . . . . . . . 19 |- F = U.B
10		ordtypelem.4	. . . . . . . . . . . . . . . . . . 19 |- C = {w e. A | A.j e. ran h jRw}
11		ordtypelem.5	. . . . . . . . . . . . . . . . . . 19 |- D = {w e. A | A.j e. (F"x)jRw}
12		ordtypelem.6	. . . . . . . . . . . . . . . . . . 19 |- G = {<.h, c>. | c = U.{v e. C | A.u e. C -. uRv}}
13		ordtypelem.7	. . . . . . . . . . . . . . . . . . 19 |- H = {w e. A | A.j e. (F"y)jRw}
14	7, 8, 9, 10, 11, 12, 13	ordtypelem1 5684	. . . . . . . . . . . . . . . . . 18 |- ((x e. On /\ R We A /\ D =/= (/)) -> (F` x) e. D)
15	14	3expb 1068	. . . . . . . . . . . . . . . . 17 |- ((x e. On /\ (R We A /\ D =/= (/))) -> (F` x) e. D)
16		ssrab2 2692	. . . . . . . . . . . . . . . . . . 19 |- {w e. A | A.j e. (F"x)jRw} C_ A
17	11, 16	eqsstri 2647	. . . . . . . . . . . . . . . . . 18 |- D C_ A
18	17	sseli 2617	. . . . . . . . . . . . . . . . 17 |- ((F` x) e. D -> (F` x) e. A)
19	15, 18	syl 12	. . . . . . . . . . . . . . . 16 |- ((x e. On /\ (R We A /\ D =/= (/))) -> (F` x) e. A)
20	6, 19	syl5cbi 226	. . . . . . . . . . . . . . 15 |- ((x e. On /\ (R We A /\ D =/= (/))) -> ((F` x) = r -> r e. A))
21	20	exp32 408	. . . . . . . . . . . . . 14 |- (x e. On -> (R We A -> (D =/= (/) -> ((F` x) = r -> r e. A))))
22	21	com12 14	. . . . . . . . . . . . 13 |- (R We A -> (x e. On -> (D =/= (/) -> ((F` x) = r -> r e. A))))
23	22	a2d 16	. . . . . . . . . . . 12 |- (R We A -> ((x e. On -> D =/= (/)) -> (x e. On -> ((F` x) = r -> r e. A))))
24	23	a4sd 1331	. . . . . . . . . . 11 |- (R We A -> (A.x(x e. On -> D =/= (/)) -> (x e. On -> ((F` x) = r -> r e. A))))
25	24	imp 377	. . . . . . . . . 10 |- ((R We A /\ A.x(x e. On -> D =/= (/))) -> (x e. On -> ((F` x) = r -> r e. A)))
26	4, 5, 25	r19.23ad 2213	. . . . . . . . 9 |- ((R We A /\ A.x(x e. On -> D =/= (/))) -> (E.x e. On (F` x) = r -> r e. A))
27	8, 9	tfr1 5132	. . . . . . . . . 10 |- F Fn On
28		fvelrnb 4719	. . . . . . . . . 10 |- (F Fn On -> (r e. ran F <-> E.x e. On (F` x) = r))
29	27, 28	ax-mp 7	. . . . . . . . 9 |- (r e. ran F <-> E.x e. On (F` x) = r)
30	26, 29	syl5ib 223	. . . . . . . 8 |- ((R We A /\ A.x(x e. On -> D =/= (/))) -> (r e. ran F -> r e. A))
31	30	ssrdv 2622	. . . . . . 7 |- ((R We A /\ A.x(x e. On -> D =/= (/))) -> ran F C_ A)
32	7	ssex 3455	. . . . . . 7 |- (ran F C_ A -> ran F e. _V)
33	31, 32	syl 12	. . . . . 6 |- ((R We A /\ A.x(x e. On -> D =/= (/))) -> ran F e. _V)
34	33	ex 402	. . . . 5 |- (R We A -> (A.x(x e. On -> D =/= (/)) -> ran F e. _V))
35	7, 8, 9, 10, 11, 12, 13	ordtypelem3 5686	. . . . . . . . . . . . . 14 |- ((x e. On /\ R We A /\ D =/= (/)) -> (y e. x -> -. (F` x) = (F` y)))
36	35	3com12 1071	. . . . . . . . . . . . 13 |- ((R We A /\ x e. On /\ D =/= (/)) -> (y e. x -> -. (F` x) = (F` y)))
37	36	3exp 1066	. . . . . . . . . . . 12 |- (R We A -> (x e. On -> (D =/= (/) -> (y e. x -> -. (F` x) = (F` y)))))
38	37	a2d 16	. . . . . . . . . . 11 |- (R We A -> ((x e. On -> D =/= (/)) -> (x e. On -> (y e. x -> -. (F` x) = (F` y)))))
39	38	imp4a 391	. . . . . . . . . 10 |- (R We A -> ((x e. On -> D =/= (/)) -> ((x e. On /\ y e. x) -> -. (F` x) = (F` y))))
40	39	19.21adv 1666	. . . . . . . . 9 |- (R We A -> ((x e. On -> D =/= (/)) -> A.y((x e. On /\ y e. x) -> -. (F` x) = (F` y))))
41	40	alimdv 1668	. . . . . . . 8 |- (R We A -> (A.x(x e. On -> D =/= (/)) -> A.xA.y((x e. On /\ y e. x) -> -. (F` x) = (F` y))))
42		r2al 2136	. . . . . . . 8 |- (A.x e. On A.y e. x -. (F` x) = (F` y) <-> A.xA.y((x e. On /\ y e. x) -> -. (F` x) = (F` y)))
43	41, 42	syl6ibr 230	. . . . . . 7 |- (R We A -> (A.x(x e. On -> D =/= (/)) -> A.x e. On A.y e. x -. (F` x) = (F` y)))
44		ssid 2634	. . . . . . . . 9 |- On C_ On
45	27	tz7.48lem 5164	. . . . . . . . 9 |- ((On C_ On /\ A.x e. On A.y e. x -. (F` x) = (F` y)) -> Fun `'(F |` On))
46	44, 45	mpan 759	. . . . . . . 8 |- (A.x e. On A.y e. x -. (F` x) = (F` y) -> Fun `'(F |` On))
47	8, 9	tfrlem6 5124	. . . . . . . . . . 11 |- Rel F
48		fndm 4512	. . . . . . . . . . . . 13 |- (F Fn On -> dom F = On)
49	27, 48	ax-mp 7	. . . . . . . . . . . 12 |- dom F = On
50	49	eqimssi 2668	. . . . . . . . . . 11 |- dom F C_ On
51		relssres 4248	. . . . . . . . . . 11 |- ((Rel F /\ dom F C_ On) -> (F |` On) = F)
52	47, 50, 51	mp2an 761	. . . . . . . . . 10 |- (F |` On) = F
53	52	cnveqi 4136	. . . . . . . . 9 |- `'(F |` On) = `'F
54		funeq 4441	. . . . . . . . 9 |- (`'(F |` On) = `'F -> (Fun `'(F |` On) <-> Fun `'F))
55	53, 54	ax-mp 7	. . . . . . . 8 |- (Fun `'(F |` On) <-> Fun `'F)
56	46, 55	sylib 215	. . . . . . 7 |- (A.x e. On A.y e. x -. (F` x) = (F` y) -> Fun `'F)
57	43, 56	syl6 25	. . . . . 6 |- (R We A -> (A.x(x e. On -> D =/= (/)) -> Fun `'F))
58		onprc 3865	. . . . . . 7 |- -. On e. _V
59		funrnex 4544	. . . . . . . . 9 |- (dom `' F e. _V -> (Fun `'F -> ran `' F e. _V))
60	59	com12 14	. . . . . . . 8 |- (Fun `'F -> (dom `' F e. _V -> ran `' F e. _V))
61		df-rn 4005	. . . . . . . . 9 |- ran F = dom `' F
62	61	eleq1i 1960	. . . . . . . 8 |- (ran F e. _V <-> dom `' F e. _V)
63		dfdm4 4151	. . . . . . . . . 10 |- dom F = ran `' F
64	49, 63	eqtr3i 1910	. . . . . . . . 9 |- On = ran `' F
65	64	eleq1i 1960	. . . . . . . 8 |- (On e. _V <-> ran `' F e. _V)
66	60, 62, 65	3imtr4g 612	. . . . . . 7 |- (Fun `'F -> (ran F e. _V -> On e. _V))
67	58, 66	mtoi 122	. . . . . 6 |- (Fun `'F -> -. ran F e. _V)
68	57, 67	syl6 25	. . . . 5 |- (R We A -> (A.x(x e. On -> D =/= (/)) -> -. ran F e. _V))
69	34, 68	jcad 661	. . . 4 |- (R We A -> (A.x(x e. On -> D =/= (/)) -> (ran F e. _V /\ -. ran F e. _V)))
70		df-ne 2019	. . . . . 6 |- (D =/= (/) <-> -. D = (/))
71	70	ralbii 2127	. . . . 5 |- (A.x e. On D =/= (/) <-> A.x e. On -. D = (/))
72		df-ral 2109	. . . . 5 |- (A.x e. On D =/= (/) <-> A.x(x e. On -> D =/= (/)))
73		ralnex 2113	. . . . 5 |- (A.x e. On -. D = (/) <-> -. E.x e. On D = (/))
74	71, 72, 73	3bitr3i 198	. . . 4 |- (A.x(x e. On -> D =/= (/)) <-> -. E.x e. On D = (/))
75	69, 74	syl5ibr 224	. . 3 |- (R We A -> (-. E.x e. On D = (/) -> (ran F e. _V /\ -. ran F e. _V)))
76	1, 75	mt3i 128	. 2 |- (R We A -> E.x e. On D = (/))
77		imaeq2 4260	. . . . . . . 8 |- (x = y -> (F"x) = (F"y))
78	77	raleqdv 2269	. . . . . . 7 |- (x = y -> (A.j e. (F"x)jRw <-> A.j e. (F"y)jRw))
79	78	rabbidv 2287	. . . . . 6 |- (x = y -> {w e. A | A.j e. (F"x)jRw} = {w e. A | A.j e. (F"y)jRw})
80	79, 11, 13	3eqtr4g 1953	. . . . 5 |- (x = y -> D = H)
81	80	eqeq1d 1892	. . . 4 |- (x = y -> (D = (/) <-> H = (/)))
82	81	onminex 3888	. . 3 |- (E.x e. On D = (/) -> E.x e. On (D = (/) /\ A.y e. x -. H = (/)))
83		df-ne 2019	. . . . . 6 |- (H =/= (/) <-> -. H = (/))
84	83	ralbii 2127	. . . . 5 |- (A.y e. x H =/= (/) <-> A.y e. x -. H = (/))
85	84	anbi2i 538	. . . 4 |- ((D = (/) /\ A.y e. x H =/= (/)) <-> (D = (/) /\ A.y e. x -. H = (/)))
86	85	rexbii 2128	. . 3 |- (E.x e. On (D = (/) /\ A.y e. x H =/= (/)) <-> E.x e. On (D = (/) /\ A.y e. x -. H = (/)))
87	82, 86	sylibr 217	. 2 |- (E.x e. On D = (/) -> E.x e. On (D = (/) /\ A.y e. x H =/= (/)))
88	76, 87	syl 12	1 |- (R We A -> E.x e. On (D = (/) /\ A.y e. x H =/= (/)))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   /\ wa 240  A.wal 1296   = wceq 1298   e. wcel 1300  {cab 1871   =/= wne 2017  A.wral 2105  E.wrex 2106  {crab 2108  _Vcvv 2292   C_ wss 2593  (/)c0 2875  U.cuni 3177   class class class wbr 3338  {copab 3395   We wwe 3624  Oncon0 3657  `'ccnv 3985  dom cdm 3986  ran crn 3987   |` cres 3988  "cima 3989  Rel wrel 3991  Fun wfun 3992   Fn wfn 3993  ` cfv 3998

This theorem is referenced by:  ordtypelem7 5690  ordtypelem7OLD 15381

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-reu 2111  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-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-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-f 4010  df-f1 4011  df-fv 4014

Copyright terms: Public domain