Theorem ordtypelem4 5918

Description: Lemma for ordtype 5922. 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 972	. . 3 |- -. (ran F e. _V /\ -. ran F e. _V)
2		df-ne 2268	. . . . . 6 |- (D =/= (/) <-> -. D = (/))
3	2	ralbii 2377	. . . . 5 |- (A.x e. On D =/= (/) <-> A.x e. On -. D = (/))
4		df-ral 2359	. . . . 5 |- (A.x e. On D =/= (/) <-> A.x(x e. On -> D =/= (/)))
5		ralnex 2363	. . . . 5 |- (A.x e. On -. D = (/) <-> -. E.x e. On D = (/))
6	3, 4, 5	3bitr3i 293	. . . 4 |- (A.x(x e. On -> D =/= (/)) <-> -. E.x e. On D = (/))
7		ordtypelem.2	. . . . . . . . . . 11 |- B = {h | E.b e. On (h Fn b /\ A.c e. b (h` c) = (G` (h |` c)))}
8		ordtypelem.3	. . . . . . . . . . 11 |- F = U.B
9	7, 8	tfr1 5296	. . . . . . . . . 10 |- F Fn On
10		fvelrnb 4805	. . . . . . . . . 10 |- (F Fn On -> (r e. ran F <-> E.x e. On (F` x) = r))
11	9, 10	ax-mp 7	. . . . . . . . 9 |- (r e. ran F <-> E.x e. On (F` x) = r)
12		ax-17 1605	. . . . . . . . . . 11 |- (R We A -> A.x R We A)
13		hba1 1639	. . . . . . . . . . 11 |- (A.x(x e. On -> D =/= (/)) -> A.xA.x(x e. On -> D =/= (/)))
14	12, 13	hban 1645	. . . . . . . . . 10 |- ((R We A /\ A.x(x e. On -> D =/= (/))) -> A.x(R We A /\ A.x(x e. On -> D =/= (/))))
15		ax-17 1605	. . . . . . . . . 10 |- (r e. A -> A.x r e. A)
16		ordtypelem.1	. . . . . . . . . . . . . . . . . . 19 |- A e. _V
17		ordtypelem.4	. . . . . . . . . . . . . . . . . . 19 |- C = {w e. A | A.j e. ran h jRw}
18		ordtypelem.5	. . . . . . . . . . . . . . . . . . 19 |- D = {w e. A | A.j e. (F"x)jRw}
19		ordtypelem.6	. . . . . . . . . . . . . . . . . . 19 |- G = {<.h, c>. | c = U.{v e. C | A.u e. C -. uRv}}
20		ordtypelem.7	. . . . . . . . . . . . . . . . . . 19 |- H = {w e. A | A.j e. (F"y)jRw}
21	16, 7, 8, 17, 18, 19, 20	ordtypelem1 5915	. . . . . . . . . . . . . . . . . 18 |- ((x e. On /\ R We A /\ D =/= (/)) -> (F` x) e. D)
22	21	3expb 1318	. . . . . . . . . . . . . . . . 17 |- ((x e. On /\ (R We A /\ D =/= (/))) -> (F` x) e. D)
23		ssrab2 2917	. . . . . . . . . . . . . . . . . . 19 |- {w e. A | A.j e. (F"x)jRw} C_ A
24	18, 23	eqsstri 2874	. . . . . . . . . . . . . . . . . 18 |- D C_ A
25	24	sseli 2848	. . . . . . . . . . . . . . . . 17 |- ((F` x) e. D -> (F` x) e. A)
26	22, 25	syl 13	. . . . . . . . . . . . . . . 16 |- ((x e. On /\ (R We A /\ D =/= (/))) -> (F` x) e. A)
27		eleq1 2204	. . . . . . . . . . . . . . . 16 |- ((F` x) = r -> ((F` x) e. A <-> r e. A))
28	26, 27	syl5ibcom 254	. . . . . . . . . . . . . . 15 |- ((x e. On /\ (R We A /\ D =/= (/))) -> ((F` x) = r -> r e. A))
29	28	exp32 578	. . . . . . . . . . . . . 14 |- (x e. On -> (R We A -> (D =/= (/) -> ((F` x) = r -> r e. A))))
30	29	com12 26	. . . . . . . . . . . . 13 |- (R We A -> (x e. On -> (D =/= (/) -> ((F` x) = r -> r e. A))))
31	30	a2d 19	. . . . . . . . . . . 12 |- (R We A -> ((x e. On -> D =/= (/)) -> (x e. On -> ((F` x) = r -> r e. A))))
32	31	a4sd 1620	. . . . . . . . . . 11 |- (R We A -> (A.x(x e. On -> D =/= (/)) -> (x e. On -> ((F` x) = r -> r e. A))))
33	32	imp 393	. . . . . . . . . 10 |- ((R We A /\ A.x(x e. On -> D =/= (/))) -> (x e. On -> ((F` x) = r -> r e. A)))
34	14, 15, 33	r19.23ad 2462	. . . . . . . . 9 |- ((R We A /\ A.x(x e. On -> D =/= (/))) -> (E.x e. On (F` x) = r -> r e. A))
35	11, 34	syl5bi 249	. . . . . . . 8 |- ((R We A /\ A.x(x e. On -> D =/= (/))) -> (r e. ran F -> r e. A))
36	35	ssrdv 2853	. . . . . . 7 |- ((R We A /\ A.x(x e. On -> D =/= (/))) -> ran F C_ A)
37	16	ssex 3622	. . . . . . 7 |- (ran F C_ A -> ran F e. _V)
38	36, 37	syl 13	. . . . . 6 |- ((R We A /\ A.x(x e. On -> D =/= (/))) -> ran F e. _V)
39	38	ex 398	. . . . 5 |- (R We A -> (A.x(x e. On -> D =/= (/)) -> ran F e. _V))
40	16, 7, 8, 17, 18, 19, 20	ordtypelem3 5917	. . . . . . . . . . . . . 14 |- ((x e. On /\ R We A /\ D =/= (/)) -> (y e. x -> -. (F` x) = (F` y)))
41	40	3com12 1321	. . . . . . . . . . . . 13 |- ((R We A /\ x e. On /\ D =/= (/)) -> (y e. x -> -. (F` x) = (F` y)))
42	41	3exp 1316	. . . . . . . . . . . 12 |- (R We A -> (x e. On -> (D =/= (/) -> (y e. x -> -. (F` x) = (F` y)))))
43	42	a2d 19	. . . . . . . . . . 11 |- (R We A -> ((x e. On -> D =/= (/)) -> (x e. On -> (y e. x -> -. (F` x) = (F` y)))))
44	43	imp4a 565	. . . . . . . . . 10 |- (R We A -> ((x e. On -> D =/= (/)) -> ((x e. On /\ y e. x) -> -. (F` x) = (F` y))))
45	44	19.21adv 1935	. . . . . . . . 9 |- (R We A -> ((x e. On -> D =/= (/)) -> A.y((x e. On /\ y e. x) -> -. (F` x) = (F` y))))
46	45	alimdv 1937	. . . . . . . 8 |- (R We A -> (A.x(x e. On -> D =/= (/)) -> A.xA.y((x e. On /\ y e. x) -> -. (F` x) = (F` y))))
47		r2al 2386	. . . . . . . 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)))
48	46, 47	syl6ibr 262	. . . . . . 7 |- (R We A -> (A.x(x e. On -> D =/= (/)) -> A.x e. On A.y e. x -. (F` x) = (F` y)))
49		ssid 2863	. . . . . . . . 9 |- On C_ On
50	9	tz7.48lem 5328	. . . . . . . . 9 |- ((On C_ On /\ A.x e. On A.y e. x -. (F` x) = (F` y)) -> Fun `'(F |` On))
51	49, 50	mpan 677	. . . . . . . 8 |- (A.x e. On A.y e. x -. (F` x) = (F` y) -> Fun `'(F |` On))
52	7, 8	tfrlem6 5288	. . . . . . . . . . 11 |- Rel F
53		fndm 4612	. . . . . . . . . . . . 13 |- (F Fn On -> dom F = On)
54	9, 53	ax-mp 7	. . . . . . . . . . . 12 |- dom F = On
55	54	eqimssi 2896	. . . . . . . . . . 11 |- dom F C_ On
56		relssres 4370	. . . . . . . . . . 11 |- ((Rel F /\ dom F C_ On) -> (F |` On) = F)
57	52, 55, 56	mp2an 681	. . . . . . . . . 10 |- (F |` On) = F
58	57	cnveqi 4264	. . . . . . . . 9 |- `'(F |` On) = `'F
59		funeq 4544	. . . . . . . . 9 |- (`'(F |` On) = `'F -> (Fun `'(F |` On) <-> Fun `'F))
60	58, 59	ax-mp 7	. . . . . . . 8 |- (Fun `'(F |` On) <-> Fun `'F)
61	51, 60	sylib 242	. . . . . . 7 |- (A.x e. On A.y e. x -. (F` x) = (F` y) -> Fun `'F)
62	48, 61	syl6 42	. . . . . 6 |- (R We A -> (A.x(x e. On -> D =/= (/)) -> Fun `'F))
63		onprc 4010	. . . . . . 7 |- -. On e. _V
64		funrnex 4640	. . . . . . . . 9 |- (dom `' F e. _V -> (Fun `'F -> ran `' F e. _V))
65	64	com12 26	. . . . . . . 8 |- (Fun `'F -> (dom `' F e. _V -> ran `' F e. _V))
66		df-rn 4138	. . . . . . . . 9 |- ran F = dom `' F
67	66	eleq1i 2207	. . . . . . . 8 |- (ran F e. _V <-> dom `' F e. _V)
68		dfdm4 4277	. . . . . . . . . 10 |- dom F = ran `' F
69	54, 68	eqtr3i 2163	. . . . . . . . 9 |- On = ran `' F
70	69	eleq1i 2207	. . . . . . . 8 |- (On e. _V <-> ran `' F e. _V)
71	65, 67, 70	3imtr4g 332	. . . . . . 7 |- (Fun `'F -> (ran F e. _V -> On e. _V))
72	63, 71	mtoi 153	. . . . . 6 |- (Fun `'F -> -. ran F e. _V)
73	62, 72	syl6 42	. . . . 5 |- (R We A -> (A.x(x e. On -> D =/= (/)) -> -. ran F e. _V))
74	39, 73	jcad 496	. . . 4 |- (R We A -> (A.x(x e. On -> D =/= (/)) -> (ran F e. _V /\ -. ran F e. _V)))
75	6, 74	syl5bir 251	. . 3 |- (R We A -> (-. E.x e. On D = (/) -> (ran F e. _V /\ -. ran F e. _V)))
76	1, 75	mt3i 161	. 2 |- (R We A -> E.x e. On D = (/))
77		imaeq2 4380	. . . . . . . 8 |- (x = y -> (F"x) = (F"y))
78	77	raleqdv 2515	. . . . . . 7 |- (x = y -> (A.j e. (F"x)jRw <-> A.j e. (F"y)jRw))
79	78	rabbidv 2533	. . . . . 6 |- (x = y -> {w e. A | A.j e. (F"x)jRw} = {w e. A | A.j e. (F"y)jRw})
80	79, 18, 20	3eqtr4g 2201	. . . . 5 |- (x = y -> D = H)
81	80	eqeq1d 2149	. . . 4 |- (x = y -> (D = (/) <-> H = (/)))
82	81	onminex 4031	. . 3 |- (E.x e. On D = (/) -> E.x e. On (D = (/) /\ A.y e. x -. H = (/)))
83		df-ne 2268	. . . . . 6 |- (H =/= (/) <-> -. H = (/))
84	83	ralbii 2377	. . . . 5 |- (A.y e. x H =/= (/) <-> A.y e. x -. H = (/))
85	84	anbi2i 708	. . . 4 |- ((D = (/) /\ A.y e. x H =/= (/)) <-> (D = (/) /\ A.y e. x -. H = (/)))
86	85	rexbii 2378	. . 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 243	. 2 |- (E.x e. On D = (/) -> E.x e. On (D = (/) /\ A.y e. x H =/= (/)))
88	76, 87	syl 13	1 |- (R We A -> E.x e. On (D = (/) /\ A.y e. x H =/= (/)))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 219   /\ wa 337  A.wal 1584   = wceq 1586   e. wcel 1588  {cab 2128   =/= wne 2266  A.wral 2355  E.wrex 2356  {crab 2358  _Vcvv 2538   C_ wss 2827  (/)c0 3082  U.cuni 3366   class class class wbr 3507  {copab 3565   We wwe 3781  Oncon0 3811  `'ccnv 4118  dom cdm 4119  ran crn 4120   |` cres 4121  "cima 4122  Rel wrel 4124  Fun wfun 4125   Fn wfn 4126  ` cfv 4131

This theorem is referenced by:  ordtypelem7 5921  ordtypelem7OLD 16205

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1592  ax-gen 1593  ax-8 1594  ax-9 1595  ax-10 1596  ax-11 1597  ax-12 1598  ax-13 1599  ax-14 1600  ax-17 1605  ax-4 1608  ax-5o 1610  ax-6o 1613  ax-9o 1763  ax-10o 1781  ax-16 1854  ax-11o 1864  ax-ext 2123  ax-rep 3596  ax-sep 3606  ax-nul 3613  ax-pow 3649  ax-pr 3687  ax-un 3929

This theorem depends on definitions:  df-bi 220  df-or 338  df-an 339  df-3or 1103  df-3an 1104  df-ex 1616  df-sb 1816  df-eu 2041  df-mo 2042  df-clab 2129  df-cleq 2134  df-clel 2137  df-ne 2268  df-ral 2359  df-rex 2360  df-reu 2361  df-rab 2362  df-v 2540  df-sbc 2700  df-csb 2774  df-dif 2830  df-un 2832  df-in 2834  df-ss 2836  df-pss 2838  df-nul 3083  df-pw 3229  df-sn 3242  df-pr 3243  df-tp 3245  df-op 3246  df-uni 3367  df-int 3401  df-iun 3438  df-br 3508  df-opab 3566  df-tr 3580  df-eprel 3744  df-id 3747  df-po 3752  df-so 3764  df-fr 3782  df-we 3798  df-ord 3814  df-on 3815  df-suc 3817  df-xp 4133  df-rel 4134  df-cnv 4135  df-co 4136  df-dm 4137  df-rn 4138  df-res 4139  df-ima 4140  df-fun 4141  df-fn 4142  df-f 4143  df-f1 4144  df-fv 4147

Copyright terms: Public domain