Theorem ordtypelem7 5690

Description: Lemma for ordtype 5691. F maps some ordinal isomorphically onto 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
ordtypelem7	|- (R We A -> E.x e. On (F |` x) Isom _E , R (x, A))

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 ordtypelem7

Step	Hyp	Ref	Expression
1		ordtypelem.1	. . 3 |- A e. _V
2		ordtypelem.2	. . 3 |- B = {h | E.b e. On (h Fn b /\ A.c e. b (h` c) = (G` (h |` c)))}
3		ordtypelem.3	. . 3 |- F = U.B
4		ordtypelem.4	. . 3 |- C = {w e. A | A.j e. ran h jRw}
5		ordtypelem.5	. . 3 |- D = {w e. A | A.j e. (F"x)jRw}
6		ordtypelem.6	. . 3 |- G = {<.h, c>. | c = U.{v e. C | A.u e. C -. uRv}}
7		ordtypelem.7	. . 3 |- H = {w e. A | A.j e. (F"y)jRw}
8	1, 2, 3, 4, 5, 6, 7	ordtypelem4 5687	. 2 |- (R We A -> E.x e. On (D = (/) /\ A.y e. x H =/= (/)))
9		df-iso 4015	. . . . 5 |- ((F |` x) Isom _E , R (x, A) <-> ((F |` x):x-1-1-onto->A /\ A.y e. x A.z e. x (y _E z <-> ((F |` x)` y)R((F |` x)` z))))
10		onss 3869	. . . . . . . . 9 |- (x e. On -> x C_ On)
11	2, 3	tfr1 5132	. . . . . . . . . 10 |- F Fn On
12		fnssres 4526	. . . . . . . . . 10 |- ((F Fn On /\ x C_ On) -> (F |` x) Fn x)
13	11, 12	mpan 759	. . . . . . . . 9 |- (x C_ On -> (F |` x) Fn x)
14	10, 13	syl 12	. . . . . . . 8 |- (x e. On -> (F |` x) Fn x)
15	14	ad2antlr 441	. . . . . . 7 |- (((R We A /\ x e. On) /\ (D = (/) /\ A.y e. x H =/= (/))) -> (F |` x) Fn x)
16	1, 2, 3, 4, 5, 6, 7	ordtypelem5 5688	. . . . . . 7 |- (((R We A /\ x e. On) /\ (D = (/) /\ A.y e. x H =/= (/))) -> Fun `'(F |` x))
17		ax-17 1317	. . . . . . . . . . . . . . 15 |- ((R We A /\ x e. On) -> A.y(R We A /\ x e. On))
18		hbra1 2147	. . . . . . . . . . . . . . 15 |- (A.y e. x H =/= (/) -> A.yA.y e. x H =/= (/))
19	17, 18	hban 1356	. . . . . . . . . . . . . 14 |- (((R We A /\ x e. On) /\ A.y e. x H =/= (/)) -> A.y((R We A /\ x e. On) /\ A.y e. x H =/= (/)))
20		ax-17 1317	. . . . . . . . . . . . . 14 |- (s e. A -> A.y s e. A)
21		eleq1 1957	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((F` y) = s -> ((F` y) e. A <-> s e. A))
22	1, 2, 3, 4, 7, 6, 5	ordtypelem1 5684	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((y e. On /\ R We A /\ H =/= (/)) -> (F` y) e. H)
23	22	3expb 1068	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((y e. On /\ (R We A /\ H =/= (/))) -> (F` y) e. H)
24		ssrab2 2692	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- {w e. A | A.j e. (F"y)jRw} C_ A
25	7, 24	eqsstri 2647	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- H C_ A
26	25	sseli 2617	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((F` y) e. H -> (F` y) e. A)
27	23, 26	syl 12	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((y e. On /\ (R We A /\ H =/= (/))) -> (F` y) e. A)
28	21, 27	syl5bi 225	. . . . . . . . . . . . . . . . . . . . . 22 |- ((F` y) = s -> ((y e. On /\ (R We A /\ H =/= (/))) -> s e. A))
29		onelon 3683	. . . . . . . . . . . . . . . . . . . . . 22 |- ((x e. On /\ y e. x) -> y e. On)
30	28, 29	sylani 513	. . . . . . . . . . . . . . . . . . . . 21 |- ((F` y) = s -> (((x e. On /\ y e. x) /\ (R We A /\ H =/= (/))) -> s e. A))
31	30	com12 14	. . . . . . . . . . . . . . . . . . . 20 |- (((x e. On /\ y e. x) /\ (R We A /\ H =/= (/))) -> ((F` y) = s -> s e. A))
32	31	exp43 415	. . . . . . . . . . . . . . . . . . 19 |- (x e. On -> (y e. x -> (R We A -> (H =/= (/) -> ((F` y) = s -> s e. A)))))
33	32	com3r 39	. . . . . . . . . . . . . . . . . 18 |- (R We A -> (x e. On -> (y e. x -> (H =/= (/) -> ((F` y) = s -> s e. A)))))
34	33	imp 377	. . . . . . . . . . . . . . . . 17 |- ((R We A /\ x e. On) -> (y e. x -> (H =/= (/) -> ((F` y) = s -> s e. A))))
35	34	a2d 16	. . . . . . . . . . . . . . . 16 |- ((R We A /\ x e. On) -> ((y e. x -> H =/= (/)) -> (y e. x -> ((F` y) = s -> s e. A))))
36		ra4 2155	. . . . . . . . . . . . . . . 16 |- (A.y e. x H =/= (/) -> (y e. x -> H =/= (/)))
37	35, 36	syl5 20	. . . . . . . . . . . . . . 15 |- ((R We A /\ x e. On) -> (A.y e. x H =/= (/) -> (y e. x -> ((F` y) = s -> s e. A))))
38	37	imp 377	. . . . . . . . . . . . . 14 |- (((R We A /\ x e. On) /\ A.y e. x H =/= (/)) -> (y e. x -> ((F` y) = s -> s e. A)))
39	19, 20, 38	r19.23ad 2213	. . . . . . . . . . . . 13 |- (((R We A /\ x e. On) /\ A.y e. x H =/= (/)) -> (E.y e. x (F` y) = s -> s e. A))
40	2, 3	tfrlem7 5125	. . . . . . . . . . . . . 14 |- Fun F
41		fvelima 4723	. . . . . . . . . . . . . 14 |- ((Fun F /\ s e. (F"x)) -> E.y e. x (F` y) = s)
42	40, 41	mpan 759	. . . . . . . . . . . . 13 |- (s e. (F"x) -> E.y e. x (F` y) = s)
43	39, 42	syl5 20	. . . . . . . . . . . 12 |- (((R We A /\ x e. On) /\ A.y e. x H =/= (/)) -> (s e. (F"x) -> s e. A))
44	43	ssrdv 2622	. . . . . . . . . . 11 |- (((R We A /\ x e. On) /\ A.y e. x H =/= (/)) -> (F"x) C_ A)
45	44	adantrl 430	. . . . . . . . . 10 |- (((R We A /\ x e. On) /\ (D = (/) /\ A.y e. x H =/= (/))) -> (F"x) C_ A)
46		simpll 448	. . . . . . . . . . . . . . . . . . . . . 22 |- (((R We A /\ x e. On) /\ (((F"x) C_ A /\ A.y e. x H =/= (/)) /\ E.z(z e. A /\ -. z e. (F"x)))) -> R We A)
47		ssrab2 2692	. . . . . . . . . . . . . . . . . . . . . . 23 |- {w e. A | A.j e. (F"x)jRw} C_ A
48	47	a1i 8	. . . . . . . . . . . . . . . . . . . . . 22 |- (((R We A /\ x e. On) /\ (((F"x) C_ A /\ A.y e. x H =/= (/)) /\ E.z(z e. A /\ -. z e. (F"x)))) -> {w e. A | A.j e. (F"x)jRw} C_ A)
49		simpl 346	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((z e. A /\ -. z e. (F"x)) -> z e. A)
50	49	a1i 8	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((R We A /\ x e. On) /\ ((F"x) C_ A /\ A.y e. x H =/= (/))) -> ((z e. A /\ -. z e. (F"x)) -> z e. A))
51	1, 2, 3, 4, 5, 6, 7	ordtypelem6 5689	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ((((R We A /\ x e. On) /\ ((F"x) C_ A /\ A.y e. x H =/= (/))) /\ ((z e. A /\ -. z e. (F"x)) /\ m e. (F"x))) -> (A.n(nRm -> (n e. (F"x) -> nRz)) -> mRz))
52		breq1 3341	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- (j = n -> (jRz <-> nRz))
53	52	notbid 673	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- (j = n -> (-. jRz <-> -. nRz))
54	53	elrab 2414	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- (n e. {j e. (F"x) | -. jRz} <-> (n e. (F"x) /\ -. nRz))
55	54	notbii 204	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (-. n e. {j e. (F"x) | -. jRz} <-> -. (n e. (F"x) /\ -. nRz))
56		iman 256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ((n e. (F"x) -> nRz) <-> -. (n e. (F"x) /\ -. nRz))
57	55, 56	bitr4i 193	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (-. n e. {j e. (F"x) | -. jRz} <-> (n e. (F"x) -> nRz))
58	57	imbi2i 202	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ((nRm -> -. n e. {j e. (F"x) | -. jRz}) <-> (nRm -> (n e. (F"x) -> nRz)))
59	58	albii 1346	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (A.n(nRm -> -. n e. {j e. (F"x) | -. jRz}) <-> A.n(nRm -> (n e. (F"x) -> nRz)))
60	51, 59	syl5ib 223	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((((R We A /\ x e. On) /\ ((F"x) C_ A /\ A.y e. x H =/= (/))) /\ ((z e. A /\ -. z e. (F"x)) /\ m e. (F"x))) -> (A.n(nRm -> -. n e. {j e. (F"x) | -. jRz}) -> mRz))
61	60	con3d 111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((((R We A /\ x e. On) /\ ((F"x) C_ A /\ A.y e. x H =/= (/))) /\ ((z e. A /\ -. z e. (F"x)) /\ m e. (F"x))) -> (-. mRz -> -. A.n(nRm -> -. n e. {j e. (F"x) | -. jRz})))
62	61	expr 418	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((((R We A /\ x e. On) /\ ((F"x) C_ A /\ A.y e. x H =/= (/))) /\ (z e. A /\ -. z e. (F"x))) -> (m e. (F"x) -> (-. mRz -> -. A.n(nRm -> -. n e. {j e. (F"x) | -. jRz}))))
63	62	imp3a 388	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((((R We A /\ x e. On) /\ ((F"x) C_ A /\ A.y e. x H =/= (/))) /\ (z e. A /\ -. z e. (F"x))) -> ((m e. (F"x) /\ -. mRz) -> -. A.n(nRm -> -. n e. {j e. (F"x) | -. jRz})))
64		breq1 3341	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (j = m -> (jRz <-> mRz))
65	64	notbid 673	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (j = m -> (-. jRz <-> -. mRz))
66	65	elrab 2414	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (m e. {j e. (F"x) | -. jRz} <-> (m e. (F"x) /\ -. mRz))
67	63, 66	syl5ib 223	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((((R We A /\ x e. On) /\ ((F"x) C_ A /\ A.y e. x H =/= (/))) /\ (z e. A /\ -. z e. (F"x))) -> (m e. {j e. (F"x) | -. jRz} -> -. A.n(nRm -> -. n e. {j e. (F"x) | -. jRz})))
68	67	r19.21aiv 2175	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((((R We A /\ x e. On) /\ ((F"x) C_ A /\ A.y e. x H =/= (/))) /\ (z e. A /\ -. z e. (F"x))) -> A.m e. {j e. (F"x) | -. jRz} -. A.n(nRm -> -. n e. {j e. (F"x) | -. jRz}))
69		con2b 182	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((nRm -> -. n e. {j e. (F"x) | -. jRz}) <-> (n e. {j e. (F"x) | -. jRz} -> -. nRm))
70	69	albii 1346	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (A.n(nRm -> -. n e. {j e. (F"x) | -. jRz}) <-> A.n(n e. {j e. (F"x) | -. jRz} -> -. nRm))
71		df-ral 2109	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (A.n e. {j e. (F"x) | -. jRz} -. nRm <-> A.n(n e. {j e. (F"x) | -. jRz} -> -. nRm))
72	70, 71	bitr4i 193	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (A.n(nRm -> -. n e. {j e. (F"x) | -. jRz}) <-> A.n e. {j e. (F"x) | -. jRz} -. nRm)
73	72	notbii 204	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (-. A.n(nRm -> -. n e. {j e. (F"x) | -. jRz}) <-> -. A.n e. {j e. (F"x) | -. jRz} -. nRm)
74	73	ralbii 2127	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (A.m e. {j e. (F"x) | -. jRz} -. A.n(nRm -> -. n e. {j e. (F"x) | -. jRz}) <-> A.m e. {j e. (F"x) | -. jRz} -. A.n e. {j e. (F"x) | -. jRz} -. nRm)
75		ralnex 2113	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (A.m e. {j e. (F"x) | -. jRz} -. A.n e. {j e. (F"x) | -. jRz} -. nRm <-> -. E.m e. {j e. (F"x) | -. jRz}A.n e. {j e. (F"x) | -. jRz} -. nRm)
76	74, 75	bitri 190	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (A.m e. {j e. (F"x) | -. jRz} -. A.n(nRm -> -. n e. {j e. (F"x) | -. jRz}) <-> -. E.m e. {j e. (F"x) | -. jRz}A.n e. {j e. (F"x) | -. jRz} -. nRm)
77	68, 76	sylib 215	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((((R We A /\ x e. On) /\ ((F"x) C_ A /\ A.y e. x H =/= (/))) /\ (z e. A /\ -. z e. (F"x))) -> -. E.m e. {j e. (F"x) | -. jRz}A.n e. {j e. (F"x) | -. jRz} -. nRm)
78		simpll 448	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (((R We A /\ x e. On) /\ ((F"x) C_ A /\ A.y e. x H =/= (/))) -> R We A)
79	78	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (((((R We A /\ x e. On) /\ ((F"x) C_ A /\ A.y e. x H =/= (/))) /\ (z e. A /\ -. z e. (F"x))) /\ E.j e. (F"x) -. jRz) -> R We A)
80		ssrab2 2692	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- {j e. (F"x) | -. jRz} C_ (F"x)
81	80	a1i 8	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (((((R We A /\ x e. On) /\ ((F"x) C_ A /\ A.y e. x H =/= (/))) /\ (z e. A /\ -. z e. (F"x))) /\ E.j e. (F"x) -. jRz) -> {j e. (F"x) | -. jRz} C_ (F"x))
82		simprl 450	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (((R We A /\ x e. On) /\ ((F"x) C_ A /\ A.y e. x H =/= (/))) -> (F"x) C_ A)
83	82	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (((((R We A /\ x e. On) /\ ((F"x) C_ A /\ A.y e. x H =/= (/))) /\ (z e. A /\ -. z e. (F"x))) /\ E.j e. (F"x) -. jRz) -> (F"x) C_ A)
84	81, 83	sstrd 2627	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (((((R We A /\ x e. On) /\ ((F"x) C_ A /\ A.y e. x H =/= (/))) /\ (z e. A /\ -. z e. (F"x))) /\ E.j e. (F"x) -. jRz) -> {j e. (F"x) | -. jRz} C_ A)
85		hbrab1 2257	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (m e. {j e. (F"x) | -. jRz} -> A.j m e. {j e. (F"x) | -. jRz})
86		ax-17 1317	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (m e. (/) -> A.j m e. (/))
87	85, 86	hbne 2103	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ({j e. (F"x) | -. jRz} =/= (/) -> A.j{j e. (F"x) | -. jRz} =/= (/))
88		rabid 2253	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (j e. {j e. (F"x) | -. jRz} <-> (j e. (F"x) /\ -. jRz))
89		ne0i 2881	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (j e. {j e. (F"x) | -. jRz} -> {j e. (F"x) | -. jRz} =/= (/))
90	88, 89	sylbir 218	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ((j e. (F"x) /\ -. jRz) -> {j e. (F"x) | -. jRz} =/= (/))
91	90	ex 402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (j e. (F"x) -> (-. jRz -> {j e. (F"x) | -. jRz} =/= (/)))
92	87, 91	r19.23ai 2209	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (E.j e. (F"x) -. jRz -> {j e. (F"x) | -. jRz} =/= (/))
93	92	adantl 424	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (((((R We A /\ x e. On) /\ ((F"x) C_ A /\ A.y e. x H =/= (/))) /\ (z e. A /\ -. z e. (F"x))) /\ E.j e. (F"x) -. jRz) -> {j e. (F"x) | -. jRz} =/= (/))
94		visset 2295	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- x e. _V
95	94	funimaex 4496	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (Fun F -> (F"x) e. _V)
96	40, 95	ax-mp 7	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (F"x) e. _V
97	96, 80	ssexi 3456	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- {j e. (F"x) | -. jRz} e. _V
98	97	wereu 3654	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((R We A /\ {j e. (F"x) | -. jRz} C_ A /\ {j e. (F"x) | -. jRz} =/= (/)) -> E!m e. {j e. (F"x) | -. jRz}A.n e. {j e. (F"x) | -. jRz} -. nRm)
99	79, 84, 93, 98	syl111anc 1100	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (((((R We A /\ x e. On) /\ ((F"x) C_ A /\ A.y e. x H =/= (/))) /\ (z e. A /\ -. z e. (F"x))) /\ E.j e. (F"x) -. jRz) -> E!m e. {j e. (F"x) | -. jRz}A.n e. {j e. (F"x) | -. jRz} -. nRm)
100		reurex 2440	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (E!m e. {j e. (F"x) | -. jRz}A.n e. {j e. (F"x) | -. jRz} -. nRm -> E.m e. {j e. (F"x) | -. jRz}A.n e. {j e. (F"x) | -. jRz} -. nRm)
101	99, 100	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (((((R We A /\ x e. On) /\ ((F"x) C_ A /\ A.y e. x H =/= (/))) /\ (z e. A /\ -. z e. (F"x))) /\ E.j e. (F"x) -. jRz) -> E.m e. {j e. (F"x) | -. jRz}A.n e. {j e. (F"x) | -. jRz} -. nRm)
102	101	ex 402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((((R We A /\ x e. On) /\ ((F"x) C_ A /\ A.y e. x H =/= (/))) /\ (z e. A /\ -. z e. (F"x))) -> (E.j e. (F"x) -. jRz -> E.m e. {j e. (F"x) | -. jRz}A.n e. {j e. (F"x) | -. jRz} -. nRm))
103		rexnal 2114	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (E.j e. (F"x) -. jRz <-> -. A.j e. (F"x)jRz)
104	102, 103	syl5ibr 224	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((((R We A /\ x e. On) /\ ((F"x) C_ A /\ A.y e. x H =/= (/))) /\ (z e. A /\ -. z e. (F"x))) -> (-. A.j e. (F"x)jRz -> E.m e. {j e. (F"x) | -. jRz}A.n e. {j e. (F"x) | -. jRz} -. nRm))
105	77, 104	mt3d 129	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((((R We A /\ x e. On) /\ ((F"x) C_ A /\ A.y e. x H =/= (/))) /\ (z e. A /\ -. z e. (F"x))) -> A.j e. (F"x)jRz)
106	105	ex 402	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((R We A /\ x e. On) /\ ((F"x) C_ A /\ A.y e. x H =/= (/))) -> ((z e. A /\ -. z e. (F"x)) -> A.j e. (F"x)jRz))
107	50, 106	jcad 661	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((R We A /\ x e. On) /\ ((F"x) C_ A /\ A.y e. x H =/= (/))) -> ((z e. A /\ -. z e. (F"x)) -> (z e. A /\ A.j e. (F"x)jRz)))
108		breq2 3342	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (w = z -> (jRw <-> jRz))
109	108	ralbidv 2123	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (w = z -> (A.j e. (F"x)jRw <-> A.j e. (F"x)jRz))
110	109	elrab 2414	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (z e. {w e. A | A.j e. (F"x)jRw} <-> (z e. A /\ A.j e. (F"x)jRz))
111	107, 110	syl6ibr 230	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((R We A /\ x e. On) /\ ((F"x) C_ A /\ A.y e. x H =/= (/))) -> ((z e. A /\ -. z e. (F"x)) -> z e. {w e. A | A.j e. (F"x)jRw}))
112		ne0i 2881	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (z e. {w e. A | A.j e. (F"x)jRw} -> {w e. A | A.j e. (F"x)jRw} =/= (/))
113	111, 112	syl6 25	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((R We A /\ x e. On) /\ ((F"x) C_ A /\ A.y e. x H =/= (/))) -> ((z e. A /\ -. z e. (F"x)) -> {w e. A | A.j e. (F"x)jRw} =/= (/)))
114	113	19.23adv 1584	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((R We A /\ x e. On) /\ ((F"x) C_ A /\ A.y e. x H =/= (/))) -> (E.z(z e. A /\ -. z e. (F"x)) -> {w e. A | A.j e. (F"x)jRw} =/= (/)))
115	114	impr 422	. . . . . . . . . . . . . . . . . . . . . 22 |- (((R We A /\ x e. On) /\ (((F"x) C_ A /\ A.y e. x H =/= (/)) /\ E.z(z e. A /\ -. z e. (F"x)))) -> {w e. A | A.j e. (F"x)jRw} =/= (/))
116	1, 47	ssexi 3456	. . . . . . . . . . . . . . . . . . . . . . 23 |- {w e. A | A.j e. (F"x)jRw} e. _V
117	116	wereucl 3655	. . . . . . . . . . . . . . . . . . . . . 22 |- ((R We A /\ {w e. A | A.j e. (F"x)jRw} C_ A /\ {w e. A | A.j e. (F"x)jRw} =/= (/)) -> U.{m e. {w e. A | A.j e. (F"x)jRw} | A.n e. {w e. A | A.j e. (F"x)jRw} -. nRm} e. {w e. A | A.j e. (F"x)jRw})
118	46, 48, 115, 117	syl111anc 1100	. . . . . . . . . . . . . . . . . . . . 21 |- (((R We A /\ x e. On) /\ (((F"x) C_ A /\ A.y e. x H =/= (/)) /\ E.z(z e. A /\ -. z e. (F"x)))) -> U.{m e. {w e. A | A.j e. (F"x)jRw} | A.n e. {w e. A | A.j e. (F"x)jRw} -. nRm} e. {w e. A | A.j e. (F"x)jRw})
119	118, 5	syl6eleqr 1982	. . . . . . . . . . . . . . . . . . . 20 |- (((R We A /\ x e. On) /\ (((F"x) C_ A /\ A.y e. x H =/= (/)) /\ E.z(z e. A /\ -. z e. (F"x)))) -> U.{m e. {w e. A | A.j e. (F"x)jRw} | A.n e. {w e. A | A.j e. (F"x)jRw} -. nRm} e. D)
120	119	expr 418	. . . . . . . . . . . . . . . . . . 19 |- (((R We A /\ x e. On) /\ ((F"x) C_ A /\ A.y e. x H =/= (/))) -> (E.z(z e. A /\ -. z e. (F"x)) -> U.{m e. {w e. A | A.j e. (F"x)jRw} | A.n e. {w e. A | A.j e. (F"x)jRw} -. nRm} e. D))
121		n0i 2880	. . . . . . . . . . . . . . . . . . 19 |- (U.{m e. {w e. A | A.j e. (F"x)jRw} | A.n e. {w e. A | A.j e. (F"x)jRw} -. nRm} e. D -> -. D = (/))
122	120, 121	syl6 25	. . . . . . . . . . . . . . . . . 18 |- (((R We A /\ x e. On) /\ ((F"x) C_ A /\ A.y e. x H =/= (/))) -> (E.z(z e. A /\ -. z e. (F"x)) -> -. D = (/)))
123		nss 2670	. . . . . . . . . . . . . . . . . 18 |- (-. A C_ (F"x) <-> E.z(z e. A /\ -. z e. (F"x)))
124	122, 123	syl5ib 223	. . . . . . . . . . . . . . . . 17 |- (((R We A /\ x e. On) /\ ((F"x) C_ A /\ A.y e. x H =/= (/))) -> (-. A C_ (F"x) -> -. D = (/)))
125	124	con4d 91	. . . . . . . . . . . . . . . 16 |- (((R We A /\ x e. On) /\ ((F"x) C_ A /\ A.y e. x H =/= (/))) -> (D = (/) -> A C_ (F"x)))
126	125	expr 418	. . . . . . . . . . . . . . 15 |- (((R We A /\ x e. On) /\ (F"x) C_ A) -> (A.y e. x H =/= (/) -> (D = (/) -> A C_ (F"x))))
127	126	com23 36	. . . . . . . . . . . . . 14 |- (((R We A /\ x e. On) /\ (F"x) C_ A) -> (D = (/) -> (A.y e. x H =/= (/) -> A C_ (F"x))))
128	127	imp3a 388	. . . . . . . . . . . . 13 |- (((R We A /\ x e. On) /\ (F"x) C_ A) -> ((D = (/) /\ A.y e. x H =/= (/)) -> A C_ (F"x)))
129	128	ex 402	. . . . . . . . . . . 12 |- ((R We A /\ x e. On) -> ((F"x) C_ A -> ((D = (/) /\ A.y e. x H =/= (/)) -> A C_ (F"x))))
130	129	com23 36	. . . . . . . . . . 11 |- ((R We A /\ x e. On) -> ((D = (/) /\ A.y e. x H =/= (/)) -> ((F"x) C_ A -> A C_ (F"x))))
131	130	imp 377	. . . . . . . . . 10 |- (((R We A /\ x e. On) /\ (D = (/) /\ A.y e. x H =/= (/))) -> ((F"x) C_ A -> A C_ (F"x)))
132	45, 131	jcai 313	. . . . . . . . 9 |- (((R We A /\ x e. On) /\ (D = (/) /\ A.y e. x H =/= (/))) -> ((F"x) C_ A /\ A C_ (F"x)))
133		eqss 2631	. . . . . . . . 9 |- ((F"x) = A <-> ((F"x) C_ A /\ A C_ (F"x)))
134	132, 133	sylibr 217	. . . . . . . 8 |- (((R We A /\ x e. On) /\ (D = (/) /\ A.y e. x H =/= (/))) -> (F"x) = A)
135		df-ima 4007	. . . . . . . 8 |- (F"x) = ran ( F |` x)
136	134, 135	syl5eqr 1942	. . . . . . 7 |- (((R We A /\ x e. On) /\ (D = (/) /\ A.y e. x H =/= (/))) -> ran ( F |` x) = A)
137	15, 16, 136	3jca 1050	. . . . . 6 |- (((R We A /\ x e. On) /\ (D = (/) /\ A.y e. x H =/= (/))) -> ((F |` x) Fn x /\ Fun `'(F |` x) /\ ran ( F |` x) = A))
138		dff1o2 4639	. . . . . 6 |- ((F |` x):x-1-1-onto->A <-> ((F |` x) Fn x /\ Fun `'(F |` x) /\ ran ( F |` x) = A))
139	137, 138	sylibr 217	. . . . 5 |- (((R We A /\ x e. On) /\ (D = (/) /\ A.y e. x H =/= (/))) -> (F |` x):x-1-1-onto->A)
140		onelon 3683	. . . . . . . . . . . . . 14 |- ((x e. On /\ z e. x) -> z e. On)
141	140	adantll 428	. . . . . . . . . . . . 13 |- (((R We A /\ x e. On) /\ z e. x) -> z e. On)
142	141	ad2ant2r 445	. . . . . . . . . . . 12 |- ((((R We A /\ x e. On) /\ A.y e. x H =/= (/)) /\ (z e. x /\ y e. x)) -> z e. On)
143		simplll 452	. . . . . . . . . . . 12 |- ((((R We A /\ x e. On) /\ A.y e. x H =/= (/)) /\ (z e. x /\ y e. x)) -> R We A)
144		visset 2295	. . . . . . . . . . . . . . . . 17 |- z e. _V
145		ax-17 1317	. . . . . . . . . . . . . . . . 17 |- (m e. z -> A.y m e. z)
146	144, 145	hbcsb1 2568	. . . . . . . . . . . . . . . 16 |- (m e. [_z / y]_H -> A.y m e. [_z / y]_H)
147		ax-17 1317	. . . . . . . . . . . . . . . 16 |- (m e. (/) -> A.y m e. (/))
148	146, 147	hbne 2103	. . . . . . . . . . . . . . 15 |- ([_z / y]_H =/= (/) -> A.y[_z / y]_H =/= (/))
149		csbeq1a 2546	. . . . . . . . . . . . . . . 16 |- (y = z -> H = [_z / y]_H)
150	149	neeq1d 2028	. . . . . . . . . . . . . . 15 |- (y = z -> (H =/= (/) <-> [_z / y]_H =/= (/)))
151	148, 150	rcla4 2373	. . . . . . . . . . . . . 14 |- (z e. x -> (A.y e. x H =/= (/) -> [_z / y]_H =/= (/)))
152	151	impcom 378	. . . . . . . . . . . . 13 |- ((A.y e. x H =/= (/) /\ z e. x) -> [_z / y]_H =/= (/))
153	152	ad2ant2lr 446	. . . . . . . . . . . 12 |- ((((R We A /\ x e. On) /\ A.y e. x H =/= (/)) /\ (z e. x /\ y e. x)) -> [_z / y]_H =/= (/))
154		ax-17 1317	. . . . . . . . . . . . . . . 16 |- (m e. {w e. A | A.j e. (F"z)jRw} -> A.x m e. {w e. A | A.j e. (F"z)jRw})
155	144, 154	csbieb 2574	. . . . . . . . . . . . . . 15 |- (A.x(x = z -> D = {w e. A | A.j e. (F"z)jRw}) <-> [_z / x]_D = {w e. A | A.j e. (F"z)jRw})
156		imaeq2 4260	. . . . . . . . . . . . . . . . . 18 |- (x = z -> (F"x) = (F"z))
157	156	raleqdv 2269	. . . . . . . . . . . . . . . . 17 |- (x = z -> (A.j e. (F"x)jRw <-> A.j e. (F"z)jRw))
158	157	rabbidv 2287	. . . . . . . . . . . . . . . 16 |- (x = z -> {w e. A | A.j e. (F"x)jRw} = {w e. A | A.j e. (F"z)jRw})
159	158, 5	syl5eq 1940	. . . . . . . . . . . . . . 15 |- (x = z -> D = {w e. A | A.j e. (F"z)jRw})
160	155, 159	mpgbi 1333	. . . . . . . . . . . . . 14 |- [_z / x]_D = {w e. A | A.j e. (F"z)jRw}
161	1, 2, 3, 4, 160, 6, 7	ordtypelem2 5685	. . . . . . . . . . . . 13 |- ((z e. On /\ R We A /\ [_z / x]_D =/= (/)) -> (y e. z -> (F` y)R(F` z)))
162		imaeq2 4260	. . . . . . . . . . . . . . . . . . 19 |- (y = x -> (F"y) = (F"x))
163	162	raleqdv 2269	. . . . . . . . . . . . . . . . . 18 |- (y = x -> (A.j e. (F"y)jRw <-> A.j e. (F"x)jRw))
164	163	rabbidv 2287	. . . . . . . . . . . . . . . . 17 |- (y = x -> {w e. A | A.j e. (F"y)jRw} = {w e. A | A.j e. (F"x)jRw})
165	164, 7, 5	3eqtr4g 1953	. . . . . . . . . . . . . . . 16 |- (y = x -> H = D)
166	165	cbvcsbv 2543	. . . . . . . . . . . . . . 15 |- (z e. _V -> [_z / y]_H = [_z / x]_D)
167	144, 166	ax-mp 7	. . . . . . . . . . . . . 14 |- [_z / y]_H = [_z / x]_D
168	167	neeq1i 2026	. . . . . . . . . . . . 13 |- ([_z / y]_H =/= (/) <-> [_z / x]_D =/= (/))
169	161, 168	syl3an3b 1135	. . . . . . . . . . . 12 |- ((z e. On /\ R We A /\ [_z / y]_H =/= (/)) -> (y e. z -> (F` y)R(F` z)))
170	142, 143, 153, 169	syl111anc 1100	. . . . . . . . . . 11 |- ((((R We A /\ x e. On) /\ A.y e. x H =/= (/)) /\ (z e. x /\ y e. x)) -> (y e. z -> (F` y)R(F` z)))
171		fveq2 4681	. . . . . . . . . . . . . 14 |- (y = z -> (F` y) = (F` z))
172	171	a1i 8	. . . . . . . . . . . . 13 |- ((((R We A /\ x e. On) /\ A.y e. x H =/= (/)) /\ (z e. x /\ y e. x)) -> (y = z -> (F` y) = (F` z)))
173	29	adantll 428	. . . . . . . . . . . . . . 15 |- (((R We A /\ x e. On) /\ y e. x) -> y e. On)
174	173	ad2ant2rl 447	. . . . . . . . . . . . . 14 |- ((((R We A /\ x e. On) /\ A.y e. x H =/= (/)) /\ (z e. x /\ y e. x)) -> y e. On)
175	36	imp 377	. . . . . . . . . . . . . . 15 |- ((A.y e. x H =/= (/) /\ y e. x) -> H =/= (/))
176	175	ad2ant2l 444	. . . . . . . . . . . . . 14 |- ((((R We A /\ x e. On) /\ A.y e. x H =/= (/)) /\ (z e. x /\ y e. x)) -> H =/= (/))
177	1, 2, 3, 4, 7, 6, 160	ordtypelem2 5685	. . . . . . . . . . . . . 14 |- ((y e. On /\ R We A /\ H =/= (/)) -> (z e. y -> (F` z)R(F` y)))
178	174, 143, 176, 177	syl111anc 1100	. . . . . . . . . . . . 13 |- ((((R We A /\ x e. On) /\ A.y e. x H =/= (/)) /\ (z e. x /\ y e. x)) -> (z e. y -> (F` z)R(F` y)))
179	172, 178	orim12d 624	. . . . . . . . . . . 12 |- ((((R We A /\ x e. On) /\ A.y e. x H =/= (/)) /\ (z e. x /\ y e. x)) -> ((y = z \/ z e. y) -> ((F` y) = (F` z) \/ (F` z)R(F` y))))
180		eloni 3667	. . . . . . . . . . . . . 14 |- (y e. On -> Ord y)
181	174, 180	syl 12	. . . . . . . . . . . . 13 |- ((((R We A /\ x e. On) /\ A.y e. x H =/= (/)) /\ (z e. x /\ y e. x)) -> Ord y)
182		eloni 3667	. . . . . . . . . . . . . 14 |- (z e. On -> Ord z)
183	142, 182	syl 12	. . . . . . . . . . . . 13 |- ((((R We A /\ x e. On) /\ A.y e. x H =/= (/)) /\ (z e. x /\ y e. x)) -> Ord z)
184		ordtri2 3696	. . . . . . . . . . . . . 14 |- ((Ord y /\ Ord z) -> (y e. z <-> -. (y = z \/ z e. y)))
185	184	con2bid 585	. . . . . . . . . . . . 13 |- ((Ord y /\ Ord z) -> ((y = z \/ z e. y) <-> -. y e. z))
186	181, 183, 185	syl11anc 524	. . . . . . . . . . . 12 |- ((((R We A /\ x e. On) /\ A.y e. x H =/= (/)) /\ (z e. x /\ y e. x)) -> ((y = z \/ z e. y) <-> -. y e. z))
187		weso 3649	. . . . . . . . . . . . . . 15 |- (R We A -> R Or A)
188	187	adantr 425	. . . . . . . . . . . . . 14 |- ((R We A /\ x e. On) -> R Or A)
189	188	ad2antrr 440	. . . . . . . . . . . . 13 |- ((((R We A /\ x e. On) /\ A.y e. x H =/= (/)) /\ (z e. x /\ y e. x)) -> R Or A)
190	25	a1i 8	. . . . . . . . . . . . . 14 |- ((((R We A /\ x e. On) /\ A.y e. x H =/= (/)) /\ (z e. x /\ y e. x)) -> H C_ A)
191	174, 143, 176, 22	syl111anc 1100	. . . . . . . . . . . . . 14 |- ((((R We A /\ x e. On) /\ A.y e. x H =/= (/)) /\ (z e. x /\ y e. x)) -> (F` y) e. H)
192	190, 191	sseldd 2620	. . . . . . . . . . . . 13 |- ((((R We A /\ x e. On) /\ A.y e. x H =/= (/)) /\ (z e. x /\ y e. x)) -> (F` y) e. A)
193		ax-17 1317	. . . . . . . . . . . . . . . . 17 |- (m e. A -> A.y m e. A)
194	146, 193	hbss 2614	. . . . . . . . . . . . . . . 16 |- ([_z / y]_H C_ A -> A.y[_z / y]_H C_ A)
195	149	sseq1d 2644	. . . . . . . . . . . . . . . 16 |- (y = z -> (H C_ A <-> [_z / y]_H C_ A))
196	194, 195, 25	chvar 1530	. . . . . . . . . . . . . . 15 |- [_z / y]_H C_ A
197	196	a1i 8	. . . . . . . . . . . . . 14 |- ((((R We A /\ x e. On) /\ A.y e. x H =/= (/)) /\ (z e. x /\ y e. x)) -> [_z / y]_H C_ A)
198		ax-17 1317	. . . . . . . . . . . . . . . . . 18 |- (m e. {w e. A | A.j e. (F"z)jRw} -> A.y m e. {w e. A | A.j e. (F"z)jRw})
199	144, 198	csbieb 2574	. . . . . . . . . . . . . . . . 17 |- (A.y(y = z -> H = {w e. A | A.j e. (F"z)jRw}) <-> [_z / y]_H = {w e. A | A.j e. (F"z)jRw})
200		imaeq2 4260	. . . . . . . . . . . . . . . . . . . 20 |- (y = z -> (F"y) = (F"z))
201	200	raleqdv 2269	. . . . . . . . . . . . . . . . . . 19 |- (y = z -> (A.j e. (F"y)jRw <-> A.j e. (F"z)jRw))
202	201	rabbidv 2287	. . . . . . . . . . . . . . . . . 18 |- (y = z -> {w e. A | A.j e. (F"y)jRw} = {w e. A | A.j e. (F"z)jRw})
203	202, 7	syl5eq 1940	. . . . . . . . . . . . . . . . 17 |- (y = z -> H = {w e. A | A.j e. (F"z)jRw})
204	199, 203	mpgbi 1333	. . . . . . . . . . . . . . . 16 |- [_z / y]_H = {w e. A | A.j e. (F"z)jRw}
205	1, 2, 3, 4, 204, 6, 5	ordtypelem1 5684	. . . . . . . . . . . . . . 15 |- ((z e. On /\ R We A /\ [_z / y]_H =/= (/)) -> (F` z) e. [_z / y]_H)
206	142, 143, 153, 205	syl111anc 1100	. . . . . . . . . . . . . 14 |- ((((R We A /\ x e. On) /\ A.y e. x H =/= (/)) /\ (z e. x /\ y e. x)) -> (F` z) e. [_z / y]_H)
207	197, 206	sseldd 2620	. . . . . . . . . . . . 13 |- ((((R We A /\ x e. On) /\ A.y e. x H =/= (/)) /\ (z e. x /\ y e. x)) -> (F` z) e. A)
208		sotric 3615	. . . . . . . . . . . . . 14 |- ((R Or A /\ ((F` y) e. A /\ (F` z) e. A)) -> ((F` y)R(F` z) <-> -. ((F` y) = (F` z) \/ (F` z)R(F` y))))
209	208	con2bid 585	. . . . . . . . . . . . 13 |- ((R Or A /\ ((F` y) e. A /\ (F` z) e. A)) -> (((F` y) = (F` z) \/ (F` z)R(F` y)) <-> -. (F` y)R(F` z)))
210	189, 192, 207, 209	syl12anc 1098	. . . . . . . . . . . 12 |- ((((R We A /\ x e. On) /\ A.y e. x H =/= (/)) /\ (z e. x /\ y e. x)) -> (((F` y) = (F` z) \/ (F` z)R(F` y)) <-> -. (F` y)R(F` z)))
211	179, 186, 210	3imtr3d 601	. . . . . . . . . . 11 |- ((((R We A /\ x e. On) /\ A.y e. x H =/= (/)) /\ (z e. x /\ y e. x)) -> (-. y e. z -> -. (F` y)R(F` z)))
212	170, 211	impcon4bid 578	. . . . . . . . . 10 |- ((((R We A /\ x e. On) /\ A.y e. x H =/= (/)) /\ (z e. x /\ y e. x)) -> (y e. z <-> (F` y)R(F` z)))
213		epel 3585	. . . . . . . . . . 11 |- (y _E z <-> y e. z)
214	213	a1i 8	. . . . . . . . . 10 |- ((((R We A /\ x e. On) /\ A.y e. x H =/= (/)) /\ (z e. x /\ y e. x)) -> (y _E z <-> y e. z))
215		fvres 4691	. . . . . . . . . . . 12 |- (y e. x -> ((F |` x)` y) = (F` y))
216		fvres 4691	. . . . . . . . . . . 12 |- (z e. x -> ((F |` x)` z) = (F` z))
217	215, 216	breqan12rd 3355	. . . . . . . . . . 11 |- ((z e. x /\ y e. x) -> (((F |` x)` y)R((F |` x)` z) <-> (F` y)R(F` z)))
218	217	adantl 424	. . . . . . . . . 10 |- ((((R We A /\ x e. On) /\ A.y e. x H =/= (/)) /\ (z e. x /\ y e. x)) -> (((F |` x)` y)R((F |` x)` z) <-> (F` y)R(F` z)))
219	212, 214, 218	3bitr4d 609	. . . . . . . . 9 |- ((((R We A /\ x e. On) /\ A.y e. x H =/= (/)) /\ (z e. x /\ y e. x)) -> (y _E z <-> ((F |` x)` y)R((F |` x)` z)))
220	219	expr 418	. . . . . . . 8 |- ((((R We A /\ x e. On) /\ A.y e. x H =/= (/)) /\ z e. x) -> (y e. x -> (y _E z <-> ((F |` x)` y)R((F |` x)` z))))
221	220	r19.21adva 2182	. . . . . . 7 |- (((R We A /\ x e. On) /\ A.y e. x H =/= (/)) -> (y e. x -> A.z e. x (y _E z <-> ((F |` x)` y)R((F |` x)` z))))
222	19, 221	r19.21ai 2174	. . . . . 6 |- (((R We A /\ x e. On) /\ A.y e. x H =/= (/)) -> A.y e. x A.z e. x (y _E z <-> ((F |` x)` y)R((F |` x)` z)))
223	222	adantrl 430	. . . . 5 |- (((R We A /\ x e. On) /\ (D = (/) /\ A.y e. x H =/= (/))) -> A.y e. x A.z e. x (y _E z <-> ((F |` x)` y)R((F |` x)` z)))
224	9, 139, 223	sylanbrc 527	. . . 4 |- (((R We A /\ x e. On) /\ (D = (/) /\ A.y e. x H =/= (/))) -> (F |` x) Isom _E , R (x, A))
225	224	exp31 407	. . 3 |- (R We A -> (x e. On -> ((D = (/) /\ A.y e. x H =/= (/)) -> (F |` x) Isom _E , R (x, A))))
226	225	reximdvai 2201	. 2 |- (R We A -> (E.x e. On (D = (/) /\ A.y e. x H =/= (/)) -> E.x e. On (F |` x) Isom _E , R (x, A)))
227	8, 226	mpd 29	1 |- (R We A -> E.x e. On (F |` x) Isom _E , R (x, A))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   \/ wo 239   /\ wa 240   /\ w3a 858  A.wal 1296   = wceq 1298   e. wcel 1300  E.wex 1326  {cab 1871   =/= wne 2017  A.wral 2105  E.wrex 2106  E!wreu 2107  {crab 2108  _Vcvv 2292  [_csb 2540   C_ wss 2593  (/)c0 2875  U.cuni 3177   class class class wbr 3338  {copab 3395   _E cep 3581   Or wor 3590   We wwe 3624  Ord word 3656  Oncon0 3657  `'ccnv 3985  ran crn 3987   |` cres 3988  "cima 3989  Fun wfun 3992   Fn wfn 3993  -1-1-onto->wf1o 3997  ` cfv 3998   Isom wiso 3999

This theorem is referenced by:  ordtype 5691  ordtypeOLD 15382

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-fo 4012  df-f1o 4013  df-fv 4014  df-iso 4015

Copyright terms: Public domain