Theorem zorn2lem7 5956

Description: Lemma for zorn2 5958.

Hypotheses

Ref	Expression
zorn2lem.1	|- A e. _V
zorn2lem.2	|- B = {f | E.h e. On (f Fn h /\ A.t e. h (f` t) = (G` (f |` t)))}
zorn2lem.3	|- F = U.B
zorn2lem.4	|- C = {z e. A | A.g e. ran f gRz}
zorn2lem.5	|- D = {z e. A | A.g e. (F"x)gRz}
zorn2lem.6	|- G = {<.f, t>. | t = U.{v e. C | A.u e. C -. uwv}}
zorn2lem.7	|- H = {z e. A | A.g e. (F"y)gRz}

Assertion

Ref	Expression
zorn2lem7	|- ((R Po A /\ A.s((s C_ A /\ R Or s) -> E.a e. A A.r e. s (rRa \/ r = a))) -> E.a e. A A.b e. A -. aRb)

Distinct variable groups:   x,y,w,h,t,z,f,g,u,v,r,s,a,b,A   B,h,t,f   x,F,y,z,v,u,f,g,h,t,r,s,a,b   h,G,t,f   t,C   y,D,u,v,f,t,a,b   x,R,y,z,w,g,u,v,f,t,s,r,a,b   x,H,u,v,f,t,s,r,a,b

Proof of Theorem zorn2lem7

Step	Hyp	Ref	Expression
1		zorn2lem.1	. . 3 |- A e. _V
2	1	weth 5949	. 2 |- E.w w We A
3		zorn2lem.2	. . . . . . . 8 |- B = {f | E.h e. On (f Fn h /\ A.t e. h (f` t) = (G` (f |` t)))}
4		zorn2lem.3	. . . . . . . 8 |- F = U.B
5		zorn2lem.4	. . . . . . . 8 |- C = {z e. A | A.g e. ran f gRz}
6		zorn2lem.5	. . . . . . . 8 |- D = {z e. A | A.g e. (F"x)gRz}
7		zorn2lem.6	. . . . . . . 8 |- G = {<.f, t>. | t = U.{v e. C | A.u e. C -. uwv}}
8	1, 3, 4, 5, 6, 7	zorn2lem4 5953	. . . . . . 7 |- ((R Po A /\ w We A) -> E.x e. On D = (/))
9		imaeq2 4260	. . . . . . . . . . . . 13 |- (x = y -> (F"x) = (F"y))
10	9	raleqdv 2269	. . . . . . . . . . . 12 |- (x = y -> (A.g e. (F"x)gRz <-> A.g e. (F"y)gRz))
11	10	rabbidv 2287	. . . . . . . . . . 11 |- (x = y -> {z e. A | A.g e. (F"x)gRz} = {z e. A | A.g e. (F"y)gRz})
12		zorn2lem.7	. . . . . . . . . . 11 |- H = {z e. A | A.g e. (F"y)gRz}
13	11, 6, 12	3eqtr4g 1953	. . . . . . . . . 10 |- (x = y -> D = H)
14	13	eqeq1d 1892	. . . . . . . . 9 |- (x = y -> (D = (/) <-> H = (/)))
15	14	onminex 3888	. . . . . . . 8 |- (E.x e. On D = (/) -> E.x e. On (D = (/) /\ A.y e. x -. H = (/)))
16		df-ne 2019	. . . . . . . . . . 11 |- (H =/= (/) <-> -. H = (/))
17	16	ralbii 2127	. . . . . . . . . 10 |- (A.y e. x H =/= (/) <-> A.y e. x -. H = (/))
18	17	anbi2i 538	. . . . . . . . 9 |- ((D = (/) /\ A.y e. x H =/= (/)) <-> (D = (/) /\ A.y e. x -. H = (/)))
19	18	rexbii 2128	. . . . . . . 8 |- (E.x e. On (D = (/) /\ A.y e. x H =/= (/)) <-> E.x e. On (D = (/) /\ A.y e. x -. H = (/)))
20	15, 19	sylibr 217	. . . . . . 7 |- (E.x e. On D = (/) -> E.x e. On (D = (/) /\ A.y e. x H =/= (/)))
21	1, 3, 4, 5, 6, 7, 12	zorn2lem5 5954	. . . . . . . . . . . . . . . . . . 19 |- (((w We A /\ x e. On) /\ A.y e. x H =/= (/)) -> (F"x) C_ A)
22	21	a1i 8	. . . . . . . . . . . . . . . . . 18 |- (R Po A -> (((w We A /\ x e. On) /\ A.y e. x H =/= (/)) -> (F"x) C_ A))
23	1, 3, 4, 5, 6, 7, 12	zorn2lem6 5955	. . . . . . . . . . . . . . . . . 18 |- (R Po A -> (((w We A /\ x e. On) /\ A.y e. x H =/= (/)) -> R Or (F"x)))
24	22, 23	jcad 661	. . . . . . . . . . . . . . . . 17 |- (R Po A -> (((w We A /\ x e. On) /\ A.y e. x H =/= (/)) -> ((F"x) C_ A /\ R Or (F"x))))
25	3, 4	tfrlem7 5125	. . . . . . . . . . . . . . . . . . 19 |- Fun F
26		visset 2295	. . . . . . . . . . . . . . . . . . . 20 |- x e. _V
27	26	funimaex 4496	. . . . . . . . . . . . . . . . . . 19 |- (Fun F -> (F"x) e. _V)
28	25, 27	ax-mp 7	. . . . . . . . . . . . . . . . . 18 |- (F"x) e. _V
29		sseq1 2637	. . . . . . . . . . . . . . . . . . . 20 |- (s = (F"x) -> (s C_ A <-> (F"x) C_ A))
30		soeq2 3609	. . . . . . . . . . . . . . . . . . . 20 |- (s = (F"x) -> (R Or s <-> R Or (F"x)))
31	29, 30	anbi12d 690	. . . . . . . . . . . . . . . . . . 19 |- (s = (F"x) -> ((s C_ A /\ R Or s) <-> ((F"x) C_ A /\ R Or (F"x))))
32		raleq 2266	. . . . . . . . . . . . . . . . . . . 20 |- (s = (F"x) -> (A.r e. s (rRa \/ r = a) <-> A.r e. (F"x)(rRa \/ r = a)))
33	32	rexbidv 2124	. . . . . . . . . . . . . . . . . . 19 |- (s = (F"x) -> (E.a e. A A.r e. s (rRa \/ r = a) <-> E.a e. A A.r e. (F"x)(rRa \/ r = a)))
34	31, 33	imbi12d 688	. . . . . . . . . . . . . . . . . 18 |- (s = (F"x) -> (((s C_ A /\ R Or s) -> E.a e. A A.r e. s (rRa \/ r = a)) <-> (((F"x) C_ A /\ R Or (F"x)) -> E.a e. A A.r e. (F"x)(rRa \/ r = a))))
35	28, 34	cla4v 2370	. . . . . . . . . . . . . . . . 17 |- (A.s((s C_ A /\ R Or s) -> E.a e. A A.r e. s (rRa \/ r = a)) -> (((F"x) C_ A /\ R Or (F"x)) -> E.a e. A A.r e. (F"x)(rRa \/ r = a)))
36	24, 35	sylan9 517	. . . . . . . . . . . . . . . 16 |- ((R Po A /\ A.s((s C_ A /\ R Or s) -> E.a e. A A.r e. s (rRa \/ r = a))) -> (((w We A /\ x e. On) /\ A.y e. x H =/= (/)) -> E.a e. A A.r e. (F"x)(rRa \/ r = a)))
37	36	adantld 426	. . . . . . . . . . . . . . 15 |- ((R Po A /\ A.s((s C_ A /\ R Or s) -> E.a e. A A.r e. s (rRa \/ r = a))) -> ((D = (/) /\ ((w We A /\ x e. On) /\ A.y e. x H =/= (/))) -> E.a e. A A.r e. (F"x)(rRa \/ r = a)))
38	37	imp 377	. . . . . . . . . . . . . 14 |- (((R Po A /\ A.s((s C_ A /\ R Or s) -> E.a e. A A.r e. s (rRa \/ r = a))) /\ (D = (/) /\ ((w We A /\ x e. On) /\ A.y e. x H =/= (/)))) -> E.a e. A A.r e. (F"x)(rRa \/ r = a))
39		noel 2879	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- -. b e. (/)
40	21	sseld 2619	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- (((w We A /\ x e. On) /\ A.y e. x H =/= (/)) -> (r e. (F"x) -> r e. A))
41		potr 3598	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- ((R Po A /\ (r e. A /\ a e. A /\ b e. A)) -> ((rRa /\ aRb) -> rRb))
42		3anass 862	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- ((r e. A /\ a e. A /\ b e. A) <-> (r e. A /\ (a e. A /\ b e. A)))
43	41, 42	sylan2br 502	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- ((R Po A /\ (r e. A /\ (a e. A /\ b e. A))) -> ((rRa /\ aRb) -> rRb))
44	43	exp3a 405	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- ((R Po A /\ (r e. A /\ (a e. A /\ b e. A))) -> (rRa -> (aRb -> rRb)))
45	44	com23 36	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ((R Po A /\ (r e. A /\ (a e. A /\ b e. A))) -> (aRb -> (rRa -> rRb)))
46	45	imp 377	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- (((R Po A /\ (r e. A /\ (a e. A /\ b e. A))) /\ aRb) -> (rRa -> rRb))
47		breq1 3341	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- (r = a -> (rRb <-> aRb))
48	47	biimprcd 173	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- (aRb -> (r = a -> rRb))
49	48	adantl 424	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- (((R Po A /\ (r e. A /\ (a e. A /\ b e. A))) /\ aRb) -> (r = a -> rRb))
50	46, 49	jaod 469	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- (((R Po A /\ (r e. A /\ (a e. A /\ b e. A))) /\ aRb) -> ((rRa \/ r = a) -> rRb))
51	50	exp42 414	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- (R Po A -> (r e. A -> ((a e. A /\ b e. A) -> (aRb -> ((rRa \/ r = a) -> rRb)))))
52	40, 51	sylan9r 519	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- ((R Po A /\ ((w We A /\ x e. On) /\ A.y e. x H =/= (/))) -> (r e. (F"x) -> ((a e. A /\ b e. A) -> (aRb -> ((rRa \/ r = a) -> rRb)))))
53	52	com24 41	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ((R Po A /\ ((w We A /\ x e. On) /\ A.y e. x H =/= (/))) -> (aRb -> ((a e. A /\ b e. A) -> (r e. (F"x) -> ((rRa \/ r = a) -> rRb)))))
54	53	com23 36	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ((R Po A /\ ((w We A /\ x e. On) /\ A.y e. x H =/= (/))) -> ((a e. A /\ b e. A) -> (aRb -> (r e. (F"x) -> ((rRa \/ r = a) -> rRb)))))
55	54	imp31 389	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ((((R Po A /\ ((w We A /\ x e. On) /\ A.y e. x H =/= (/))) /\ (a e. A /\ b e. A)) /\ aRb) -> (r e. (F"x) -> ((rRa \/ r = a) -> rRb)))
56	55	a2d 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ((((R Po A /\ ((w We A /\ x e. On) /\ A.y e. x H =/= (/))) /\ (a e. A /\ b e. A)) /\ aRb) -> ((r e. (F"x) -> (rRa \/ r = a)) -> (r e. (F"x) -> rRb)))
57	56	alimdv 1668	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ((((R Po A /\ ((w We A /\ x e. On) /\ A.y e. x H =/= (/))) /\ (a e. A /\ b e. A)) /\ aRb) -> (A.r(r e. (F"x) -> (rRa \/ r = a)) -> A.r(r e. (F"x) -> rRb)))
58		df-ral 2109	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (A.r e. (F"x)(rRa \/ r = a) <-> A.r(r e. (F"x) -> (rRa \/ r = a)))
59		df-ral 2109	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (A.r e. (F"x)rRb <-> A.r(r e. (F"x) -> rRb))
60	57, 58, 59	3imtr4g 612	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ((((R Po A /\ ((w We A /\ x e. On) /\ A.y e. x H =/= (/))) /\ (a e. A /\ b e. A)) /\ aRb) -> (A.r e. (F"x)(rRa \/ r = a) -> A.r e. (F"x)rRb))
61	6	eqeq1i 1891	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- (D = (/) <-> {z e. A | A.g e. (F"x)gRz} = (/))
62		eleq2 1958	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ({z e. A | A.g e. (F"x)gRz} = (/) -> (b e. {z e. A | A.g e. (F"x)gRz} <-> b e. (/)))
63	61, 62	sylbi 216	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- (D = (/) -> (b e. {z e. A | A.g e. (F"x)gRz} <-> b e. (/)))
64		breq2 3342	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- (z = b -> (gRz <-> gRb))
65	64	ralbidv 2123	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- (z = b -> (A.g e. (F"x)gRz <-> A.g e. (F"x)gRb))
66	65	elrab 2414	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- (b e. {z e. A | A.g e. (F"x)gRz} <-> (b e. A /\ A.g e. (F"x)gRb))
67	63, 66	syl5bbr 593	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- (D = (/) -> ((b e. A /\ A.g e. (F"x)gRb) <-> b e. (/)))
68	67	biimpd 170	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (D = (/) -> ((b e. A /\ A.g e. (F"x)gRb) -> b e. (/)))
69	68	expdimp 406	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ((D = (/) /\ b e. A) -> (A.g e. (F"x)gRb -> b e. (/)))
70		breq1 3341	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (r = g -> (rRb <-> gRb))
71	70	cbvralv 2280	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (A.r e. (F"x)rRb <-> A.g e. (F"x)gRb)
72	69, 71	syl5ib 223	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ((D = (/) /\ b e. A) -> (A.r e. (F"x)rRb -> b e. (/)))
73	60, 72	sylan9r 519	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (((D = (/) /\ b e. A) /\ (((R Po A /\ ((w We A /\ x e. On) /\ A.y e. x H =/= (/))) /\ (a e. A /\ b e. A)) /\ aRb)) -> (A.r e. (F"x)(rRa \/ r = a) -> b e. (/)))
74	73	exp32 408	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((D = (/) /\ b e. A) -> (((R Po A /\ ((w We A /\ x e. On) /\ A.y e. x H =/= (/))) /\ (a e. A /\ b e. A)) -> (aRb -> (A.r e. (F"x)(rRa \/ r = a) -> b e. (/)))))
75	74	com34 40	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((D = (/) /\ b e. A) -> (((R Po A /\ ((w We A /\ x e. On) /\ A.y e. x H =/= (/))) /\ (a e. A /\ b e. A)) -> (A.r e. (F"x)(rRa \/ r = a) -> (aRb -> b e. (/)))))
76	75	imp31 389	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((((D = (/) /\ b e. A) /\ ((R Po A /\ ((w We A /\ x e. On) /\ A.y e. x H =/= (/))) /\ (a e. A /\ b e. A))) /\ A.r e. (F"x)(rRa \/ r = a)) -> (aRb -> b e. (/)))
77	39, 76	mtoi 122	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((((D = (/) /\ b e. A) /\ ((R Po A /\ ((w We A /\ x e. On) /\ A.y e. x H =/= (/))) /\ (a e. A /\ b e. A))) /\ A.r e. (F"x)(rRa \/ r = a)) -> -. aRb)
78	77	exp42 414	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((D = (/) /\ b e. A) -> ((R Po A /\ ((w We A /\ x e. On) /\ A.y e. x H =/= (/))) -> ((a e. A /\ b e. A) -> (A.r e. (F"x)(rRa \/ r = a) -> -. aRb))))
79	78	exp4a 409	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((D = (/) /\ b e. A) -> ((R Po A /\ ((w We A /\ x e. On) /\ A.y e. x H =/= (/))) -> (a e. A -> (b e. A -> (A.r e. (F"x)(rRa \/ r = a) -> -. aRb)))))
80	79	com34 40	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((D = (/) /\ b e. A) -> ((R Po A /\ ((w We A /\ x e. On) /\ A.y e. x H =/= (/))) -> (b e. A -> (a e. A -> (A.r e. (F"x)(rRa \/ r = a) -> -. aRb)))))
81	80	ex 402	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (D = (/) -> (b e. A -> ((R Po A /\ ((w We A /\ x e. On) /\ A.y e. x H =/= (/))) -> (b e. A -> (a e. A -> (A.r e. (F"x)(rRa \/ r = a) -> -. aRb))))))
82	81	com4r 45	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (b e. A -> (D = (/) -> (b e. A -> ((R Po A /\ ((w We A /\ x e. On) /\ A.y e. x H =/= (/))) -> (a e. A -> (A.r e. (F"x)(rRa \/ r = a) -> -. aRb))))))
83	82	pm2.43a 80	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (b e. A -> (D = (/) -> ((R Po A /\ ((w We A /\ x e. On) /\ A.y e. x H =/= (/))) -> (a e. A -> (A.r e. (F"x)(rRa \/ r = a) -> -. aRb)))))
84	83	imp3a 388	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (b e. A -> ((D = (/) /\ (R Po A /\ ((w We A /\ x e. On) /\ A.y e. x H =/= (/)))) -> (a e. A -> (A.r e. (F"x)(rRa \/ r = a) -> -. aRb))))
85	84	com4l 43	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((D = (/) /\ (R Po A /\ ((w We A /\ x e. On) /\ A.y e. x H =/= (/)))) -> (a e. A -> (A.r e. (F"x)(rRa \/ r = a) -> (b e. A -> -. aRb))))
86	85	imp3a 388	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((D = (/) /\ (R Po A /\ ((w We A /\ x e. On) /\ A.y e. x H =/= (/)))) -> ((a e. A /\ A.r e. (F"x)(rRa \/ r = a)) -> (b e. A -> -. aRb)))
87	86	19.21adv 1666	. . . . . . . . . . . . . . . . . . . . . 22 |- ((D = (/) /\ (R Po A /\ ((w We A /\ x e. On) /\ A.y e. x H =/= (/)))) -> ((a e. A /\ A.r e. (F"x)(rRa \/ r = a)) -> A.b(b e. A -> -. aRb)))
88		df-ral 2109	. . . . . . . . . . . . . . . . . . . . . 22 |- (A.b e. A -. aRb <-> A.b(b e. A -> -. aRb))
89	87, 88	syl6ibr 230	. . . . . . . . . . . . . . . . . . . . 21 |- ((D = (/) /\ (R Po A /\ ((w We A /\ x e. On) /\ A.y e. x H =/= (/)))) -> ((a e. A /\ A.r e. (F"x)(rRa \/ r = a)) -> A.b e. A -. aRb))
90	89	exp3a 405	. . . . . . . . . . . . . . . . . . . 20 |- ((D = (/) /\ (R Po A /\ ((w We A /\ x e. On) /\ A.y e. x H =/= (/)))) -> (a e. A -> (A.r e. (F"x)(rRa \/ r = a) -> A.b e. A -. aRb)))
91	90	imdistand 493	. . . . . . . . . . . . . . . . . . 19 |- ((D = (/) /\ (R Po A /\ ((w We A /\ x e. On) /\ A.y e. x H =/= (/)))) -> ((a e. A /\ A.r e. (F"x)(rRa \/ r = a)) -> (a e. A /\ A.b e. A -. aRb)))
92	91	reximdv2 2200	. . . . . . . . . . . . . . . . . 18 |- ((D = (/) /\ (R Po A /\ ((w We A /\ x e. On) /\ A.y e. x H =/= (/)))) -> (E.a e. A A.r e. (F"x)(rRa \/ r = a) -> E.a e. A A.b e. A -. aRb))
93	92	exp32 408	. . . . . . . . . . . . . . . . 17 |- (D = (/) -> (R Po A -> (((w We A /\ x e. On) /\ A.y e. x H =/= (/)) -> (E.a e. A A.r e. (F"x)(rRa \/ r = a) -> E.a e. A A.b e. A -. aRb))))
94	93	com12 14	. . . . . . . . . . . . . . . 16 |- (R Po A -> (D = (/) -> (((w We A /\ x e. On) /\ A.y e. x H =/= (/)) -> (E.a e. A A.r e. (F"x)(rRa \/ r = a) -> E.a e. A A.b e. A -. aRb))))
95	94	adantr 425	. . . . . . . . . . . . . . 15 |- ((R Po A /\ A.s((s C_ A /\ R Or s) -> E.a e. A A.r e. s (rRa \/ r = a))) -> (D = (/) -> (((w We A /\ x e. On) /\ A.y e. x H =/= (/)) -> (E.a e. A A.r e. (F"x)(rRa \/ r = a) -> E.a e. A A.b e. A -. aRb))))
96	95	imp32 390	. . . . . . . . . . . . . 14 |- (((R Po A /\ A.s((s C_ A /\ R Or s) -> E.a e. A A.r e. s (rRa \/ r = a))) /\ (D = (/) /\ ((w We A /\ x e. On) /\ A.y e. x H =/= (/)))) -> (E.a e. A A.r e. (F"x)(rRa \/ r = a) -> E.a e. A A.b e. A -. aRb))
97	38, 96	mpd 29	. . . . . . . . . . . . 13 |- (((R Po A /\ A.s((s C_ A /\ R Or s) -> E.a e. A A.r e. s (rRa \/ r = a))) /\ (D = (/) /\ ((w We A /\ x e. On) /\ A.y e. x H =/= (/)))) -> E.a e. A A.b e. A -. aRb)
98	97	exp45 417	. . . . . . . . . . . 12 |- ((R Po A /\ A.s((s C_ A /\ R Or s) -> E.a e. A A.r e. s (rRa \/ r = a))) -> (D = (/) -> ((w We A /\ x e. On) -> (A.y e. x H =/= (/) -> E.a e. A A.b e. A -. aRb))))
99	98	com23 36	. . . . . . . . . . 11 |- ((R Po A /\ A.s((s C_ A /\ R Or s) -> E.a e. A A.r e. s (rRa \/ r = a))) -> ((w We A /\ x e. On) -> (D = (/) -> (A.y e. x H =/= (/) -> E.a e. A A.b e. A -. aRb))))
100	99	expdimp 406	. . . . . . . . . 10 |- (((R Po A /\ A.s((s C_ A /\ R Or s) -> E.a e. A A.r e. s (rRa \/ r = a))) /\ w We A) -> (x e. On -> (D = (/) -> (A.y e. x H =/= (/) -> E.a e. A A.b e. A -. aRb))))
101	100	imp4a 391	. . . . . . . . 9 |- (((R Po A /\ A.s((s C_ A /\ R Or s) -> E.a e. A A.r e. s (rRa \/ r = a))) /\ w We A) -> (x e. On -> ((D = (/) /\ A.y e. x H =/= (/)) -> E.a e. A A.b e. A -. aRb)))
102	101	com3l 38	. . . . . . . 8 |- (x e. On -> ((D = (/) /\ A.y e. x H =/= (/)) -> (((R Po A /\ A.s((s C_ A /\ R Or s) -> E.a e. A A.r e. s (rRa \/ r = a))) /\ w We A) -> E.a e. A A.b e. A -. aRb)))
103	102	r19.23aiv 2211	. . . . . . 7 |- (E.x e. On (D = (/) /\ A.y e. x H =/= (/)) -> (((R Po A /\ A.s((s C_ A /\ R Or s) -> E.a e. A A.r e. s (rRa \/ r = a))) /\ w We A) -> E.a e. A A.b e. A -. aRb))
104	8, 20, 103	3syl 24	. . . . . 6 |- ((R Po A /\ w We A) -> (((R Po A /\ A.s((s C_ A /\ R Or s) -> E.a e. A A.r e. s (rRa \/ r = a))) /\ w We A) -> E.a e. A A.b e. A -. aRb))
105	104	adantlr 429	. . . . 5 |- (((R Po A /\ A.s((s C_ A /\ R Or s) -> E.a e. A A.r e. s (rRa \/ r = a))) /\ w We A) -> (((R Po A /\ A.s((s C_ A /\ R Or s) -> E.a e. A A.r e. s (rRa \/ r = a))) /\ w We A) -> E.a e. A A.b e. A -. aRb))
106	105	pm2.43i 78	. . . 4 |- (((R Po A /\ A.s((s C_ A /\ R Or s) -> E.a e. A A.r e. s (rRa \/ r = a))) /\ w We A) -> E.a e. A A.b e. A -. aRb)
107	106	ex 402	. . 3 |- ((R Po A /\ A.s((s C_ A /\ R Or s) -> E.a e. A A.r e. s (rRa \/ r = a))) -> (w We A -> E.a e. A A.b e. A -. aRb))
108	107	19.23adv 1584	. 2 |- ((R Po A /\ A.s((s C_ A /\ R Or s) -> E.a e. A A.r e. s (rRa \/ r = a))) -> (E.w w We A -> E.a e. A A.b e. A -. aRb))
109	2, 108	mpi 55	1 |- ((R Po A /\ A.s((s C_ A /\ R Or s) -> E.a e. A A.r e. s (rRa \/ r = a))) -> E.a e. A A.b e. A -. aRb)

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  {crab 2108  _Vcvv 2292   C_ wss 2593  (/)c0 2875  U.cuni 3177   class class class wbr 3338  {copab 3395   Po wpo 3589   Or wor 3590   We wwe 3624  Oncon0 3657  ran crn 3987   |` cres 3988  "cima 3989  Fun wfun 3992   Fn wfn 3993  ` cfv 3998

This theorem is referenced by:  zorn2 5958

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  ax-ac 5906

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