Theorem ordtypelem6 5689

Description: Lemma for ordtype 5691. If z is not in (F"x), m is in (F"x), and every element of (F"x) which is less than m is also less than z, m is also less than z.

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
ordtypelem6	|- ((((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))

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

Proof of Theorem ordtypelem6

Step	Hyp	Ref	Expression
1		eleq1 1957	. . . . . . 7 |- (r = x -> (r e. On <-> x e. On))
2	1	anbi2d 678	. . . . . 6 |- (r = x -> ((R We A /\ r e. On) <-> (R We A /\ x e. On)))
3		imaeq2 4260	. . . . . . . 8 |- (r = x -> (F"r) = (F"x))
4	3	sseq1d 2644	. . . . . . 7 |- (r = x -> ((F"r) C_ A <-> (F"x) C_ A))
5		raleq 2266	. . . . . . 7 |- (r = x -> (A.y e. r H =/= (/) <-> A.y e. x H =/= (/)))
6	4, 5	anbi12d 690	. . . . . 6 |- (r = x -> (((F"r) C_ A /\ A.y e. r H =/= (/)) <-> ((F"x) C_ A /\ A.y e. x H =/= (/))))
7	2, 6	anbi12d 690	. . . . 5 |- (r = x -> (((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) <-> ((R We A /\ x e. On) /\ ((F"x) C_ A /\ A.y e. x H =/= (/)))))
8	3	eleq2d 1964	. . . . . . . 8 |- (r = x -> (z e. (F"r) <-> z e. (F"x)))
9	8	notbid 673	. . . . . . 7 |- (r = x -> (-. z e. (F"r) <-> -. z e. (F"x)))
10	9	anbi2d 678	. . . . . 6 |- (r = x -> ((z e. A /\ -. z e. (F"r)) <-> (z e. A /\ -. z e. (F"x))))
11	3	eleq2d 1964	. . . . . 6 |- (r = x -> (m e. (F"r) <-> m e. (F"x)))
12	10, 11	anbi12d 690	. . . . 5 |- (r = x -> (((z e. A /\ -. z e. (F"r)) /\ m e. (F"r)) <-> ((z e. A /\ -. z e. (F"x)) /\ m e. (F"x))))
13	7, 12	anbi12d 690	. . . 4 |- (r = x -> ((((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) /\ ((z e. A /\ -. z e. (F"r)) /\ m e. (F"r))) <-> (((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)))))
14	3	eleq2d 1964	. . . . . . . 8 |- (r = x -> (n e. (F"r) <-> n e. (F"x)))
15	14	imbi1d 675	. . . . . . 7 |- (r = x -> ((n e. (F"r) -> nRz) <-> (n e. (F"x) -> nRz)))
16	15	imbi2d 674	. . . . . 6 |- (r = x -> ((nRm -> (n e. (F"r) -> nRz)) <-> (nRm -> (n e. (F"x) -> nRz))))
17	16	albidv 1656	. . . . 5 |- (r = x -> (A.n(nRm -> (n e. (F"r) -> nRz)) <-> A.n(nRm -> (n e. (F"x) -> nRz))))
18	17	imbi1d 675	. . . 4 |- (r = x -> ((A.n(nRm -> (n e. (F"r) -> nRz)) -> mRz) <-> (A.n(nRm -> (n e. (F"x) -> nRz)) -> mRz)))
19	13, 18	imbi12d 688	. . 3 |- (r = x -> (((((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) /\ ((z e. A /\ -. z e. (F"r)) /\ m e. (F"r))) -> (A.n(nRm -> (n e. (F"r) -> nRz)) -> mRz)) <-> ((((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))))
20	19	a4v 1649	. 2 |- (A.r((((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) /\ ((z e. A /\ -. z e. (F"r)) /\ m e. (F"r))) -> (A.n(nRm -> (n e. (F"r) -> nRz)) -> mRz)) -> ((((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)))
21		onelon 3683	. . . . . . . . . . . . 13 |- ((r e. On /\ x e. r) -> x e. On)
22		ordtypelem.2	. . . . . . . . . . . . . 14 |- B = {h | E.b e. On (h Fn b /\ A.c e. b (h` c) = (G` (h |` c)))}
23		ordtypelem.3	. . . . . . . . . . . . . 14 |- F = U.B
24	22, 23	tfr2 5133	. . . . . . . . . . . . 13 |- (x e. On -> (F` x) = (G` (F |` x)))
25	21, 24	syl 12	. . . . . . . . . . . 12 |- ((r e. On /\ x e. r) -> (F` x) = (G` (F |` x)))
26	25	adantll 428	. . . . . . . . . . 11 |- (((R We A /\ r e. On) /\ x e. r) -> (F` x) = (G` (F |` x)))
27	26	adantlr 429	. . . . . . . . . 10 |- ((((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) /\ x e. r) -> (F` x) = (G` (F |` x)))
28	27	adantlr 429	. . . . . . . . 9 |- (((((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) /\ (z e. A /\ -. z e. (F"r))) /\ x e. r) -> (F` x) = (G` (F |` x)))
29		ordtypelem.6	. . . . . . . . . . 11 |- G = {<.h, c>. | c = U.{v e. C | A.u e. C -. uRv}}
30	29	fveq1i 4682	. . . . . . . . . 10 |- (G` (F |` x)) = ({<.h, c>. | c = U.{v e. C | A.u e. C -. uRv}}` (F |` x))
31	22, 23	tfrlem7 5125	. . . . . . . . . . . 12 |- Fun F
32		visset 2295	. . . . . . . . . . . 12 |- x e. _V
33		resfunexg 4500	. . . . . . . . . . . 12 |- ((Fun F /\ x e. _V) -> (F |` x) e. _V)
34	31, 32, 33	mp2an 761	. . . . . . . . . . 11 |- (F |` x) e. _V
35		ordtypelem.5	. . . . . . . . . . . . . 14 |- D = {w e. A | A.j e. (F"x)jRw}
36		ordtypelem.1	. . . . . . . . . . . . . . 15 |- A e. _V
37	36	rabex 3461	. . . . . . . . . . . . . 14 |- {w e. A | A.j e. (F"x)jRw} e. _V
38	35, 37	eqeltri 1967	. . . . . . . . . . . . 13 |- D e. _V
39	38	rabex 3461	. . . . . . . . . . . 12 |- {v e. D | A.u e. D -. uRv} e. _V
40	39	uniex 3794	. . . . . . . . . . 11 |- U.{v e. D | A.u e. D -. uRv} e. _V
41		rneq 4186	. . . . . . . . . . . . . . . . . . . 20 |- (h = (F |` x) -> ran h = ran ( F |` x))
42		df-ima 4007	. . . . . . . . . . . . . . . . . . . 20 |- (F"x) = ran ( F |` x)
43	41, 42	syl6eqr 1946	. . . . . . . . . . . . . . . . . . 19 |- (h = (F |` x) -> ran h = (F"x))
44	43	raleqdv 2269	. . . . . . . . . . . . . . . . . 18 |- (h = (F |` x) -> (A.j e. ran h jRw <-> A.j e. (F"x)jRw))
45	44	rabbidv 2287	. . . . . . . . . . . . . . . . 17 |- (h = (F |` x) -> {w e. A | A.j e. ran h jRw} = {w e. A | A.j e. (F"x)jRw})
46		ordtypelem.4	. . . . . . . . . . . . . . . . 17 |- C = {w e. A | A.j e. ran h jRw}
47	45, 46, 35	3eqtr4g 1953	. . . . . . . . . . . . . . . 16 |- (h = (F |` x) -> C = D)
48	47	eleq2d 1964	. . . . . . . . . . . . . . 15 |- (h = (F |` x) -> (v e. C <-> v e. D))
49	47	raleqdv 2269	. . . . . . . . . . . . . . 15 |- (h = (F |` x) -> (A.u e. C -. uRv <-> A.u e. D -. uRv))
50	48, 49	anbi12d 690	. . . . . . . . . . . . . 14 |- (h = (F |` x) -> ((v e. C /\ A.u e. C -. uRv) <-> (v e. D /\ A.u e. D -. uRv)))
51	50	abbidv 2008	. . . . . . . . . . . . 13 |- (h = (F |` x) -> {v | (v e. C /\ A.u e. C -. uRv)} = {v | (v e. D /\ A.u e. D -. uRv)})
52		df-rab 2112	. . . . . . . . . . . . 13 |- {v e. C | A.u e. C -. uRv} = {v | (v e. C /\ A.u e. C -. uRv)}
53		df-rab 2112	. . . . . . . . . . . . 13 |- {v e. D | A.u e. D -. uRv} = {v | (v e. D /\ A.u e. D -. uRv)}
54	51, 52, 53	3eqtr4g 1953	. . . . . . . . . . . 12 |- (h = (F |` x) -> {v e. C | A.u e. C -. uRv} = {v e. D | A.u e. D -. uRv})
55	54	unieqd 3188	. . . . . . . . . . 11 |- (h = (F |` x) -> U.{v e. C | A.u e. C -. uRv} = U.{v e. D | A.u e. D -. uRv})
56	34, 40, 55	fvopab 4753	. . . . . . . . . 10 |- ({<.h, c>. | c = U.{v e. C | A.u e. C -. uRv}}` (F |` x)) = U.{v e. D | A.u e. D -. uRv}
57	30, 56	eqtri 1908	. . . . . . . . 9 |- (G` (F |` x)) = U.{v e. D | A.u e. D -. uRv}
58	28, 57	syl6eq 1944	. . . . . . . 8 |- (((((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) /\ (z e. A /\ -. z e. (F"r))) /\ x e. r) -> (F` x) = U.{v e. D | A.u e. D -. uRv})
59	58	eqeq1d 1892	. . . . . . 7 |- (((((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) /\ (z e. A /\ -. z e. (F"r))) /\ x e. r) -> ((F` x) = m <-> U.{v e. D | A.u e. D -. uRv} = m))
60		breq2 3342	. . . . . . . . . . 11 |- (U.{v e. D | A.u e. D -. uRv} = m -> (nRU.{v e. D | A.u e. D -. uRv} <-> nRm))
61	60	imbi1d 675	. . . . . . . . . 10 |- (U.{v e. D | A.u e. D -. uRv} = m -> ((nRU.{v e. D | A.u e. D -. uRv} -> (n e. (F"r) -> nRz)) <-> (nRm -> (n e. (F"r) -> nRz))))
62	61	albidv 1656	. . . . . . . . 9 |- (U.{v e. D | A.u e. D -. uRv} = m -> (A.n(nRU.{v e. D | A.u e. D -. uRv} -> (n e. (F"r) -> nRz)) <-> A.n(nRm -> (n e. (F"r) -> nRz))))
63		breq1 3341	. . . . . . . . 9 |- (U.{v e. D | A.u e. D -. uRv} = m -> (U.{v e. D | A.u e. D -. uRv}Rz <-> mRz))
64	62, 63	imbi12d 688	. . . . . . . 8 |- (U.{v e. D | A.u e. D -. uRv} = m -> ((A.n(nRU.{v e. D | A.u e. D -. uRv} -> (n e. (F"r) -> nRz)) -> U.{v e. D | A.u e. D -. uRv}Rz) <-> (A.n(nRm -> (n e. (F"r) -> nRz)) -> mRz)))
65		simpll 448	. . . . . . . . . . . 12 |- (((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) -> R We A)
66	65	ad2antrr 440	. . . . . . . . . . 11 |- (((((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) /\ (z e. A /\ -. z e. (F"r))) /\ x e. r) -> R We A)
67		ssrab2 2692	. . . . . . . . . . . . 13 |- {w e. A | A.j e. (F"x)jRw} C_ A
68	35, 67	eqsstri 2647	. . . . . . . . . . . 12 |- D C_ A
69	68	a1i 8	. . . . . . . . . . 11 |- (((((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) /\ (z e. A /\ -. z e. (F"r))) /\ x e. r) -> D C_ A)
70		imaeq2 4260	. . . . . . . . . . . . . . . . . . 19 |- (y = x -> (F"y) = (F"x))
71	70	raleqdv 2269	. . . . . . . . . . . . . . . . . 18 |- (y = x -> (A.j e. (F"y)jRw <-> A.j e. (F"x)jRw))
72	71	rabbidv 2287	. . . . . . . . . . . . . . . . 17 |- (y = x -> {w e. A | A.j e. (F"y)jRw} = {w e. A | A.j e. (F"x)jRw})
73		ordtypelem.7	. . . . . . . . . . . . . . . . 17 |- H = {w e. A | A.j e. (F"y)jRw}
74	72, 73, 35	3eqtr4g 1953	. . . . . . . . . . . . . . . 16 |- (y = x -> H = D)
75	74	neeq1d 2028	. . . . . . . . . . . . . . 15 |- (y = x -> (H =/= (/) <-> D =/= (/)))
76	75	rcla4cv 2377	. . . . . . . . . . . . . 14 |- (A.y e. r H =/= (/) -> (x e. r -> D =/= (/)))
77	76	adantl 424	. . . . . . . . . . . . 13 |- (((F"r) C_ A /\ A.y e. r H =/= (/)) -> (x e. r -> D =/= (/)))
78	77	ad2antlr 441	. . . . . . . . . . . 12 |- ((((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) /\ (z e. A /\ -. z e. (F"r))) -> (x e. r -> D =/= (/)))
79	78	imp 377	. . . . . . . . . . 11 |- (((((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) /\ (z e. A /\ -. z e. (F"r))) /\ x e. r) -> D =/= (/))
80	38	wereu 3654	. . . . . . . . . . 11 |- ((R We A /\ D C_ A /\ D =/= (/)) -> E!v e. D A.u e. D -. uRv)
81	66, 69, 79, 80	syl111anc 1100	. . . . . . . . . 10 |- (((((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) /\ (z e. A /\ -. z e. (F"r))) /\ x e. r) -> E!v e. D A.u e. D -. uRv)
82		reuuni4 3813	. . . . . . . . . 10 |- (E!v e. D A.u e. D -. uRv -> [U.{v e. D | A.u e. D -. uRv} / v]A.u e. D -. uRv)
83	81, 82	syl 12	. . . . . . . . 9 |- (((((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) /\ (z e. A /\ -. z e. (F"r))) /\ x e. r) -> [U.{v e. D | A.u e. D -. uRv} / v]A.u e. D -. uRv)
84		visset 2295	. . . . . . . . . . . . . . . 16 |- z e. _V
85		ax-17 1317	. . . . . . . . . . . . . . . . 17 |- (m e. z -> A.u m e. z)
86		ax-17 1317	. . . . . . . . . . . . . . . . . 18 |- (z e. D -> A.u z e. D)
87		ax-17 1317	. . . . . . . . . . . . . . . . . . . 20 |- (m e. R -> A.u m e. R)
88		hbra1 2147	. . . . . . . . . . . . . . . . . . . . . 22 |- (A.u e. D -. uRv -> A.uA.u e. D -. uRv)
89		ax-17 1317	. . . . . . . . . . . . . . . . . . . . . 22 |- (m e. D -> A.u m e. D)
90	88, 89	hbrab 2258	. . . . . . . . . . . . . . . . . . . . 21 |- (m e. {v e. D | A.u e. D -. uRv} -> A.u m e. {v e. D | A.u e. D -. uRv})
91	90	hbuni 3183	. . . . . . . . . . . . . . . . . . . 20 |- (m e. U.{v e. D | A.u e. D -. uRv} -> A.u m e. U.{v e. D | A.u e. D -. uRv})
92	85, 87, 91	hbbr 3381	. . . . . . . . . . . . . . . . . . 19 |- (zRU.{v e. D | A.u e. D -. uRv} -> A.u zRU.{v e. D | A.u e. D -. uRv})
93	92	hbn 1351	. . . . . . . . . . . . . . . . . 18 |- (-. zRU.{v e. D | A.u e. D -. uRv} -> A.u -. zRU.{v e. D | A.u e. D -. uRv})
94	86, 93	hbim 1354	. . . . . . . . . . . . . . . . 17 |- ((z e. D -> -. zRU.{v e. D | A.u e. D -. uRv}) -> A.u(z e. D -> -. zRU.{v e. D | A.u e. D -. uRv}))
95		eleq1 1957	. . . . . . . . . . . . . . . . . 18 |- (u = z -> (u e. D <-> z e. D))
96		breq1 3341	. . . . . . . . . . . . . . . . . . 19 |- (u = z -> (uRU.{v e. D | A.u e. D -. uRv} <-> zRU.{v e. D | A.u e. D -. uRv}))
97	96	notbid 673	. . . . . . . . . . . . . . . . . 18 |- (u = z -> (-. uRU.{v e. D | A.u e. D -. uRv} <-> -. zRU.{v e. D | A.u e. D -. uRv}))
98	95, 97	imbi12d 688	. . . . . . . . . . . . . . . . 17 |- (u = z -> ((u e. D -> -. uRU.{v e. D | A.u e. D -. uRv}) <-> (z e. D -> -. zRU.{v e. D | A.u e. D -. uRv})))
99	85, 94, 98	cla4gf 2361	. . . . . . . . . . . . . . . 16 |- (z e. _V -> (A.u(u e. D -> -. uRU.{v e. D | A.u e. D -. uRv}) -> (z e. D -> -. zRU.{v e. D | A.u e. D -. uRv})))
100	84, 99	ax-mp 7	. . . . . . . . . . . . . . 15 |- (A.u(u e. D -> -. uRU.{v e. D | A.u e. D -. uRv}) -> (z e. D -> -. zRU.{v e. D | A.u e. D -. uRv}))
101		simprl 450	. . . . . . . . . . . . . . . . . 18 |- ((((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) /\ (z e. A /\ -. z e. (F"r))) -> z e. A)
102	101	ad2antrr 440	. . . . . . . . . . . . . . . . 17 |- ((((((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) /\ (z e. A /\ -. z e. (F"r))) /\ x e. r) /\ A.n(nRU.{v e. D | A.u e. D -. uRv} -> (n e. (F"r) -> nRz))) -> z e. A)
103		simplll 452	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) /\ (z e. A /\ -. z e. (F"r))) -> R We A)
104	103	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((((((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) /\ (z e. A /\ -. z e. (F"r))) /\ x e. r) /\ j e. (F"x)) -> R We A)
105	68	a1i 8	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((((((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) /\ (z e. A /\ -. z e. (F"r))) /\ x e. r) /\ j e. (F"x)) -> D C_ A)
106	76	imp 377	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((A.y e. r H =/= (/) /\ x e. r) -> D =/= (/))
107	106	adantll 428	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((((F"r) C_ A /\ A.y e. r H =/= (/)) /\ x e. r) -> D =/= (/))
108	107	adantll 428	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) /\ x e. r) -> D =/= (/))
109	108	adantlr 429	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) /\ (z e. A /\ -. z e. (F"r))) /\ x e. r) -> D =/= (/))
110	109	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((((((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) /\ (z e. A /\ -. z e. (F"r))) /\ x e. r) /\ j e. (F"x)) -> D =/= (/))
111	38	wereucl 3655	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((R We A /\ D C_ A /\ D =/= (/)) -> U.{v e. D | A.u e. D -. uRv} e. D)
112	104, 105, 110, 111	syl111anc 1100	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((((((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) /\ (z e. A /\ -. z e. (F"r))) /\ x e. r) /\ j e. (F"x)) -> U.{v e. D | A.u e. D -. uRv} e. D)
113		ra4 2155	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (A.j e. (F"x)jRU.{v e. D | A.u e. D -. uRv} -> (j e. (F"x) -> jRU.{v e. D | A.u e. D -. uRv}))
114	113	com12 14	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (j e. (F"x) -> (A.j e. (F"x)jRU.{v e. D | A.u e. D -. uRv} -> jRU.{v e. D | A.u e. D -. uRv}))
115	114	adantl 424	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((((((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) /\ (z e. A /\ -. z e. (F"r))) /\ x e. r) /\ j e. (F"x)) -> (A.j e. (F"x)jRU.{v e. D | A.u e. D -. uRv} -> jRU.{v e. D | A.u e. D -. uRv}))
116	115	adantld 426	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((((((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) /\ (z e. A /\ -. z e. (F"r))) /\ x e. r) /\ j e. (F"x)) -> ((U.{v e. D | A.u e. D -. uRv} e. A /\ A.j e. (F"x)jRU.{v e. D | A.u e. D -. uRv}) -> jRU.{v e. D | A.u e. D -. uRv}))
117	35	eleq2i 1961	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (U.{v e. D | A.u e. D -. uRv} e. D <-> U.{v e. D | A.u e. D -. uRv} e. {w e. A | A.j e. (F"x)jRw})
118		breq2 3342	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (w = U.{v e. D | A.u e. D -. uRv} -> (jRw <-> jRU.{v e. D | A.u e. D -. uRv}))
119	118	ralbidv 2123	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (w = U.{v e. D | A.u e. D -. uRv} -> (A.j e. (F"x)jRw <-> A.j e. (F"x)jRU.{v e. D | A.u e. D -. uRv}))
120	119	elrab 2414	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (U.{v e. D | A.u e. D -. uRv} e. {w e. A | A.j e. (F"x)jRw} <-> (U.{v e. D | A.u e. D -. uRv} e. A /\ A.j e. (F"x)jRU.{v e. D | A.u e. D -. uRv}))
121	117, 120	bitri 190	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (U.{v e. D | A.u e. D -. uRv} e. D <-> (U.{v e. D | A.u e. D -. uRv} e. A /\ A.j e. (F"x)jRU.{v e. D | A.u e. D -. uRv}))
122	116, 121	syl5ib 223	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((((((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) /\ (z e. A /\ -. z e. (F"r))) /\ x e. r) /\ j e. (F"x)) -> (U.{v e. D | A.u e. D -. uRv} e. D -> jRU.{v e. D | A.u e. D -. uRv}))
123	112, 122	mpd 29	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((((((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) /\ (z e. A /\ -. z e. (F"r))) /\ x e. r) /\ j e. (F"x)) -> jRU.{v e. D | A.u e. D -. uRv})
124		imass2 4299	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (x C_ r -> (F"x) C_ (F"r))
125	124	sseld 2619	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (x C_ r -> (j e. (F"x) -> j e. (F"r)))
126	125	imp 377	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((x C_ r /\ j e. (F"x)) -> j e. (F"r))
127		onelss 3705	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (r e. On -> (x e. r -> x C_ r))
128	127	imp 377	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((r e. On /\ x e. r) -> x C_ r)
129		simpllr 453	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) /\ (z e. A /\ -. z e. (F"r))) -> r e. On)
130	128, 129	sylan 497	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) /\ (z e. A /\ -. z e. (F"r))) /\ x e. r) -> x C_ r)
131	126, 130	sylan 497	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((((((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) /\ (z e. A /\ -. z e. (F"r))) /\ x e. r) /\ j e. (F"x)) -> j e. (F"r))
132		idd 75	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((((((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) /\ (z e. A /\ -. z e. (F"r))) /\ x e. r) /\ j e. (F"x)) -> ((j e. (F"r) -> jRz) -> (j e. (F"r) -> jRz)))
133	131, 132	mpid 58	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((((((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) /\ (z e. A /\ -. z e. (F"r))) /\ x e. r) /\ j e. (F"x)) -> ((j e. (F"r) -> jRz) -> jRz))
134	133	imim2d 28	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((((((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) /\ (z e. A /\ -. z e. (F"r))) /\ x e. r) /\ j e. (F"x)) -> ((jRU.{v e. D | A.u e. D -. uRv} -> (j e. (F"r) -> jRz)) -> (jRU.{v e. D | A.u e. D -. uRv} -> jRz)))
135	123, 134	mpid 58	. . . . . . . . . . . . . . . . . . . . . 22 |- ((((((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) /\ (z e. A /\ -. z e. (F"r))) /\ x e. r) /\ j e. (F"x)) -> ((jRU.{v e. D | A.u e. D -. uRv} -> (j e. (F"r) -> jRz)) -> jRz))
136	135	ex 402	. . . . . . . . . . . . . . . . . . . . 21 |- (((((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) /\ (z e. A /\ -. z e. (F"r))) /\ x e. r) -> (j e. (F"x) -> ((jRU.{v e. D | A.u e. D -. uRv} -> (j e. (F"r) -> jRz)) -> jRz)))
137	136	com23 36	. . . . . . . . . . . . . . . . . . . 20 |- (((((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) /\ (z e. A /\ -. z e. (F"r))) /\ x e. r) -> ((jRU.{v e. D | A.u e. D -. uRv} -> (j e. (F"r) -> jRz)) -> (j e. (F"x) -> jRz)))
138	137	imp 377	. . . . . . . . . . . . . . . . . . 19 |- ((((((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) /\ (z e. A /\ -. z e. (F"r))) /\ x e. r) /\ (jRU.{v e. D | A.u e. D -. uRv} -> (j e. (F"r) -> jRz))) -> (j e. (F"x) -> jRz))
139		breq1 3341	. . . . . . . . . . . . . . . . . . . . 21 |- (n = j -> (nRU.{v e. D | A.u e. D -. uRv} <-> jRU.{v e. D | A.u e. D -. uRv}))
140		eleq1 1957	. . . . . . . . . . . . . . . . . . . . . 22 |- (n = j -> (n e. (F"r) <-> j e. (F"r)))
141		breq1 3341	. . . . . . . . . . . . . . . . . . . . . 22 |- (n = j -> (nRz <-> jRz))
142	140, 141	imbi12d 688	. . . . . . . . . . . . . . . . . . . . 21 |- (n = j -> ((n e. (F"r) -> nRz) <-> (j e. (F"r) -> jRz)))
143	139, 142	imbi12d 688	. . . . . . . . . . . . . . . . . . . 20 |- (n = j -> ((nRU.{v e. D | A.u e. D -. uRv} -> (n e. (F"r) -> nRz)) <-> (jRU.{v e. D | A.u e. D -. uRv} -> (j e. (F"r) -> jRz))))
144	143	a4v 1649	. . . . . . . . . . . . . . . . . . 19 |- (A.n(nRU.{v e. D | A.u e. D -. uRv} -> (n e. (F"r) -> nRz)) -> (jRU.{v e. D | A.u e. D -. uRv} -> (j e. (F"r) -> jRz)))
145	138, 144	sylan2 500	. . . . . . . . . . . . . . . . . 18 |- ((((((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) /\ (z e. A /\ -. z e. (F"r))) /\ x e. r) /\ A.n(nRU.{v e. D | A.u e. D -. uRv} -> (n e. (F"r) -> nRz))) -> (j e. (F"x) -> jRz))
146	145	r19.21aiv 2175	. . . . . . . . . . . . . . . . 17 |- ((((((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) /\ (z e. A /\ -. z e. (F"r))) /\ x e. r) /\ A.n(nRU.{v e. D | A.u e. D -. uRv} -> (n e. (F"r) -> nRz))) -> A.j e. (F"x)jRz)
147	102, 146	jca 310	. . . . . . . . . . . . . . . 16 |- ((((((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) /\ (z e. A /\ -. z e. (F"r))) /\ x e. r) /\ A.n(nRU.{v e. D | A.u e. D -. uRv} -> (n e. (F"r) -> nRz))) -> (z e. A /\ A.j e. (F"x)jRz))
148	35	eleq2i 1961	. . . . . . . . . . . . . . . . 17 |- (z e. D <-> z e. {w e. A | A.j e. (F"x)jRw})
149		breq2 3342	. . . . . . . . . . . . . . . . . . 19 |- (w = z -> (jRw <-> jRz))
150	149	ralbidv 2123	. . . . . . . . . . . . . . . . . 18 |- (w = z -> (A.j e. (F"x)jRw <-> A.j e. (F"x)jRz))
151	150	elrab 2414	. . . . . . . . . . . . . . . . 17 |- (z e. {w e. A | A.j e. (F"x)jRw} <-> (z e. A /\ A.j e. (F"x)jRz))
152	148, 151	bitr2i 191	. . . . . . . . . . . . . . . 16 |- ((z e. A /\ A.j e. (F"x)jRz) <-> z e. D)
153	147, 152	sylib 215	. . . . . . . . . . . . . . 15 |- ((((((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) /\ (z e. A /\ -. z e. (F"r))) /\ x e. r) /\ A.n(nRU.{v e. D | A.u e. D -. uRv} -> (n e. (F"r) -> nRz))) -> z e. D)
154	100, 153	syl5com 63	. . . . . . . . . . . . . 14 |- ((((((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) /\ (z e. A /\ -. z e. (F"r))) /\ x e. r) /\ A.n(nRU.{v e. D | A.u e. D -. uRv} -> (n e. (F"r) -> nRz))) -> (A.u(u e. D -> -. uRU.{v e. D | A.u e. D -. uRv}) -> -. zRU.{v e. D | A.u e. D -. uRv}))
155		ioran 331	. . . . . . . . . . . . . . . . 17 |- (-. (U.{v e. D | A.u e. D -. uRv} = z \/ zRU.{v e. D | A.u e. D -. uRv}) <-> (-. U.{v e. D | A.u e. D -. uRv} = z /\ -. zRU.{v e. D | A.u e. D -. uRv}))
156		simplrr 455	. . . . . . . . . . . . . . . . . . 19 |- (((((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) /\ (z e. A /\ -. z e. (F"r))) /\ x e. r) -> -. z e. (F"r))
157	156	ad2antrr 440	. . . . . . . . . . . . . . . . . 18 |- (((((((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) /\ (z e. A /\ -. z e. (F"r))) /\ x e. r) /\ A.n(nRU.{v e. D | A.u e. D -. uRv} -> (n e. (F"r) -> nRz))) /\ -. zRU.{v e. D | A.u e. D -. uRv}) -> -. z e. (F"r))
158		eleq1 1957	. . . . . . . . . . . . . . . . . . . 20 |- (U.{v e. D | A.u e. D -. uRv} = z -> (U.{v e. D | A.u e. D -. uRv} e. (F"r) <-> z e. (F"r)))
159	28, 57	syl6req 1945	. . . . . . . . . . . . . . . . . . . . 21 |- (((((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) /\ (z e. A /\ -. z e. (F"r))) /\ x e. r) -> U.{v e. D | A.u e. D -. uRv} = (F` x))
160	22, 23	tfr1 5132	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- F Fn On
161		fndm 4512	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (F Fn On -> dom F = On)
162	160, 161	ax-mp 7	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- dom F = On
163	21, 162	syl6eleqr 1982	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((r e. On /\ x e. r) -> x e. dom F)
164	163	adantll 428	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((R We A /\ r e. On) /\ x e. r) -> x e. dom F)
165	164	adantlr 429	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) /\ x e. r) -> x e. dom F)
166	165	adantlr 429	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) /\ (z e. A /\ -. z e. (F"r))) /\ x e. r) -> x e. dom F)
167	166, 31	jctil 316	. . . . . . . . . . . . . . . . . . . . . 22 |- (((((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) /\ (z e. A /\ -. z e. (F"r))) /\ x e. r) -> (Fun F /\ x e. dom F))
168		simpr 350	. . . . . . . . . . . . . . . . . . . . . 22 |- (((((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) /\ (z e. A /\ -. z e. (F"r))) /\ x e. r) -> x e. r)
169		funfvima 4828	. . . . . . . . . . . . . . . . . . . . . 22 |- ((Fun F /\ x e. dom F) -> (x e. r -> (F` x) e. (F"r)))
170	167, 168, 169	sylc 83	. . . . . . . . . . . . . . . . . . . . 21 |- (((((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) /\ (z e. A /\ -. z e. (F"r))) /\ x e. r) -> (F` x) e. (F"r))
171	159, 170	eqeltrd 1971	. . . . . . . . . . . . . . . . . . . 20 |- (((((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) /\ (z e. A /\ -. z e. (F"r))) /\ x e. r) -> U.{v e. D | A.u e. D -. uRv} e. (F"r))
172	158, 171	syl5cbi 226	. . . . . . . . . . . . . . . . . . 19 |- (((((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) /\ (z e. A /\ -. z e. (F"r))) /\ x e. r) -> (U.{v e. D | A.u e. D -. uRv} = z -> z e. (F"r)))
173	172	ad2antrr 440	. . . . . . . . . . . . . . . . . 18 |- (((((((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) /\ (z e. A /\ -. z e. (F"r))) /\ x e. r) /\ A.n(nRU.{v e. D | A.u e. D -. uRv} -> (n e. (F"r) -> nRz))) /\ -. zRU.{v e. D | A.u e. D -. uRv}) -> (U.{v e. D | A.u e. D -. uRv} = z -> z e. (F"r)))
174	157, 173	mtod 123	. . . . . . . . . . . . . . . . 17 |- (((((((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) /\ (z e. A /\ -. z e. (F"r))) /\ x e. r) /\ A.n(nRU.{v e. D | A.u e. D -. uRv} -> (n e. (F"r) -> nRz))) /\ -. zRU.{v e. D | A.u e. D -. uRv}) -> -. U.{v e. D | A.u e. D -. uRv} = z)
175		simpr 350	. . . . . . . . . . . . . . . . 17 |- (((((((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) /\ (z e. A /\ -. z e. (F"r))) /\ x e. r) /\ A.n(nRU.{v e. D | A.u e. D -. uRv} -> (n e. (F"r) -> nRz))) /\ -. zRU.{v e. D | A.u e. D -. uRv}) -> -. zRU.{v e. D | A.u e. D -. uRv})
176	155, 174, 175	sylanbrc 527	. . . . . . . . . . . . . . . 16 |- (((((((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) /\ (z e. A /\ -. z e. (F"r))) /\ x e. r) /\ A.n(nRU.{v e. D | A.u e. D -. uRv} -> (n e. (F"r) -> nRz))) /\ -. zRU.{v e. D | A.u e. D -. uRv}) -> -. (U.{v e. D | A.u e. D -. uRv} = z \/ zRU.{v e. D | A.u e. D -. uRv}))
177		weso 3649	. . . . . . . . . . . . . . . . . . . 20 |- (R We A -> R Or A)
178	177	ad2antrr 440	. . . . . . . . . . . . . . . . . . 19 |- (((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) -> R Or A)
179	178	ad2antrr 440	. . . . . . . . . . . . . . . . . 18 |- (((((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) /\ (z e. A /\ -. z e. (F"r))) /\ x e. r) -> R Or A)
180	179	ad2antrr 440	. . . . . . . . . . . . . . . . 17 |- (((((((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) /\ (z e. A /\ -. z e. (F"r))) /\ x e. r) /\ A.n(nRU.{v e. D | A.u e. D -. uRv} -> (n e. (F"r) -> nRz))) /\ -. zRU.{v e. D | A.u e. D -. uRv}) -> R Or A)
181	68	a1i 8	. . . . . . . . . . . . . . . . . 18 |- (((((((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) /\ (z e. A /\ -. z e. (F"r))) /\ x e. r) /\ A.n(nRU.{v e. D | A.u e. D -. uRv} -> (n e. (F"r) -> nRz))) /\ -. zRU.{v e. D | A.u e. D -. uRv}) -> D C_ A)
182	66	ad2antrr 440	. . . . . . . . . . . . . . . . . . 19 |- (((((((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) /\ (z e. A /\ -. z e. (F"r))) /\ x e. r) /\ A.n(nRU.{v e. D | A.u e. D -. uRv} -> (n e. (F"r) -> nRz))) /\ -. zRU.{v e. D | A.u e. D -. uRv}) -> R We A)
183	79	ad2antrr 440	. . . . . . . . . . . . . . . . . . 19 |- (((((((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) /\ (z e. A /\ -. z e. (F"r))) /\ x e. r) /\ A.n(nRU.{v e. D | A.u e. D -. uRv} -> (n e. (F"r) -> nRz))) /\ -. zRU.{v e. D | A.u e. D -. uRv}) -> D =/= (/))
184	182, 181, 183, 111	syl111anc 1100	. . . . . . . . . . . . . . . . . 18 |- (((((((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) /\ (z e. A /\ -. z e. (F"r))) /\ x e. r) /\ A.n(nRU.{v e. D | A.u e. D -. uRv} -> (n e. (F"r) -> nRz))) /\ -. zRU.{v e. D | A.u e. D -. uRv}) -> U.{v e. D | A.u e. D -. uRv} e. D)
185	181, 184	sseldd 2620	. . . . . . . . . . . . . . . . 17 |- (((((((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) /\ (z e. A /\ -. z e. (F"r))) /\ x e. r) /\ A.n(nRU.{v e. D | A.u e. D -. uRv} -> (n e. (F"r) -> nRz))) /\ -. zRU.{v e. D | A.u e. D -. uRv}) -> U.{v e. D | A.u e. D -. uRv} e. A)
186		simplrl 454	. . . . . . . . . . . . . . . . . 18 |- (((((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) /\ (z e. A /\ -. z e. (F"r))) /\ x e. r) -> z e. A)
187	186	ad2antrr 440	. . . . . . . . . . . . . . . . 17 |- (((((((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) /\ (z e. A /\ -. z e. (F"r))) /\ x e. r) /\ A.n(nRU.{v e. D | A.u e. D -. uRv} -> (n e. (F"r) -> nRz))) /\ -. zRU.{v e. D | A.u e. D -. uRv}) -> z e. A)
188		sotric 3615	. . . . . . . . . . . . . . . . 17 |- ((R Or A /\ (U.{v e. D | A.u e. D -. uRv} e. A /\ z e. A)) -> (U.{v e. D | A.u e. D -. uRv}Rz <-> -. (U.{v e. D | A.u e. D -. uRv} = z \/ zRU.{v e. D | A.u e. D -. uRv})))
189	180, 185, 187, 188	syl12anc 1098	. . . . . . . . . . . . . . . 16 |- (((((((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) /\ (z e. A /\ -. z e. (F"r))) /\ x e. r) /\ A.n(nRU.{v e. D | A.u e. D -. uRv} -> (n e. (F"r) -> nRz))) /\ -. zRU.{v e. D | A.u e. D -. uRv}) -> (U.{v e. D | A.u e. D -. uRv}Rz <-> -. (U.{v e. D | A.u e. D -. uRv} = z \/ zRU.{v e. D | A.u e. D -. uRv})))
190	176, 189	mpbird 213	. . . . . . . . . . . . . . 15 |- (((((((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) /\ (z e. A /\ -. z e. (F"r))) /\ x e. r) /\ A.n(nRU.{v e. D | A.u e. D -. uRv} -> (n e. (F"r) -> nRz))) /\ -. zRU.{v e. D | A.u e. D -. uRv}) -> U.{v e. D | A.u e. D -. uRv}Rz)
191	190	ex 402	. . . . . . . . . . . . . 14 |- ((((((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) /\ (z e. A /\ -. z e. (F"r))) /\ x e. r) /\ A.n(nRU.{v e. D | A.u e. D -. uRv} -> (n e. (F"r) -> nRz))) -> (-. zRU.{v e. D | A.u e. D -. uRv} -> U.{v e. D | A.u e. D -. uRv}Rz))
192	154, 191	syld 30	. . . . . . . . . . . . 13 |- ((((((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) /\ (z e. A /\ -. z e. (F"r))) /\ x e. r) /\ A.n(nRU.{v e. D | A.u e. D -. uRv} -> (n e. (F"r) -> nRz))) -> (A.u(u e. D -> -. uRU.{v e. D | A.u e. D -. uRv}) -> U.{v e. D | A.u e. D -. uRv}Rz))
193		df-ral 2109	. . . . . . . . . . . . 13 |- (A.u e. D -. uRU.{v e. D | A.u e. D -. uRv} <-> A.u(u e. D -> -. uRU.{v e. D | A.u e. D -. uRv}))
194	192, 193	syl5ib 223	. . . . . . . . . . . 12 |- ((((((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) /\ (z e. A /\ -. z e. (F"r))) /\ x e. r) /\ A.n(nRU.{v e. D | A.u e. D -. uRv} -> (n e. (F"r) -> nRz))) -> (A.u e. D -. uRU.{v e. D | A.u e. D -. uRv} -> U.{v e. D | A.u e. D -. uRv}Rz))
195	194	ex 402	. . . . . . . . . . 11 |- (((((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) /\ (z e. A /\ -. z e. (F"r))) /\ x e. r) -> (A.n(nRU.{v e. D | A.u e. D -. uRv} -> (n e. (F"r) -> nRz)) -> (A.u e. D -. uRU.{v e. D | A.u e. D -. uRv} -> U.{v e. D | A.u e. D -. uRv}Rz)))
196	195	com23 36	. . . . . . . . . 10 |- (((((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) /\ (z e. A /\ -. z e. (F"r))) /\ x e. r) -> (A.u e. D -. uRU.{v e. D | A.u e. D -. uRv} -> (A.n(nRU.{v e. D | A.u e. D -. uRv} -> (n e. (F"r) -> nRz)) -> U.{v e. D | A.u e. D -. uRv}Rz)))
197		ax-17 1317	. . . . . . . . . . . . 13 |- (A.u e. D -. uRv -> A.wA.u e. D -. uRv)
198		ax-17 1317	. . . . . . . . . . . . 13 |- (A.u e. D -. uRw -> A.vA.u e. D -. uRw)
199		breq2 3342	. . . . . . . . . . . . . . 15 |- (v = w -> (uRv <-> uRw))
200	199	notbid 673	. . . . . . . . . . . . . 14 |- (v = w -> (-. uRv <-> -. uRw))
201	200	ralbidv 2123	. . . . . . . . . . . . 13 |- (v = w -> (A.u e. D -. uRv <-> A.u e. D -. uRw))
202	197, 198, 201	cbvsbc 2479	. . . . . . . . . . . 12 |- (U.{v e. D | A.u e. D -. uRv} e. _V -> ([U.{v e. D | A.u e. D -. uRv} / v]A.u e. D -. uRv <-> [U.{v e. D | A.u e. D -. uRv} / w]A.u e. D -. uRw))
203	40, 202	ax-mp 7	. . . . . . . . . . 11 |- ([U.{v e. D | A.u e. D -. uRv} / v]A.u e. D -. uRv <-> [U.{v e. D | A.u e. D -. uRv} / w]A.u e. D -. uRw)
204		ax-17 1317	. . . . . . . . . . . . . 14 |- (m e. w -> A.u m e. w)
205	204, 91	hbeq 1995	. . . . . . . . . . . . 13 |- (w = U.{v e. D | A.u e. D -. uRv} -> A.u w = U.{v e. D | A.u e. D -. uRv})
206		breq2 3342	. . . . . . . . . . . . . 14 |- (w = U.{v e. D | A.u e. D -. uRv} -> (uRw <-> uRU.{v e. D | A.u e. D -. uRv}))
207	206	notbid 673	. . . . . . . . . . . . 13 |- (w = U.{v e. D | A.u e. D -. uRv} -> (-. uRw <-> -. uRU.{v e. D | A.u e. D -. uRv}))
208	205, 207	ralbid 2121	. . . . . . . . . . . 12 |- (w = U.{v e. D | A.u e. D -. uRv} -> (A.u e. D -. uRw <-> A.u e. D -. uRU.{v e. D | A.u e. D -. uRv}))
209	40, 208	sbcie 2485	. . . . . . . . . . 11 |- ([U.{v e. D | A.u e. D -. uRv} / w]A.u e. D -. uRw <-> A.u e. D -. uRU.{v e. D | A.u e. D -. uRv})
210	203, 209	bitri 190	. . . . . . . . . 10 |- ([U.{v e. D | A.u e. D -. uRv} / v]A.u e. D -. uRv <-> A.u e. D -. uRU.{v e. D | A.u e. D -. uRv})
211	196, 210	syl5ib 223	. . . . . . . . 9 |- (((((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) /\ (z e. A /\ -. z e. (F"r))) /\ x e. r) -> ([U.{v e. D | A.u e. D -. uRv} / v]A.u e. D -. uRv -> (A.n(nRU.{v e. D | A.u e. D -. uRv} -> (n e. (F"r) -> nRz)) -> U.{v e. D | A.u e. D -. uRv}Rz)))
212	83, 211	mpd 29	. . . . . . . 8 |- (((((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) /\ (z e. A /\ -. z e. (F"r))) /\ x e. r) -> (A.n(nRU.{v e. D | A.u e. D -. uRv} -> (n e. (F"r) -> nRz)) -> U.{v e. D | A.u e. D -. uRv}Rz))
213	64, 212	syl5cbi 226	. . . . . . 7 |- (((((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) /\ (z e. A /\ -. z e. (F"r))) /\ x e. r) -> (U.{v e. D | A.u e. D -. uRv} = m -> (A.n(nRm -> (n e. (F"r) -> nRz)) -> mRz)))
214	59, 213	sylbid 220	. . . . . 6 |- (((((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) /\ (z e. A /\ -. z e. (F"r))) /\ x e. r) -> ((F` x) = m -> (A.n(nRm -> (n e. (F"r) -> nRz)) -> mRz)))
215	214	ex 402	. . . . 5 |- ((((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) /\ (z e. A /\ -. z e. (F"r))) -> (x e. r -> ((F` x) = m -> (A.n(nRm -> (n e. (F"r) -> nRz)) -> mRz))))
216	215	r19.23adv 2215	. . . 4 |- ((((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) /\ (z e. A /\ -. z e. (F"r))) -> (E.x e. r (F` x) = m -> (A.n(nRm -> (n e. (F"r) -> nRz)) -> mRz)))
217		fvelima 4723	. . . . 5 |- ((Fun F /\ m e. (F"r)) -> E.x e. r (F` x) = m)
218	31, 217	mpan 759	. . . 4 |- (m e. (F"r) -> E.x e. r (F` x) = m)
219	216, 218	syl5 20	. . 3 |- ((((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) /\ (z e. A /\ -. z e. (F"r))) -> (m e. (F"r) -> (A.n(nRm -> (n e. (F"r) -> nRz)) -> mRz)))
220	219	impr 422	. 2 |- ((((R We A /\ r e. On) /\ ((F"r) C_ A /\ A.y e. r H =/= (/))) /\ ((z e. A /\ -. z e. (F"r)) /\ m e. (F"r))) -> (A.n(nRm -> (n e. (F"r) -> nRz)) -> mRz))
221	20, 220	mpg 1332	1 |- ((((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))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   \/ wo 239   /\ wa 240  A.wal 1296   = wceq 1298   e. wcel 1300  [wsbc 1534  {cab 1871   =/= wne 2017  A.wral 2105  E.wrex 2106  E!wreu 2107  {crab 2108  _Vcvv 2292   C_ wss 2593  (/)c0 2875  U.cuni 3177   class class class wbr 3338  {copab 3395   Or wor 3590   We wwe 3624  Oncon0 3657  dom cdm 3986  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-fv 4014

Copyright terms: Public domain