MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  zorn2lem7 Unicode version

Theorem zorn2lem7 8338
Description: Lemma for zorn2 8342. (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
StepHypRef Expression
1 ween 7872 . . 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 }
52, 3, 4zorn2lem4 8335 . . . . . . . 8  |-  ( ( R  Po  A  /\  w  We  A )  ->  E. x  e.  On  D  =  (/) )
6 imaeq2 5158 . . . . . . . . . . . . . 14  |-  ( x  =  y  ->  ( F " x )  =  ( F " y
) )
76raleqdv 2870 . . . . . . . . . . . . 13  |-  ( x  =  y  ->  ( A. g  e.  ( F " x ) g R z  <->  A. g  e.  ( F " y
) g R z ) )
87rabbidv 2908 . . . . . . . . . . . 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 }
108, 4, 93eqtr4g 2461 . . . . . . . . . . 11  |-  ( x  =  y  ->  D  =  H )
1110eqeq1d 2412 . . . . . . . . . 10  |-  ( x  =  y  ->  ( D  =  (/)  <->  H  =  (/) ) )
1211onminex 4746 . . . . . . . . 9  |-  ( E. x  e.  On  D  =  (/)  ->  E. x  e.  On  ( D  =  (/)  /\  A. y  e.  x  -.  H  =  (/) ) )
13 df-ne 2569 . . . . . . . . . . . 12  |-  ( H  =/=  (/)  <->  -.  H  =  (/) )
1413ralbii 2690 . . . . . . . . . . 11  |-  ( A. y  e.  x  H  =/=  (/)  <->  A. y  e.  x  -.  H  =  (/) )
1514anbi2i 676 . . . . . . . . . 10  |-  ( ( D  =  (/)  /\  A. y  e.  x  H  =/=  (/) )  <->  ( D  =  (/)  /\  A. y  e.  x  -.  H  =  (/) ) )
1615rexbii 2691 . . . . . . . . 9  |-  ( E. x  e.  On  ( D  =  (/)  /\  A. y  e.  x  H  =/=  (/) )  <->  E. x  e.  On  ( D  =  (/)  /\  A. y  e.  x  -.  H  =  (/) ) )
1712, 16sylibr 204 . . . . . . . 8  |-  ( E. x  e.  On  D  =  (/)  ->  E. x  e.  On  ( D  =  (/)  /\  A. y  e.  x  H  =/=  (/) ) )
182, 3, 4, 9zorn2lem5 8336 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( w  We  A  /\  x  e.  On )  /\  A. y  e.  x  H  =/=  (/) )  -> 
( F " x
)  C_  A )
1918a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( R  Po  A  ->  (
( ( w  We  A  /\  x  e.  On )  /\  A. y  e.  x  H  =/=  (/) )  ->  ( F " x )  C_  A ) )
202, 3, 4, 9zorn2lem6 8337 . . . . . . . . . . . . . . . . . . 19  |-  ( R  Po  A  ->  (
( ( w  We  A  /\  x  e.  On )  /\  A. y  e.  x  H  =/=  (/) )  ->  R  Or  ( F " x
) ) )
2119, 20jcad 520 . . . . . . . . . . . . . . . . . 18  |-  ( R  Po  A  ->  (
( ( w  We  A  /\  x  e.  On )  /\  A. y  e.  x  H  =/=  (/) )  ->  (
( F " x
)  C_  A  /\  R  Or  ( F " x ) ) ) )
222tfr1 6617 . . . . . . . . . . . . . . . . . . . 20  |-  F  Fn  On
23 fnfun 5501 . . . . . . . . . . . . . . . . . . . 20  |-  ( F  Fn  On  ->  Fun  F )
24 vex 2919 . . . . . . . . . . . . . . . . . . . . 21  |-  x  e. 
_V
2524funimaex 5490 . . . . . . . . . . . . . . . . . . . 20  |-  ( Fun 
F  ->  ( F " x )  e.  _V )
2622, 23, 25mp2b 10 . . . . . . . . . . . . . . . . . . 19  |-  ( F
" x )  e. 
_V
27 sseq1 3329 . . . . . . . . . . . . . . . . . . . . 21  |-  ( s  =  ( F "
x )  ->  (
s  C_  A  <->  ( F " x )  C_  A
) )
28 soeq2 4483 . . . . . . . . . . . . . . . . . . . . 21  |-  ( s  =  ( F "
x )  ->  ( R  Or  s  <->  R  Or  ( F " x ) ) )
2927, 28anbi12d 692 . . . . . . . . . . . . . . . . . . . 20  |-  ( s  =  ( F "
x )  ->  (
( s  C_  A  /\  R  Or  s
)  <->  ( ( F
" x )  C_  A  /\  R  Or  ( F " x ) ) ) )
30 raleq 2864 . . . . . . . . . . . . . . . . . . . . 21  |-  ( s  =  ( F "
x )  ->  ( A. r  e.  s 
( r R a  \/  r  =  a )  <->  A. r  e.  ( F " x ) ( r R a  \/  r  =  a ) ) )
3130rexbidv 2687 . . . . . . . . . . . . . . . . . . . 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 ) ) )
3229, 31imbi12d 312 . . . . . . . . . . . . . . . . . . 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 ) ) ) )
3326, 32spcv 3002 . . . . . . . . . . . . . . . . . 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 ) ) )
3421, 33sylan9 639 . . . . . . . . . . . . . . . . 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 ) ) )
3534adantld 454 . . . . . . . . . . . . . . . 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 ) ) )
3635imp 419 . . . . . . . . . . . . . . 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 3592 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  -.  b  e.  (/)
3818sseld 3307 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( ( w  We  A  /\  x  e.  On )  /\  A. y  e.  x  H  =/=  (/) )  -> 
( r  e.  ( F " x )  ->  r  e.  A
) )
39 3anass 940 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( ( r  e.  A  /\  a  e.  A  /\  b  e.  A )  <->  ( r  e.  A  /\  ( a  e.  A  /\  b  e.  A
) ) )
40 potr 4475 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( ( R  Po  A  /\  ( r  e.  A  /\  a  e.  A  /\  b  e.  A
) )  ->  (
( r R a  /\  a R b )  ->  r R
b ) )
4139, 40sylan2br 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( ( R  Po  A  /\  ( r  e.  A  /\  ( a  e.  A  /\  b  e.  A
) ) )  -> 
( ( r R a  /\  a R b )  ->  r R b ) )
4241exp3acom23 1378 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( ( R  Po  A  /\  ( r  e.  A  /\  ( a  e.  A  /\  b  e.  A
) ) )  -> 
( a R b  ->  ( r R a  ->  r R
b ) ) )
4342imp 419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( ( ( R  Po  A  /\  ( r  e.  A  /\  ( a  e.  A  /\  b  e.  A
) ) )  /\  a R b )  -> 
( r R a  ->  r R b ) )
44 breq1 4175 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( r  =  a  ->  (
r R b  <->  a R
b ) )
4544biimprcd 217 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( a R b  ->  (
r  =  a  -> 
r R b ) )
4645adantl 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( ( ( R  Po  A  /\  ( r  e.  A  /\  ( a  e.  A  /\  b  e.  A
) ) )  /\  a R b )  -> 
( r  =  a  ->  r R b ) )
4743, 46jaod 370 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( ( ( R  Po  A  /\  ( r  e.  A  /\  ( a  e.  A  /\  b  e.  A
) ) )  /\  a R b )  -> 
( ( r R a  \/  r  =  a )  ->  r R b ) )
4847exp42 595 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( R  Po  A  ->  (
r  e.  A  -> 
( ( a  e.  A  /\  b  e.  A )  ->  (
a R b  -> 
( ( r R a  \/  r  =  a )  ->  r R b ) ) ) ) )
4938, 48sylan9r 640 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
5049com24 83 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
5150com23 74 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
5251imp31 422 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
5352a2d 24 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
5453ralimdv2 2746 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4175 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( r  =  g  ->  (
r R b  <->  g R
b ) )
5655cbvralv 2892 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( A. r  e.  ( F " x ) r R b  <->  A. g  e.  ( F " x ) g R b )
57 breq2 4176 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( z  =  b  ->  (
g R z  <->  g R
b ) )
5857ralbidv 2686 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( z  =  b  ->  ( A. g  e.  ( F " x ) g R z  <->  A. g  e.  ( F " x
) g R b ) )
5958elrab 3052 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
604eqeq1i 2411 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( D  =  (/)  <->  { z  e.  A  |  A. g  e.  ( F " x ) g R z }  =  (/) )
61 eleq2 2465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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.  (/) ) )
6260, 61sylbi 188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( D  =  (/)  ->  ( b  e.  { z  e.  A  |  A. g  e.  ( F " x
) g R z }  <->  b  e.  (/) ) )
6359, 62syl5bbr 251 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( D  =  (/)  ->  ( ( b  e.  A  /\  A. g  e.  ( F
" x ) g R b )  <->  b  e.  (/) ) )
6463biimpd 199 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( D  =  (/)  ->  ( ( b  e.  A  /\  A. g  e.  ( F
" x ) g R b )  -> 
b  e.  (/) ) )
6564expdimp 427 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( D  =  (/)  /\  b  e.  A )  ->  ( A. g  e.  ( F " x ) g R b  ->  b  e.  (/) ) )
6656, 65syl5bi 209 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( D  =  (/)  /\  b  e.  A )  ->  ( A. r  e.  ( F " x ) r R b  ->  b  e.  (/) ) )
6754, 66sylan9r 640 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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.  (/) ) )
6867exp32 589 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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.  (/) ) ) ) )
6968com34 79 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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.  (/) ) ) ) )
7069imp31 422 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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.  (/) ) )
7137, 70mtoi 171 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
7271exp42 595 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
7372exp4a 590 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
7473com34 79 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
7574ex 424 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
7675com4r 82 . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
7776pm2.43a 47 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
7877imp3a 421 . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
7978com4l 80 . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
8079imp3a 421 . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
8180ralrimdv 2755 . . . . . . . . . . . . . . . . . . . . 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 ) )
8281exp3a 426 . . . . . . . . . . . . . . . . . . . 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 ) ) )
8382reximdvai 2776 . . . . . . . . . . . . . . . . . . 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 ) )
8483exp32 589 . . . . . . . . . . . . . . . . . 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 ) ) ) )
8584com12 29 . . . . . . . . . . . . . . . . 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 ) ) ) )
8685adantr 452 . . . . . . . . . . . . . . . 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 ) ) ) )
8786imp32 423 . . . . . . . . . . . . . . 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 ) )
8836, 87mpd 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 )
8988exp45 598 . . . . . . . . . . . . 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 ) ) ) )
9089com23 74 . . . . . . . . . . . 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 ) ) ) )
9190expdimp 427 . . . . . . . . . . 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 ) ) ) )
9291imp4a 573 . . . . . . . . . 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 ) ) )
9392com3l 77 . . . . . . . . 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 ) ) )
9493rexlimiv 2784 . . . . . . . 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 ) )
955, 17, 943syl 19 . . . . . . 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 ) )
9695adantlr 696 . . . . . 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 ) )
9796pm2.43i 45 . . . . 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 )
9897expcom 425 . . . 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 ) )
9998exlimiv 1641 . . 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 ) )
1001, 99sylbi 188 . 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 ) )
1011003impib 1151 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 )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177    \/ wo 358    /\ wa 359    /\ w3a 936   A.wal 1546   E.wex 1547    = wceq 1649    e. wcel 1721    =/= wne 2567   A.wral 2666   E.wrex 2667   {crab 2670   _Vcvv 2916    C_ wss 3280   (/)c0 3588   class class class wbr 4172    e. cmpt 4226    Po wpo 4461    Or wor 4462    We wwe 4500   Oncon0 4541   dom cdm 4837   ran crn 4838   "cima 4840   Fun wfun 5407    Fn wfn 5408   iota_crio 6501  recscrecs 6591   cardccrd 7778
This theorem is referenced by:  zorn2g  8339
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-rep 4280  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-reu 2673  df-rmo 2674  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-tp 3782  df-op 3783  df-uni 3976  df-int 4011  df-iun 4055  df-br 4173  df-opab 4227  df-mpt 4228  df-tr 4263  df-eprel 4454  df-id 4458  df-po 4463  df-so 4464  df-fr 4501  df-se 4502  df-we 4503  df-ord 4544  df-on 4545  df-suc 4547  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-isom 5422  df-riota 6508  df-recs 6592  df-en 7069  df-card 7782
  Copyright terms: Public domain W3C validator