Theorem zorn2lem7 9324

Description: Lemma for zorn2 9328. (Contributed by NM, 6-Apr-1997.) (Revised by Mario Carneiro, 9-May-2015.)

Hypotheses

Ref	Expression
zorn2lem.3	|- F = recs ( ( f e. _V |-> ( iota_ v e. C A. u e. C -. u w v ) ) )
zorn2lem.4	|- C = { z e. A | A. g e. ran f g R z }
zorn2lem.5	|- D = { z e. A | A. g e. ( F " x ) g R z }
zorn2lem.7	|- H = { z e. A | A. g e. ( F " y ) g R z }

Assertion

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

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

Allowed substitution hints:   C( x, y, z, w, u, f, g, s, r, a, b)   D( x, z, w, g, s, r)   F( w)   H( y, z, w, g)

Proof of Theorem zorn2lem7

Step	Hyp	Ref	Expression
1		ween 8858	. . 3 |- ( A e. dom card <-> E. w w We A )
2		zorn2lem.3	. . . . . . . . 9 |- F = recs ( ( f e. _V |-> ( iota_ v e. C A. u e. C -. u w v ) ) )
3		zorn2lem.4	. . . . . . . . 9 |- C = { z e. A | A. g e. ran f g R z }
4		zorn2lem.5	. . . . . . . . 9 |- D = { z e. A | A. g e. ( F " x ) g R z }
5	2, 3, 4	zorn2lem4 9321	. . . . . . . 8 |- ( ( R Po A /\ w We A ) -> E. x e. On D = (/) )
6		imaeq2 5462	. . . . . . . . . . . . . 14 |- ( x = y -> ( F " x ) = ( F " y ) )
7	6	raleqdv 3144	. . . . . . . . . . . . 13 |- ( x = y -> ( A. g e. ( F " x ) g R z <-> A. g e. ( F " y ) g R z ) )
8	7	rabbidv 3189	. . . . . . . . . . . 12 |- ( x = y -> { z e. A | A. g e. ( F " x ) g R z } = { z e. A | A. g e. ( F " y ) g R z } )
9		zorn2lem.7	. . . . . . . . . . . 12 |- H = { z e. A | A. g e. ( F " y ) g R z }
10	8, 4, 9	3eqtr4g 2681	. . . . . . . . . . 11 |- ( x = y -> D = H )
11	10	eqeq1d 2624	. . . . . . . . . 10 |- ( x = y -> ( D = (/) <-> H = (/) ) )
12	11	onminex 7007	. . . . . . . . 9 |- ( E. x e. On D = (/) -> E. x e. On ( D = (/) /\ A. y e. x -. H = (/) ) )
13		df-ne 2795	. . . . . . . . . . . 12 |- ( H =/= (/) <-> -. H = (/) )
14	13	ralbii 2980	. . . . . . . . . . 11 |- ( A. y e. x H =/= (/) <-> A. y e. x -. H = (/) )
15	14	anbi2i 730	. . . . . . . . . 10 |- ( ( D = (/) /\ A. y e. x H =/= (/) ) <-> ( D = (/) /\ A. y e. x -. H = (/) ) )
16	15	rexbii 3041	. . . . . . . . 9 |- ( E. x e. On ( D = (/) /\ A. y e. x H =/= (/) ) <-> E. x e. On ( D = (/) /\ A. y e. x -. H = (/) ) )
17	12, 16	sylibr 224	. . . . . . . 8 |- ( E. x e. On D = (/) -> E. x e. On ( D = (/) /\ A. y e. x H =/= (/) ) )
18	2, 3, 4, 9	zorn2lem5 9322	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( w We A /\ x e. On ) /\ A. y e. x H =/= (/) ) -> ( F " x ) C_ A )
19	18	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( R Po A -> ( ( ( w We A /\ x e. On ) /\ A. y e. x H =/= (/) ) -> ( F " x ) C_ A ) )
20	2, 3, 4, 9	zorn2lem6 9323	. . . . . . . . . . . . . . . . . . 19 |- ( R Po A -> ( ( ( w We A /\ x e. On ) /\ A. y e. x H =/= (/) ) -> R Or ( F " x ) ) )
21	19, 20	jcad 555	. . . . . . . . . . . . . . . . . 18 |- ( R Po A -> ( ( ( w We A /\ x e. On ) /\ A. y e. x H =/= (/) ) -> ( ( F " x ) C_ A /\ R Or ( F " x ) ) ) )
22	2	tfr1 7493	. . . . . . . . . . . . . . . . . . . 20 |- F Fn On
23		fnfun 5988	. . . . . . . . . . . . . . . . . . . 20 |- ( F Fn On -> Fun F )
24		vex 3203	. . . . . . . . . . . . . . . . . . . . 21 |- x e. _V
25	24	funimaex 5976	. . . . . . . . . . . . . . . . . . . 20 |- ( Fun F -> ( F " x ) e. _V )
26	22, 23, 25	mp2b 10	. . . . . . . . . . . . . . . . . . 19 |- ( F " x ) e. _V
27		sseq1 3626	. . . . . . . . . . . . . . . . . . . . 21 |- ( s = ( F " x ) -> ( s C_ A <-> ( F " x ) C_ A ) )
28		soeq2 5055	. . . . . . . . . . . . . . . . . . . . 21 |- ( s = ( F " x ) -> ( R Or s <-> R Or ( F " x ) ) )
29	27, 28	anbi12d 747	. . . . . . . . . . . . . . . . . . . 20 |- ( s = ( F " x ) -> ( ( s C_ A /\ R Or s ) <-> ( ( F " x ) C_ A /\ R Or ( F " x ) ) ) )
30		raleq 3138	. . . . . . . . . . . . . . . . . . . . 21 |- ( s = ( F " x ) -> ( A. r e. s ( r R a \/ r = a ) <-> A. r e. ( F " x ) ( r R a \/ r = a ) ) )
31	30	rexbidv 3052	. . . . . . . . . . . . . . . . . . . 20 |- ( s = ( F " x ) -> ( E. a e. A A. r e. s ( r R a \/ r = a ) <-> E. a e. A A. r e. ( F " x ) ( r R a \/ r = a ) ) )
32	29, 31	imbi12d 334	. . . . . . . . . . . . . . . . . . 19 |- ( s = ( F " x ) -> ( ( ( s C_ A /\ R Or s ) -> E. a e. A A. r e. s ( r R a \/ r = a ) ) <-> ( ( ( F " x ) C_ A /\ R Or ( F " x ) ) -> E. a e. A A. r e. ( F " x ) ( r R a \/ r = a ) ) ) )
33	26, 32	spcv 3299	. . . . . . . . . . . . . . . . . 18 |- ( A. s ( ( s C_ A /\ R Or s ) -> E. a e. A A. r e. s ( r R a \/ r = a ) ) -> ( ( ( F " x ) C_ A /\ R Or ( F " x ) ) -> E. a e. A A. r e. ( F " x ) ( r R a \/ r = a ) ) )
34	21, 33	sylan9 689	. . . . . . . . . . . . . . . . 17 |- ( ( R Po A /\ A. s ( ( s C_ A /\ R Or s ) -> E. a e. A A. r e. s ( r R a \/ r = a ) ) ) -> ( ( ( w We A /\ x e. On ) /\ A. y e. x H =/= (/) ) -> E. a e. A A. r e. ( F " x ) ( r R a \/ r = a ) ) )
35	34	adantld 483	. . . . . . . . . . . . . . . 16 |- ( ( R Po A /\ A. s ( ( s C_ A /\ R Or s ) -> E. a e. A A. r e. s ( r R a \/ r = a ) ) ) -> ( ( D = (/) /\ ( ( w We A /\ x e. On ) /\ A. y e. x H =/= (/) ) ) -> E. a e. A A. r e. ( F " x ) ( r R a \/ r = a ) ) )
36	35	imp 445	. . . . . . . . . . . . . . 15 |- ( ( ( R Po A /\ A. s ( ( s C_ A /\ R Or s ) -> E. a e. A A. r e. s ( r R a \/ r = a ) ) ) /\ ( D = (/) /\ ( ( w We A /\ x e. On ) /\ A. y e. x H =/= (/) ) ) ) -> E. a e. A A. r e. ( F " x ) ( r R a \/ r = a ) )
37		noel 3919	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- -. b e. (/)
38	18	sseld 3602	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ( ( ( w We A /\ x e. On ) /\ A. y e. x H =/= (/) ) -> ( r e. ( F " x ) -> r e. A ) )
39		3anass 1042	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ( ( r e. A /\ a e. A /\ b e. A ) <-> ( r e. A /\ ( a e. A /\ b e. A ) ) )
40		potr 5047	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ( ( R Po A /\ ( r e. A /\ a e. A /\ b e. A ) ) -> ( ( r R a /\ a R b ) -> r R b ) )
41	39, 40	sylan2br 493	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ( ( R Po A /\ ( r e. A /\ ( a e. A /\ b e. A ) ) ) -> ( ( r R a /\ a R b ) -> r R b ) )
42	41	expcomd 454	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ( ( R Po A /\ ( r e. A /\ ( a e. A /\ b e. A ) ) ) -> ( a R b -> ( r R a -> r R b ) ) )
43	42	imp 445	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ( ( ( R Po A /\ ( r e. A /\ ( a e. A /\ b e. A ) ) ) /\ a R b ) -> ( r R a -> r R b ) )
44		breq1 4656	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ( r = a -> ( r R b <-> a R b ) )
45	44	biimprcd 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ( a R b -> ( r = a -> r R b ) )
46	45	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ( ( ( R Po A /\ ( r e. A /\ ( a e. A /\ b e. A ) ) ) /\ a R b ) -> ( r = a -> r R b ) )
47	43, 46	jaod 395	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- ( ( ( R Po A /\ ( r e. A /\ ( a e. A /\ b e. A ) ) ) /\ a R b ) -> ( ( r R a \/ r = a ) -> r R b ) )
48	47	exp42 639	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ( R Po A -> ( r e. A -> ( ( a e. A /\ b e. A ) -> ( a R b -> ( ( r R a \/ r = a ) -> r R b ) ) ) ) )
49	38, 48	sylan9r 690	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ( ( R Po A /\ ( ( w We A /\ x e. On ) /\ A. y e. x H =/= (/) ) ) -> ( r e. ( F " x ) -> ( ( a e. A /\ b e. A ) -> ( a R b -> ( ( r R a \/ r = a ) -> r R b ) ) ) ) )
50	49	com24 95	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( ( R Po A /\ ( ( w We A /\ x e. On ) /\ A. y e. x H =/= (/) ) ) -> ( a R b -> ( ( a e. A /\ b e. A ) -> ( r e. ( F " x ) -> ( ( r R a \/ r = a ) -> r R b ) ) ) ) )
51	50	com23 86	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ( R Po A /\ ( ( w We A /\ x e. On ) /\ A. y e. x H =/= (/) ) ) -> ( ( a e. A /\ b e. A ) -> ( a R b -> ( r e. ( F " x ) -> ( ( r R a \/ r = a ) -> r R b ) ) ) ) )
52	51	imp31 448	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( ( ( R Po A /\ ( ( w We A /\ x e. On ) /\ A. y e. x H =/= (/) ) ) /\ ( a e. A /\ b e. A ) ) /\ a R b ) -> ( r e. ( F " x ) -> ( ( r R a \/ r = a ) -> r R b ) ) )
53	52	a2d 29	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ( ( R Po A /\ ( ( w We A /\ x e. On ) /\ A. y e. x H =/= (/) ) ) /\ ( a e. A /\ b e. A ) ) /\ a R b ) -> ( ( r e. ( F " x ) -> ( r R a \/ r = a ) ) -> ( r e. ( F " x ) -> r R b ) ) )
54	53	ralimdv2 2961	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( ( R Po A /\ ( ( w We A /\ x e. On ) /\ A. y e. x H =/= (/) ) ) /\ ( a e. A /\ b e. A ) ) /\ a R b ) -> ( A. r e. ( F " x ) ( r R a \/ r = a ) -> A. r e. ( F " x ) r R b ) )
55		breq1 4656	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( r = g -> ( r R b <-> g R b ) )
56	55	cbvralv 3171	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( A. r e. ( F " x ) r R b <-> A. g e. ( F " x ) g R b )
57		breq2 4657	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ( z = b -> ( g R z <-> g R b ) )
58	57	ralbidv 2986	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ( z = b -> ( A. g e. ( F " x ) g R z <-> A. g e. ( F " x ) g R b ) )
59	58	elrab 3363	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( b e. { z e. A | A. g e. ( F " x ) g R z } <-> ( b e. A /\ A. g e. ( F " x ) g R b ) )
60	4	eqeq1i 2627	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ( D = (/) <-> { z e. A | A. g e. ( F " x ) g R z } = (/) )
61		eleq2 2690	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ( { z e. A | A. g e. ( F " x ) g R z } = (/) -> ( b e. { z e. A | A. g e. ( F " x ) g R z } <-> b e. (/) ) )
62	60, 61	sylbi 207	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( D = (/) -> ( b e. { z e. A | A. g e. ( F " x ) g R z } <-> b e. (/) ) )
63	59, 62	syl5bbr 274	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( D = (/) -> ( ( b e. A /\ A. g e. ( F " x ) g R b ) <-> b e. (/) ) )
64	63	biimpd 219	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( D = (/) -> ( ( b e. A /\ A. g e. ( F " x ) g R b ) -> b e. (/) ) )
65	64	expdimp 453	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( D = (/) /\ b e. A ) -> ( A. g e. ( F " x ) g R b -> b e. (/) ) )
66	56, 65	syl5bi 232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( D = (/) /\ b e. A ) -> ( A. r e. ( F " x ) r R b -> b e. (/) ) )
67	54, 66	sylan9r 690	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) /\ a R b ) ) -> ( A. r e. ( F " x ) ( r R a \/ r = a ) -> b e. (/) ) )
68	67	exp32 631	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 b -> ( A. r e. ( F " x ) ( r R a \/ r = a ) -> b e. (/) ) ) ) )
69	68	com34 91	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ( r R a \/ r = a ) -> ( a R b -> b e. (/) ) ) ) )
70	69	imp31 448	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ( r R a \/ r = a ) ) -> ( a R b -> b e. (/) ) )
71	37, 70	mtoi 190	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ( r R a \/ r = a ) ) -> -. a R b )
72	71	exp42 639	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ( r R a \/ r = a ) -> -. a R b ) ) ) )
73	72	exp4a 633	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( 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 ) ( r R a \/ r = a ) -> -. a R b ) ) ) ) )
74	73	com34 91	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ( r R a \/ r = a ) -> -. a R b ) ) ) ) )
75	74	ex 450	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( 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 ) ( r R a \/ r = a ) -> -. a R b ) ) ) ) ) )
76	75	com4r 94	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( 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 ) ( r R a \/ r = a ) -> -. a R b ) ) ) ) ) )
77	76	pm2.43a 54	. . . . . . . . . . . . . . . . . . . . . . . . 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 ) ( r R a \/ r = a ) -> -. a R b ) ) ) ) )
78	77	impd 447	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( 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 ) ( r R a \/ r = a ) -> -. a R b ) ) ) )
79	78	com4l 92	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( D = (/) /\ ( R Po A /\ ( ( w We A /\ x e. On ) /\ A. y e. x H =/= (/) ) ) ) -> ( a e. A -> ( A. r e. ( F " x ) ( r R a \/ r = a ) -> ( b e. A -> -. a R b ) ) ) )
80	79	impd 447	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( D = (/) /\ ( R Po A /\ ( ( w We A /\ x e. On ) /\ A. y e. x H =/= (/) ) ) ) -> ( ( a e. A /\ A. r e. ( F " x ) ( r R a \/ r = a ) ) -> ( b e. A -> -. a R b ) ) )
81	80	ralrimdv 2968	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( D = (/) /\ ( R Po A /\ ( ( w We A /\ x e. On ) /\ A. y e. x H =/= (/) ) ) ) -> ( ( a e. A /\ A. r e. ( F " x ) ( r R a \/ r = a ) ) -> A. b e. A -. a R b ) )
82	81	expd 452	. . . . . . . . . . . . . . . . . . . 20 |- ( ( D = (/) /\ ( R Po A /\ ( ( w We A /\ x e. On ) /\ A. y e. x H =/= (/) ) ) ) -> ( a e. A -> ( A. r e. ( F " x ) ( r R a \/ r = a ) -> A. b e. A -. a R b ) ) )
83	82	reximdvai 3015	. . . . . . . . . . . . . . . . . . 19 |- ( ( D = (/) /\ ( R Po A /\ ( ( w We A /\ x e. On ) /\ A. y e. x H =/= (/) ) ) ) -> ( E. a e. A A. r e. ( F " x ) ( r R a \/ r = a ) -> E. a e. A A. b e. A -. a R b ) )
84	83	exp32 631	. . . . . . . . . . . . . . . . . 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 ) ( r R a \/ r = a ) -> E. a e. A A. b e. A -. a R b ) ) ) )
85	84	com12 32	. . . . . . . . . . . . . . . . 17 |- ( R Po A -> ( D = (/) -> ( ( ( w We A /\ x e. On ) /\ A. y e. x H =/= (/) ) -> ( E. a e. A A. r e. ( F " x ) ( r R a \/ r = a ) -> E. a e. A A. b e. A -. a R b ) ) ) )
86	85	adantr 481	. . . . . . . . . . . . . . . 16 |- ( ( R Po A /\ A. s ( ( s C_ A /\ R Or s ) -> E. a e. A A. r e. s ( r R a \/ r = a ) ) ) -> ( D = (/) -> ( ( ( w We A /\ x e. On ) /\ A. y e. x H =/= (/) ) -> ( E. a e. A A. r e. ( F " x ) ( r R a \/ r = a ) -> E. a e. A A. b e. A -. a R b ) ) ) )
87	86	imp32 449	. . . . . . . . . . . . . . 15 |- ( ( ( R Po A /\ A. s ( ( s C_ A /\ R Or s ) -> E. a e. A A. r e. s ( r R a \/ r = a ) ) ) /\ ( D = (/) /\ ( ( w We A /\ x e. On ) /\ A. y e. x H =/= (/) ) ) ) -> ( E. a e. A A. r e. ( F " x ) ( r R a \/ r = a ) -> E. a e. A A. b e. A -. a R b ) )
88	36, 87	mpd 15	. . . . . . . . . . . . . 14 |- ( ( ( R Po A /\ A. s ( ( s C_ A /\ R Or s ) -> E. a e. A A. r e. s ( r R a \/ r = a ) ) ) /\ ( D = (/) /\ ( ( w We A /\ x e. On ) /\ A. y e. x H =/= (/) ) ) ) -> E. a e. A A. b e. A -. a R b )
89	88	exp45 642	. . . . . . . . . . . . 13 |- ( ( R Po A /\ A. s ( ( s C_ A /\ R Or s ) -> E. a e. A A. r e. s ( r R a \/ r = a ) ) ) -> ( D = (/) -> ( ( w We A /\ x e. On ) -> ( A. y e. x H =/= (/) -> E. a e. A A. b e. A -. a R b ) ) ) )
90	89	com23 86	. . . . . . . . . . . 12 |- ( ( R Po A /\ A. s ( ( s C_ A /\ R Or s ) -> E. a e. A A. r e. s ( r R a \/ r = a ) ) ) -> ( ( w We A /\ x e. On ) -> ( D = (/) -> ( A. y e. x H =/= (/) -> E. a e. A A. b e. A -. a R b ) ) ) )
91	90	expdimp 453	. . . . . . . . . . 11 |- ( ( ( R Po A /\ A. s ( ( s C_ A /\ R Or s ) -> E. a e. A A. r e. s ( r R a \/ r = a ) ) ) /\ w We A ) -> ( x e. On -> ( D = (/) -> ( A. y e. x H =/= (/) -> E. a e. A A. b e. A -. a R b ) ) ) )
92	91	imp4a 614	. . . . . . . . . 10 |- ( ( ( R Po A /\ A. s ( ( s C_ A /\ R Or s ) -> E. a e. A A. r e. s ( r R a \/ r = a ) ) ) /\ w We A ) -> ( x e. On -> ( ( D = (/) /\ A. y e. x H =/= (/) ) -> E. a e. A A. b e. A -. a R b ) ) )
93	92	com3l 89	. . . . . . . . 9 |- ( 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 ( r R a \/ r = a ) ) ) /\ w We A ) -> E. a e. A A. b e. A -. a R b ) ) )
94	93	rexlimiv 3027	. . . . . . . 8 |- ( 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 ( r R a \/ r = a ) ) ) /\ w We A ) -> E. a e. A A. b e. A -. a R b ) )
95	5, 17, 94	3syl 18	. . . . . . 7 |- ( ( 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 ( r R a \/ r = a ) ) ) /\ w We A ) -> E. a e. A A. b e. A -. a R b ) )
96	95	adantlr 751	. . . . . 6 |- ( ( ( R Po A /\ A. s ( ( s C_ A /\ R Or s ) -> E. a e. A A. r e. s ( r R a \/ r = a ) ) ) /\ w We A ) -> ( ( ( R Po A /\ A. s ( ( s C_ A /\ R Or s ) -> E. a e. A A. r e. s ( r R a \/ r = a ) ) ) /\ w We A ) -> E. a e. A A. b e. A -. a R b ) )
97	96	pm2.43i 52	. . . . 5 |- ( ( ( R Po A /\ A. s ( ( s C_ A /\ R Or s ) -> E. a e. A A. r e. s ( r R a \/ r = a ) ) ) /\ w We A ) -> E. a e. A A. b e. A -. a R b )
98	97	expcom 451	. . . 4 |- ( w We A -> ( ( R Po A /\ A. s ( ( s C_ A /\ R Or s ) -> E. a e. A A. r e. s ( r R a \/ r = a ) ) ) -> E. a e. A A. b e. A -. a R b ) )
99	98	exlimiv 1858	. . 3 |- ( E. w w We A -> ( ( R Po A /\ A. s ( ( s C_ A /\ R Or s ) -> E. a e. A A. r e. s ( r R a \/ r = a ) ) ) -> E. a e. A A. b e. A -. a R b ) )
100	1, 99	sylbi 207	. 2 |- ( A e. dom card -> ( ( R Po A /\ A. s ( ( s C_ A /\ R Or s ) -> E. a e. A A. r e. s ( r R a \/ r = a ) ) ) -> E. a e. A A. b e. A -. a R b ) )
101	100	3impib 1262	1 |- ( ( A e. dom card /\ R Po A /\ A. s ( ( s C_ A /\ R Or s ) -> E. a e. A A. r e. s ( r R a \/ r = a ) ) ) -> E. a e. A A. b e. A -. a R b )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   \/ wo 383   /\ wa 384   /\ w3a 1037   A.wal 1481   = wceq 1483   E.wex 1704   e. wcel 1990   =/= wne 2794   A.wral 2912   E.wrex 2913   {crab 2916   _Vcvv 3200   C_ wss 3574   (/)c0 3915   class class class wbr 4653   |-> cmpt 4729   Po wpo 5033   Or wor 5034   We wwe 5072   dom cdm 5114   ran crn 5115   "cima 5117   Oncon0 5723   Fun wfun 5882   Fn wfn 5883   iota_crio 6610  recscrecs 7467   cardccrd 8761

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-se 5074  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-isom 5897  df-riota 6611  df-wrecs 7407  df-recs 7468  df-en 7956  df-card 8765

This theorem is referenced by:  zorn2g  9325