Theorem ordtypelem5 5688

Description: Lemma for ordtype 5691. Establish injectivity of F when restricted to the ordinal number of ordtypelem4 5687.

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
ordtypelem5	|- (((R We A /\ x e. On) /\ (D = (/) /\ A.y e. x H =/= (/))) -> Fun `'(F |` x))

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 ordtypelem5

Step	Hyp	Ref	Expression
1		onss 3869	. . 3 |- (x e. On -> x C_ On)
2	1	ad2antlr 441	. 2 |- (((R We A /\ x e. On) /\ (D = (/) /\ A.y e. x H =/= (/))) -> x C_ On)
3		visset 2295	. . . . . . . . . 10 |- z e. _V
4		ax-17 1317	. . . . . . . . . 10 |- (m e. z -> A.y m e. z)
5	3, 4	hbcsb1 2568	. . . . . . . . 9 |- (m e. [_z / y]_H -> A.y m e. [_z / y]_H)
6		ax-17 1317	. . . . . . . . 9 |- (m e. (/) -> A.y m e. (/))
7	5, 6	hbne 2103	. . . . . . . 8 |- ([_z / y]_H =/= (/) -> A.y[_z / y]_H =/= (/))
8		csbeq1a 2546	. . . . . . . . 9 |- (y = z -> H = [_z / y]_H)
9	8	neeq1d 2028	. . . . . . . 8 |- (y = z -> (H =/= (/) <-> [_z / y]_H =/= (/)))
10	7, 9	rcla4 2373	. . . . . . 7 |- (z e. x -> (A.y e. x H =/= (/) -> [_z / y]_H =/= (/)))
11		ordtypelem.1	. . . . . . . . . . . . . . . 16 |- A e. _V
12		ordtypelem.2	. . . . . . . . . . . . . . . 16 |- B = {h | E.b e. On (h Fn b /\ A.c e. b (h` c) = (G` (h |` c)))}
13		ordtypelem.3	. . . . . . . . . . . . . . . 16 |- F = U.B
14		ordtypelem.4	. . . . . . . . . . . . . . . 16 |- C = {w e. A | A.j e. ran h jRw}
15		ordtypelem.5	. . . . . . . . . . . . . . . 16 |- D = {w e. A | A.j e. (F"x)jRw}
16		ordtypelem.6	. . . . . . . . . . . . . . . 16 |- G = {<.h, c>. | c = U.{v e. C | A.u e. C -. uRv}}
17		ordtypelem.7	. . . . . . . . . . . . . . . 16 |- H = {w e. A | A.j e. (F"y)jRw}
18	11, 12, 13, 14, 15, 16, 17	ordtypelem3 5686	. . . . . . . . . . . . . . 15 |- ((x e. On /\ R We A /\ D =/= (/)) -> (y e. x -> -. (F` x) = (F` y)))
19	18	gen2 1329	. . . . . . . . . . . . . 14 |- A.xA.y((x e. On /\ R We A /\ D =/= (/)) -> (y e. x -> -. (F` x) = (F` y)))
20		ax-17 1317	. . . . . . . . . . . . . . . . 17 |- (m e. z -> A.x m e. z)
21		ax-17 1317	. . . . . . . . . . . . . . . . . . . 20 |- (z e. On -> A.x z e. On)
22		ax-17 1317	. . . . . . . . . . . . . . . . . . . 20 |- (R We A -> A.x R We A)
23	3, 20	hbcsb1 2568	. . . . . . . . . . . . . . . . . . . . 21 |- (m e. [_z / x]_D -> A.x m e. [_z / x]_D)
24		ax-17 1317	. . . . . . . . . . . . . . . . . . . . 21 |- (m e. (/) -> A.x m e. (/))
25	23, 24	hbne 2103	. . . . . . . . . . . . . . . . . . . 20 |- ([_z / x]_D =/= (/) -> A.x[_z / x]_D =/= (/))
26	21, 22, 25	hb3an 1359	. . . . . . . . . . . . . . . . . . 19 |- ((z e. On /\ R We A /\ [_z / x]_D =/= (/)) -> A.x(z e. On /\ R We A /\ [_z / x]_D =/= (/)))
27		ax-17 1317	. . . . . . . . . . . . . . . . . . 19 |- ((y e. z -> -. (F` z) = (F` y)) -> A.x(y e. z -> -. (F` z) = (F` y)))
28	26, 27	hbim 1354	. . . . . . . . . . . . . . . . . 18 |- (((z e. On /\ R We A /\ [_z / x]_D =/= (/)) -> (y e. z -> -. (F` z) = (F` y))) -> A.x((z e. On /\ R We A /\ [_z / x]_D =/= (/)) -> (y e. z -> -. (F` z) = (F` y))))
29	28	hbal 1352	. . . . . . . . . . . . . . . . 17 |- (A.y((z e. On /\ R We A /\ [_z / x]_D =/= (/)) -> (y e. z -> -. (F` z) = (F` y))) -> A.xA.y((z e. On /\ R We A /\ [_z / x]_D =/= (/)) -> (y e. z -> -. (F` z) = (F` y))))
30		eleq1 1957	. . . . . . . . . . . . . . . . . . . 20 |- (x = z -> (x e. On <-> z e. On))
31		csbeq1a 2546	. . . . . . . . . . . . . . . . . . . . 21 |- (x = z -> D = [_z / x]_D)
32	31	neeq1d 2028	. . . . . . . . . . . . . . . . . . . 20 |- (x = z -> (D =/= (/) <-> [_z / x]_D =/= (/)))
33	30, 32	3anbi13d 1170	. . . . . . . . . . . . . . . . . . 19 |- (x = z -> ((x e. On /\ R We A /\ D =/= (/)) <-> (z e. On /\ R We A /\ [_z / x]_D =/= (/))))
34		eleq2 1958	. . . . . . . . . . . . . . . . . . . 20 |- (x = z -> (y e. x <-> y e. z))
35		fveq2 4681	. . . . . . . . . . . . . . . . . . . . . 22 |- (x = z -> (F` x) = (F` z))
36	35	eqeq1d 1892	. . . . . . . . . . . . . . . . . . . . 21 |- (x = z -> ((F` x) = (F` y) <-> (F` z) = (F` y)))
37	36	notbid 673	. . . . . . . . . . . . . . . . . . . 20 |- (x = z -> (-. (F` x) = (F` y) <-> -. (F` z) = (F` y)))
38	34, 37	imbi12d 688	. . . . . . . . . . . . . . . . . . 19 |- (x = z -> ((y e. x -> -. (F` x) = (F` y)) <-> (y e. z -> -. (F` z) = (F` y))))
39	33, 38	imbi12d 688	. . . . . . . . . . . . . . . . . 18 |- (x = z -> (((x e. On /\ R We A /\ D =/= (/)) -> (y e. x -> -. (F` x) = (F` y))) <-> ((z e. On /\ R We A /\ [_z / x]_D =/= (/)) -> (y e. z -> -. (F` z) = (F` y)))))
40	39	albidv 1656	. . . . . . . . . . . . . . . . 17 |- (x = z -> (A.y((x e. On /\ R We A /\ D =/= (/)) -> (y e. x -> -. (F` x) = (F` y))) <-> A.y((z e. On /\ R We A /\ [_z / x]_D =/= (/)) -> (y e. z -> -. (F` z) = (F` y)))))
41	20, 29, 40	cla4gf 2361	. . . . . . . . . . . . . . . 16 |- (z e. _V -> (A.xA.y((x e. On /\ R We A /\ D =/= (/)) -> (y e. x -> -. (F` x) = (F` y))) -> A.y((z e. On /\ R We A /\ [_z / x]_D =/= (/)) -> (y e. z -> -. (F` z) = (F` y)))))
42	3, 41	ax-mp 7	. . . . . . . . . . . . . . 15 |- (A.xA.y((x e. On /\ R We A /\ D =/= (/)) -> (y e. x -> -. (F` x) = (F` y))) -> A.y((z e. On /\ R We A /\ [_z / x]_D =/= (/)) -> (y e. z -> -. (F` z) = (F` y))))
43		eleq1 1957	. . . . . . . . . . . . . . . . . 18 |- (y = r -> (y e. z <-> r e. z))
44		fveq2 4681	. . . . . . . . . . . . . . . . . . . 20 |- (y = r -> (F` y) = (F` r))
45	44	eqeq2d 1895	. . . . . . . . . . . . . . . . . . 19 |- (y = r -> ((F` z) = (F` y) <-> (F` z) = (F` r)))
46	45	notbid 673	. . . . . . . . . . . . . . . . . 18 |- (y = r -> (-. (F` z) = (F` y) <-> -. (F` z) = (F` r)))
47	43, 46	imbi12d 688	. . . . . . . . . . . . . . . . 17 |- (y = r -> ((y e. z -> -. (F` z) = (F` y)) <-> (r e. z -> -. (F` z) = (F` r))))
48	47	imbi2d 674	. . . . . . . . . . . . . . . 16 |- (y = r -> (((z e. On /\ R We A /\ [_z / x]_D =/= (/)) -> (y e. z -> -. (F` z) = (F` y))) <-> ((z e. On /\ R We A /\ [_z / x]_D =/= (/)) -> (r e. z -> -. (F` z) = (F` r)))))
49	48	a4v 1649	. . . . . . . . . . . . . . 15 |- (A.y((z e. On /\ R We A /\ [_z / x]_D =/= (/)) -> (y e. z -> -. (F` z) = (F` y))) -> ((z e. On /\ R We A /\ [_z / x]_D =/= (/)) -> (r e. z -> -. (F` z) = (F` r))))
50	42, 49	syl 12	. . . . . . . . . . . . . 14 |- (A.xA.y((x e. On /\ R We A /\ D =/= (/)) -> (y e. x -> -. (F` x) = (F` y))) -> ((z e. On /\ R We A /\ [_z / x]_D =/= (/)) -> (r e. z -> -. (F` z) = (F` r))))
51	19, 50	ax-mp 7	. . . . . . . . . . . . 13 |- ((z e. On /\ R We A /\ [_z / x]_D =/= (/)) -> (r e. z -> -. (F` z) = (F` r)))
52	51	3expia 1069	. . . . . . . . . . . 12 |- ((z e. On /\ R We A) -> ([_z / x]_D =/= (/) -> (r e. z -> -. (F` z) = (F` r))))
53	52	ancoms 484	. . . . . . . . . . 11 |- ((R We A /\ z e. On) -> ([_z / x]_D =/= (/) -> (r e. z -> -. (F` z) = (F` r))))
54		onelon 3683	. . . . . . . . . . 11 |- ((x e. On /\ z e. x) -> z e. On)
55	53, 54	sylan2 500	. . . . . . . . . 10 |- ((R We A /\ (x e. On /\ z e. x)) -> ([_z / x]_D =/= (/) -> (r e. z -> -. (F` z) = (F` r))))
56	55	expr 418	. . . . . . . . 9 |- ((R We A /\ x e. On) -> (z e. x -> ([_z / x]_D =/= (/) -> (r e. z -> -. (F` z) = (F` r)))))
57	56	com3l 38	. . . . . . . 8 |- (z e. x -> ([_z / x]_D =/= (/) -> ((R We A /\ x e. On) -> (r e. z -> -. (F` z) = (F` r)))))
58		imaeq2 4260	. . . . . . . . . . . . . 14 |- (y = x -> (F"y) = (F"x))
59	58	raleqdv 2269	. . . . . . . . . . . . 13 |- (y = x -> (A.j e. (F"y)jRw <-> A.j e. (F"x)jRw))
60	59	rabbidv 2287	. . . . . . . . . . . 12 |- (y = x -> {w e. A | A.j e. (F"y)jRw} = {w e. A | A.j e. (F"x)jRw})
61	60, 17, 15	3eqtr4g 1953	. . . . . . . . . . 11 |- (y = x -> H = D)
62	61	cbvcsbv 2543	. . . . . . . . . 10 |- (z e. _V -> [_z / y]_H = [_z / x]_D)
63	3, 62	ax-mp 7	. . . . . . . . 9 |- [_z / y]_H = [_z / x]_D
64	63	neeq1i 2026	. . . . . . . 8 |- ([_z / y]_H =/= (/) <-> [_z / x]_D =/= (/))
65	57, 64	syl5ib 223	. . . . . . 7 |- (z e. x -> ([_z / y]_H =/= (/) -> ((R We A /\ x e. On) -> (r e. z -> -. (F` z) = (F` r)))))
66	10, 65	syld 30	. . . . . 6 |- (z e. x -> (A.y e. x H =/= (/) -> ((R We A /\ x e. On) -> (r e. z -> -. (F` z) = (F` r)))))
67	66	com13 37	. . . . 5 |- ((R We A /\ x e. On) -> (A.y e. x H =/= (/) -> (z e. x -> (r e. z -> -. (F` z) = (F` r)))))
68	67	imp4b 392	. . . 4 |- (((R We A /\ x e. On) /\ A.y e. x H =/= (/)) -> ((z e. x /\ r e. z) -> -. (F` z) = (F` r)))
69	68	adantrl 430	. . 3 |- (((R We A /\ x e. On) /\ (D = (/) /\ A.y e. x H =/= (/))) -> ((z e. x /\ r e. z) -> -. (F` z) = (F` r)))
70	69	r19.21aivv 2183	. 2 |- (((R We A /\ x e. On) /\ (D = (/) /\ A.y e. x H =/= (/))) -> A.z e. x A.r e. z -. (F` z) = (F` r))
71	12, 13	tfr1 5132	. . 3 |- F Fn On
72	71	tz7.48lem 5164	. 2 |- ((x C_ On /\ A.z e. x A.r e. z -. (F` z) = (F` r)) -> Fun `'(F |` x))
73	2, 70, 72	syl11anc 524	1 |- (((R We A /\ x e. On) /\ (D = (/) /\ A.y e. x H =/= (/))) -> Fun `'(F |` x))

Syntax hints:  -. wn 2   -> wi 3   /\ wa 240   /\ w3a 858  A.wal 1296   = wceq 1298   e. wcel 1300  {cab 1871   =/= wne 2017  A.wral 2105  E.wrex 2106  {crab 2108  _Vcvv 2292  [_csb 2540   C_ wss 2593  (/)c0 2875  U.cuni 3177   class class class wbr 3338  {copab 3395   We wwe 3624  Oncon0 3657  `'ccnv 3985  ran crn 3987   |` cres 3988  "cima 3989  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-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