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

Theorem zorn2lem6 8412
Description: Lemma for zorn2 8417. (Contributed by NM, 4-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
zorn2lem6  |-  ( R  Po  A  ->  (
( ( w  We  A  /\  x  e.  On )  /\  A. y  e.  x  H  =/=  (/) )  ->  R  Or  ( F " x
) ) )
Distinct variable groups:    f, g, u, v, w, x, y, z, A    D, f, u, v, y    f, F, g, u, v, x, y, z    R, f, g, u, v, w, x, y, z    v, C    x, H, u, v, f
Allowed substitution hints:    C( x, y, z, w, u, f, g)    D( x, z, w, g)    F( w)    H( y,
z, w, g)

Proof of Theorem zorn2lem6
Dummy variables  a 
b  r  s are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 zorn2lem.3 . . . . . 6  |-  F  = recs ( ( f  e. 
_V  |->  ( iota_ v  e.  C A. u  e.  C  -.  u w v ) ) )
2 zorn2lem.4 . . . . . 6  |-  C  =  { z  e.  A  |  A. g  e.  ran  f  g R z }
3 zorn2lem.5 . . . . . 6  |-  D  =  { z  e.  A  |  A. g  e.  ( F " x ) g R z }
4 zorn2lem.7 . . . . . 6  |-  H  =  { z  e.  A  |  A. g  e.  ( F " y ) g R z }
51, 2, 3, 4zorn2lem5 8411 . . . . 5  |-  ( ( ( w  We  A  /\  x  e.  On )  /\  A. y  e.  x  H  =/=  (/) )  -> 
( F " x
)  C_  A )
6 poss 4534 . . . . 5  |-  ( ( F " x ) 
C_  A  ->  ( R  Po  A  ->  R  Po  ( F "
x ) ) )
75, 6syl 16 . . . 4  |-  ( ( ( w  We  A  /\  x  e.  On )  /\  A. y  e.  x  H  =/=  (/) )  -> 
( R  Po  A  ->  R  Po  ( F
" x ) ) )
87com12 30 . . 3  |-  ( R  Po  A  ->  (
( ( w  We  A  /\  x  e.  On )  /\  A. y  e.  x  H  =/=  (/) )  ->  R  Po  ( F " x
) ) )
91tfr1 6687 . . . . . . . 8  |-  F  Fn  On
10 fnfun 5571 . . . . . . . 8  |-  ( F  Fn  On  ->  Fun  F )
11 fvelima 5807 . . . . . . . . . . 11  |-  ( ( Fun  F  /\  s  e.  ( F " x
) )  ->  E. b  e.  x  ( F `  b )  =  s )
12 df-rex 2717 . . . . . . . . . . 11  |-  ( E. b  e.  x  ( F `  b )  =  s  <->  E. b
( b  e.  x  /\  ( F `  b
)  =  s ) )
1311, 12sylib 190 . . . . . . . . . 10  |-  ( ( Fun  F  /\  s  e.  ( F " x
) )  ->  E. b
( b  e.  x  /\  ( F `  b
)  =  s ) )
1413ex 425 . . . . . . . . 9  |-  ( Fun 
F  ->  ( s  e.  ( F " x
)  ->  E. b
( b  e.  x  /\  ( F `  b
)  =  s ) ) )
15 fvelima 5807 . . . . . . . . . . 11  |-  ( ( Fun  F  /\  r  e.  ( F " x
) )  ->  E. a  e.  x  ( F `  a )  =  r )
16 df-rex 2717 . . . . . . . . . . 11  |-  ( E. a  e.  x  ( F `  a )  =  r  <->  E. a
( a  e.  x  /\  ( F `  a
)  =  r ) )
1715, 16sylib 190 . . . . . . . . . 10  |-  ( ( Fun  F  /\  r  e.  ( F " x
) )  ->  E. a
( a  e.  x  /\  ( F `  a
)  =  r ) )
1817ex 425 . . . . . . . . 9  |-  ( Fun 
F  ->  ( r  e.  ( F " x
)  ->  E. a
( a  e.  x  /\  ( F `  a
)  =  r ) ) )
1914, 18anim12d 548 . . . . . . . 8  |-  ( Fun 
F  ->  ( (
s  e.  ( F
" x )  /\  r  e.  ( F " x ) )  -> 
( E. b ( b  e.  x  /\  ( F `  b )  =  s )  /\  E. a ( a  e.  x  /\  ( F `
 a )  =  r ) ) ) )
209, 10, 19mp2b 10 . . . . . . 7  |-  ( ( s  e.  ( F
" x )  /\  r  e.  ( F " x ) )  -> 
( E. b ( b  e.  x  /\  ( F `  b )  =  s )  /\  E. a ( a  e.  x  /\  ( F `
 a )  =  r ) ) )
21 an4 799 . . . . . . . . 9  |-  ( ( ( b  e.  x  /\  a  e.  x
)  /\  ( ( F `  b )  =  s  /\  ( F `  a )  =  r ) )  <-> 
( ( b  e.  x  /\  ( F `
 b )  =  s )  /\  (
a  e.  x  /\  ( F `  a )  =  r ) ) )
22212exbii 1594 . . . . . . . 8  |-  ( E. b E. a ( ( b  e.  x  /\  a  e.  x
)  /\  ( ( F `  b )  =  s  /\  ( F `  a )  =  r ) )  <->  E. b E. a ( ( b  e.  x  /\  ( F `  b
)  =  s )  /\  ( a  e.  x  /\  ( F `
 a )  =  r ) ) )
23 eeanv 1940 . . . . . . . 8  |-  ( E. b E. a ( ( b  e.  x  /\  ( F `  b
)  =  s )  /\  ( a  e.  x  /\  ( F `
 a )  =  r ) )  <->  ( E. b ( b  e.  x  /\  ( F `
 b )  =  s )  /\  E. a ( a  e.  x  /\  ( F `
 a )  =  r ) ) )
2422, 23bitri 242 . . . . . . 7  |-  ( E. b E. a ( ( b  e.  x  /\  a  e.  x
)  /\  ( ( F `  b )  =  s  /\  ( F `  a )  =  r ) )  <-> 
( E. b ( b  e.  x  /\  ( F `  b )  =  s )  /\  E. a ( a  e.  x  /\  ( F `
 a )  =  r ) ) )
2520, 24sylibr 205 . . . . . 6  |-  ( ( s  e.  ( F
" x )  /\  r  e.  ( F " x ) )  ->  E. b E. a ( ( b  e.  x  /\  a  e.  x
)  /\  ( ( F `  b )  =  s  /\  ( F `  a )  =  r ) ) )
264neeq1i 2617 . . . . . . . . . . 11  |-  ( H  =/=  (/)  <->  { z  e.  A  |  A. g  e.  ( F " y ) g R z }  =/=  (/) )
2726ralbii 2735 . . . . . . . . . 10  |-  ( A. y  e.  x  H  =/=  (/)  <->  A. y  e.  x  { z  e.  A  |  A. g  e.  ( F " y ) g R z }  =/=  (/) )
28 imaeq2 5228 . . . . . . . . . . . . . . 15  |-  ( y  =  b  ->  ( F " y )  =  ( F " b
) )
2928raleqdv 2916 . . . . . . . . . . . . . 14  |-  ( y  =  b  ->  ( A. g  e.  ( F " y ) g R z  <->  A. g  e.  ( F " b
) g R z ) )
3029rabbidv 2954 . . . . . . . . . . . . 13  |-  ( y  =  b  ->  { z  e.  A  |  A. g  e.  ( F " y ) g R z }  =  {
z  e.  A  |  A. g  e.  ( F " b ) g R z } )
3130neeq1d 2620 . . . . . . . . . . . 12  |-  ( y  =  b  ->  ( { z  e.  A  |  A. g  e.  ( F " y ) g R z }  =/=  (/)  <->  { z  e.  A  |  A. g  e.  ( F " b ) g R z }  =/=  (/) ) )
3231rspccv 3055 . . . . . . . . . . 11  |-  ( A. y  e.  x  {
z  e.  A  |  A. g  e.  ( F " y ) g R z }  =/=  (/) 
->  ( b  e.  x  ->  { z  e.  A  |  A. g  e.  ( F " b ) g R z }  =/=  (/) ) )
33 imaeq2 5228 . . . . . . . . . . . . . . 15  |-  ( y  =  a  ->  ( F " y )  =  ( F " a
) )
3433raleqdv 2916 . . . . . . . . . . . . . 14  |-  ( y  =  a  ->  ( A. g  e.  ( F " y ) g R z  <->  A. g  e.  ( F " a
) g R z ) )
3534rabbidv 2954 . . . . . . . . . . . . 13  |-  ( y  =  a  ->  { z  e.  A  |  A. g  e.  ( F " y ) g R z }  =  {
z  e.  A  |  A. g  e.  ( F " a ) g R z } )
3635neeq1d 2620 . . . . . . . . . . . 12  |-  ( y  =  a  ->  ( { z  e.  A  |  A. g  e.  ( F " y ) g R z }  =/=  (/)  <->  { z  e.  A  |  A. g  e.  ( F " a ) g R z }  =/=  (/) ) )
3736rspccv 3055 . . . . . . . . . . 11  |-  ( A. y  e.  x  {
z  e.  A  |  A. g  e.  ( F " y ) g R z }  =/=  (/) 
->  ( a  e.  x  ->  { z  e.  A  |  A. g  e.  ( F " a ) g R z }  =/=  (/) ) )
3832, 37anim12d 548 . . . . . . . . . 10  |-  ( A. y  e.  x  {
z  e.  A  |  A. g  e.  ( F " y ) g R z }  =/=  (/) 
->  ( ( b  e.  x  /\  a  e.  x )  ->  ( { z  e.  A  |  A. g  e.  ( F " b ) g R z }  =/=  (/)  /\  { z  e.  A  |  A. g  e.  ( F " a ) g R z }  =/=  (/) ) ) )
3927, 38sylbi 189 . . . . . . . . 9  |-  ( A. y  e.  x  H  =/=  (/)  ->  ( (
b  e.  x  /\  a  e.  x )  ->  ( { z  e.  A  |  A. g  e.  ( F " b
) g R z }  =/=  (/)  /\  {
z  e.  A  |  A. g  e.  ( F " a ) g R z }  =/=  (/) ) ) )
40 onelon 4635 . . . . . . . . . . . . . . . 16  |-  ( ( x  e.  On  /\  b  e.  x )  ->  b  e.  On )
41 onelon 4635 . . . . . . . . . . . . . . . 16  |-  ( ( x  e.  On  /\  a  e.  x )  ->  a  e.  On )
4240, 41anim12dan 812 . . . . . . . . . . . . . . 15  |-  ( ( x  e.  On  /\  ( b  e.  x  /\  a  e.  x
) )  ->  (
b  e.  On  /\  a  e.  On )
)
4342ex 425 . . . . . . . . . . . . . 14  |-  ( x  e.  On  ->  (
( b  e.  x  /\  a  e.  x
)  ->  ( b  e.  On  /\  a  e.  On ) ) )
44 eloni 4620 . . . . . . . . . . . . . . . . . 18  |-  ( b  e.  On  ->  Ord  b )
45 eloni 4620 . . . . . . . . . . . . . . . . . 18  |-  ( a  e.  On  ->  Ord  a )
46 ordtri3or 4642 . . . . . . . . . . . . . . . . . 18  |-  ( ( Ord  b  /\  Ord  a )  ->  (
b  e.  a  \/  b  =  a  \/  a  e.  b ) )
4744, 45, 46syl2an 465 . . . . . . . . . . . . . . . . 17  |-  ( ( b  e.  On  /\  a  e.  On )  ->  ( b  e.  a  \/  b  =  a  \/  a  e.  b ) )
48 eqid 2442 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  { z  e.  A  |  A. g  e.  ( F " a ) g R z }  =  {
z  e.  A  |  A. g  e.  ( F " a ) g R z }
491, 2, 48zorn2lem2 8408 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( a  e.  On  /\  ( w  We  A  /\  { z  e.  A  |  A. g  e.  ( F " a ) g R z }  =/=  (/) ) )  -> 
( b  e.  a  ->  ( F `  b ) R ( F `  a ) ) )
5049adantll 696 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( b  e.  On  /\  a  e.  On )  /\  ( w  We  A  /\  { z  e.  A  |  A. g  e.  ( F " a ) g R z }  =/=  (/) ) )  ->  ( b  e.  a  ->  ( F `  b ) R ( F `  a ) ) )
51 breq12 4242 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( F `  b
)  =  s  /\  ( F `  a )  =  r )  -> 
( ( F `  b ) R ( F `  a )  <-> 
s R r ) )
5251biimpcd 217 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( F `  b ) R ( F `  a )  ->  (
( ( F `  b )  =  s  /\  ( F `  a )  =  r )  ->  s R
r ) )
5350, 52syl6 32 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( b  e.  On  /\  a  e.  On )  /\  ( w  We  A  /\  { z  e.  A  |  A. g  e.  ( F " a ) g R z }  =/=  (/) ) )  ->  ( b  e.  a  ->  ( (
( F `  b
)  =  s  /\  ( F `  a )  =  r )  -> 
s R r ) ) )
5453com23 75 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( b  e.  On  /\  a  e.  On )  /\  ( w  We  A  /\  { z  e.  A  |  A. g  e.  ( F " a ) g R z }  =/=  (/) ) )  ->  ( ( ( F `  b )  =  s  /\  ( F `  a )  =  r )  -> 
( b  e.  a  ->  s R r ) ) )
5554adantrrl 706 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( b  e.  On  /\  a  e.  On )  /\  ( w  We  A  /\  ( { z  e.  A  |  A. g  e.  ( F " b ) g R z }  =/=  (/) 
/\  { z  e.  A  |  A. g  e.  ( F " a
) g R z }  =/=  (/) ) ) )  ->  ( (
( F `  b
)  =  s  /\  ( F `  a )  =  r )  -> 
( b  e.  a  ->  s R r ) ) )
5655imp 420 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( b  e.  On  /\  a  e.  On )  /\  (
w  We  A  /\  ( { z  e.  A  |  A. g  e.  ( F " b ) g R z }  =/=  (/)  /\  { z  e.  A  |  A. g  e.  ( F " a ) g R z }  =/=  (/) ) ) )  /\  ( ( F `  b )  =  s  /\  ( F `  a )  =  r ) )  ->  ( b  e.  a  ->  s R
r ) )
57 fveq2 5757 . . . . . . . . . . . . . . . . . . . 20  |-  ( b  =  a  ->  ( F `  b )  =  ( F `  a ) )
58 eqeq12 2454 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( F `  b
)  =  s  /\  ( F `  a )  =  r )  -> 
( ( F `  b )  =  ( F `  a )  <-> 
s  =  r ) )
5957, 58syl5ib 212 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( F `  b
)  =  s  /\  ( F `  a )  =  r )  -> 
( b  =  a  ->  s  =  r ) )
6059adantl 454 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( b  e.  On  /\  a  e.  On )  /\  (
w  We  A  /\  ( { z  e.  A  |  A. g  e.  ( F " b ) g R z }  =/=  (/)  /\  { z  e.  A  |  A. g  e.  ( F " a ) g R z }  =/=  (/) ) ) )  /\  ( ( F `  b )  =  s  /\  ( F `  a )  =  r ) )  ->  ( b  =  a  ->  s  =  r ) )
61 eqid 2442 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  { z  e.  A  |  A. g  e.  ( F " b ) g R z }  =  {
z  e.  A  |  A. g  e.  ( F " b ) g R z }
621, 2, 61zorn2lem2 8408 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( b  e.  On  /\  ( w  We  A  /\  { z  e.  A  |  A. g  e.  ( F " b ) g R z }  =/=  (/) ) )  -> 
( a  e.  b  ->  ( F `  a ) R ( F `  b ) ) )
6362adantlr 697 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( b  e.  On  /\  a  e.  On )  /\  ( w  We  A  /\  { z  e.  A  |  A. g  e.  ( F " b ) g R z }  =/=  (/) ) )  ->  ( a  e.  b  ->  ( F `  a ) R ( F `  b ) ) )
64 breq12 4242 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( F `  a
)  =  r  /\  ( F `  b )  =  s )  -> 
( ( F `  a ) R ( F `  b )  <-> 
r R s ) )
6564ancoms 441 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( F `  b
)  =  s  /\  ( F `  a )  =  r )  -> 
( ( F `  a ) R ( F `  b )  <-> 
r R s ) )
6665biimpcd 217 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( F `  a ) R ( F `  b )  ->  (
( ( F `  b )  =  s  /\  ( F `  a )  =  r )  ->  r R
s ) )
6763, 66syl6 32 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( b  e.  On  /\  a  e.  On )  /\  ( w  We  A  /\  { z  e.  A  |  A. g  e.  ( F " b ) g R z }  =/=  (/) ) )  ->  ( a  e.  b  ->  ( (
( F `  b
)  =  s  /\  ( F `  a )  =  r )  -> 
r R s ) ) )
6867com23 75 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( b  e.  On  /\  a  e.  On )  /\  ( w  We  A  /\  { z  e.  A  |  A. g  e.  ( F " b ) g R z }  =/=  (/) ) )  ->  ( ( ( F `  b )  =  s  /\  ( F `  a )  =  r )  -> 
( a  e.  b  ->  r R s ) ) )
6968adantrrr 707 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( b  e.  On  /\  a  e.  On )  /\  ( w  We  A  /\  ( { z  e.  A  |  A. g  e.  ( F " b ) g R z }  =/=  (/) 
/\  { z  e.  A  |  A. g  e.  ( F " a
) g R z }  =/=  (/) ) ) )  ->  ( (
( F `  b
)  =  s  /\  ( F `  a )  =  r )  -> 
( a  e.  b  ->  r R s ) ) )
7069imp 420 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( b  e.  On  /\  a  e.  On )  /\  (
w  We  A  /\  ( { z  e.  A  |  A. g  e.  ( F " b ) g R z }  =/=  (/)  /\  { z  e.  A  |  A. g  e.  ( F " a ) g R z }  =/=  (/) ) ) )  /\  ( ( F `  b )  =  s  /\  ( F `  a )  =  r ) )  ->  ( a  e.  b  ->  r R
s ) )
7156, 60, 703orim123d 1263 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( b  e.  On  /\  a  e.  On )  /\  (
w  We  A  /\  ( { z  e.  A  |  A. g  e.  ( F " b ) g R z }  =/=  (/)  /\  { z  e.  A  |  A. g  e.  ( F " a ) g R z }  =/=  (/) ) ) )  /\  ( ( F `  b )  =  s  /\  ( F `  a )  =  r ) )  ->  ( ( b  e.  a  \/  b  =  a  \/  a  e.  b )  ->  (
s R r  \/  s  =  r  \/  r R s ) ) )
7247, 71syl5 31 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( b  e.  On  /\  a  e.  On )  /\  (
w  We  A  /\  ( { z  e.  A  |  A. g  e.  ( F " b ) g R z }  =/=  (/)  /\  { z  e.  A  |  A. g  e.  ( F " a ) g R z }  =/=  (/) ) ) )  /\  ( ( F `  b )  =  s  /\  ( F `  a )  =  r ) )  ->  ( ( b  e.  On  /\  a  e.  On )  ->  (
s R r  \/  s  =  r  \/  r R s ) ) )
7372exp31 589 . . . . . . . . . . . . . . 15  |-  ( ( b  e.  On  /\  a  e.  On )  ->  ( ( w  We  A  /\  ( { z  e.  A  |  A. g  e.  ( F " b ) g R z }  =/=  (/) 
/\  { z  e.  A  |  A. g  e.  ( F " a
) g R z }  =/=  (/) ) )  ->  ( ( ( F `  b )  =  s  /\  ( F `  a )  =  r )  -> 
( ( b  e.  On  /\  a  e.  On )  ->  (
s R r  \/  s  =  r  \/  r R s ) ) ) ) )
7473com4r 83 . . . . . . . . . . . . . 14  |-  ( ( b  e.  On  /\  a  e.  On )  ->  ( ( b  e.  On  /\  a  e.  On )  ->  (
( w  We  A  /\  ( { z  e.  A  |  A. g  e.  ( F " b
) g R z }  =/=  (/)  /\  {
z  e.  A  |  A. g  e.  ( F " a ) g R z }  =/=  (/) ) )  ->  (
( ( F `  b )  =  s  /\  ( F `  a )  =  r )  ->  ( s R r  \/  s  =  r  \/  r R s ) ) ) ) )
7543, 43, 74syl6c 63 . . . . . . . . . . . . 13  |-  ( x  e.  On  ->  (
( b  e.  x  /\  a  e.  x
)  ->  ( (
w  We  A  /\  ( { z  e.  A  |  A. g  e.  ( F " b ) g R z }  =/=  (/)  /\  { z  e.  A  |  A. g  e.  ( F " a ) g R z }  =/=  (/) ) )  ->  ( ( ( F `  b )  =  s  /\  ( F `  a )  =  r )  -> 
( s R r  \/  s  =  r  \/  r R s ) ) ) ) )
7675exp4a 591 . . . . . . . . . . . 12  |-  ( x  e.  On  ->  (
( b  e.  x  /\  a  e.  x
)  ->  ( w  We  A  ->  ( ( { z  e.  A  |  A. g  e.  ( F " b ) g R z }  =/=  (/)  /\  { z  e.  A  |  A. g  e.  ( F " a ) g R z }  =/=  (/) )  -> 
( ( ( F `
 b )  =  s  /\  ( F `
 a )  =  r )  ->  (
s R r  \/  s  =  r  \/  r R s ) ) ) ) ) )
7776com3r 76 . . . . . . . . . . 11  |-  ( w  We  A  ->  (
x  e.  On  ->  ( ( b  e.  x  /\  a  e.  x
)  ->  ( ( { z  e.  A  |  A. g  e.  ( F " b ) g R z }  =/=  (/)  /\  { z  e.  A  |  A. g  e.  ( F " a ) g R z }  =/=  (/) )  -> 
( ( ( F `
 b )  =  s  /\  ( F `
 a )  =  r )  ->  (
s R r  \/  s  =  r  \/  r R s ) ) ) ) ) )
7877imp 420 . . . . . . . . . 10  |-  ( ( w  We  A  /\  x  e.  On )  ->  ( ( b  e.  x  /\  a  e.  x )  ->  (
( { z  e.  A  |  A. g  e.  ( F " b
) g R z }  =/=  (/)  /\  {
z  e.  A  |  A. g  e.  ( F " a ) g R z }  =/=  (/) )  ->  ( (
( F `  b
)  =  s  /\  ( F `  a )  =  r )  -> 
( s R r  \/  s  =  r  \/  r R s ) ) ) ) )
7978a2d 25 . . . . . . . . 9  |-  ( ( w  We  A  /\  x  e.  On )  ->  ( ( ( b  e.  x  /\  a  e.  x )  ->  ( { z  e.  A  |  A. g  e.  ( F " b ) g R z }  =/=  (/)  /\  { z  e.  A  |  A. g  e.  ( F " a ) g R z }  =/=  (/) ) )  ->  ( ( b  e.  x  /\  a  e.  x )  ->  (
( ( F `  b )  =  s  /\  ( F `  a )  =  r )  ->  ( s R r  \/  s  =  r  \/  r R s ) ) ) ) )
8039, 79syl5 31 . . . . . . . 8  |-  ( ( w  We  A  /\  x  e.  On )  ->  ( A. y  e.  x  H  =/=  (/)  ->  (
( b  e.  x  /\  a  e.  x
)  ->  ( (
( F `  b
)  =  s  /\  ( F `  a )  =  r )  -> 
( s R r  \/  s  =  r  \/  r R s ) ) ) ) )
8180imp4b 575 . . . . . . 7  |-  ( ( ( w  We  A  /\  x  e.  On )  /\  A. y  e.  x  H  =/=  (/) )  -> 
( ( ( b  e.  x  /\  a  e.  x )  /\  (
( F `  b
)  =  s  /\  ( F `  a )  =  r ) )  ->  ( s R r  \/  s  =  r  \/  r R s ) ) )
8281exlimdvv 1648 . . . . . 6  |-  ( ( ( w  We  A  /\  x  e.  On )  /\  A. y  e.  x  H  =/=  (/) )  -> 
( E. b E. a ( ( b  e.  x  /\  a  e.  x )  /\  (
( F `  b
)  =  s  /\  ( F `  a )  =  r ) )  ->  ( s R r  \/  s  =  r  \/  r R s ) ) )
8325, 82syl5 31 . . . . 5  |-  ( ( ( w  We  A  /\  x  e.  On )  /\  A. y  e.  x  H  =/=  (/) )  -> 
( ( s  e.  ( F " x
)  /\  r  e.  ( F " x ) )  ->  ( s R r  \/  s  =  r  \/  r R s ) ) )
8483ralrimivv 2803 . . . 4  |-  ( ( ( w  We  A  /\  x  e.  On )  /\  A. y  e.  x  H  =/=  (/) )  ->  A. s  e.  ( F " x ) A. r  e.  ( F " x ) ( s R r  \/  s  =  r  \/  r R s ) )
8584a1i 11 . . 3  |-  ( R  Po  A  ->  (
( ( w  We  A  /\  x  e.  On )  /\  A. y  e.  x  H  =/=  (/) )  ->  A. s  e.  ( F " x
) A. r  e.  ( F " x
) ( s R r  \/  s  =  r  \/  r R s ) ) )
868, 85jcad 521 . 2  |-  ( R  Po  A  ->  (
( ( w  We  A  /\  x  e.  On )  /\  A. y  e.  x  H  =/=  (/) )  ->  ( R  Po  ( F " x )  /\  A. s  e.  ( F " x ) A. r  e.  ( F " x
) ( s R r  \/  s  =  r  \/  r R s ) ) ) )
87 df-so 4533 . 2  |-  ( R  Or  ( F "
x )  <->  ( R  Po  ( F " x
)  /\  A. s  e.  ( F " x
) A. r  e.  ( F " x
) ( s R r  \/  s  =  r  \/  r R s ) ) )
8886, 87syl6ibr 220 1  |-  ( R  Po  A  ->  (
( ( w  We  A  /\  x  e.  On )  /\  A. y  e.  x  H  =/=  (/) )  ->  R  Or  ( F " x
) ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 178    /\ wa 360    \/ w3o 936   E.wex 1551    = wceq 1653    e. wcel 1727    =/= wne 2605   A.wral 2711   E.wrex 2712   {crab 2715   _Vcvv 2962    C_ wss 3306   (/)c0 3613   class class class wbr 4237    e. cmpt 4291    Po wpo 4530    Or wor 4531    We wwe 4569   Ord word 4609   Oncon0 4610   ran crn 4908   "cima 4910   Fun wfun 5477    Fn wfn 5478   ` cfv 5483   iota_crio 6571  recscrecs 6661
This theorem is referenced by:  zorn2lem7  8413
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1668  ax-8 1689  ax-13 1729  ax-14 1731  ax-6 1746  ax-7 1751  ax-11 1763  ax-12 1953  ax-ext 2423  ax-rep 4345  ax-sep 4355  ax-nul 4363  ax-pow 4406  ax-pr 4432  ax-un 4730
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2291  df-mo 2292  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-ne 2607  df-ral 2716  df-rex 2717  df-reu 2718  df-rmo 2719  df-rab 2720  df-v 2964  df-sbc 3168  df-csb 3268  df-dif 3309  df-un 3311  df-in 3313  df-ss 3320  df-pss 3322  df-nul 3614  df-if 3764  df-sn 3844  df-pr 3845  df-tp 3846  df-op 3847  df-uni 4040  df-iun 4119  df-br 4238  df-opab 4292  df-mpt 4293  df-tr 4328  df-eprel 4523  df-id 4527  df-po 4532  df-so 4533  df-fr 4570  df-we 4572  df-ord 4613  df-on 4614  df-suc 4616  df-xp 4913  df-rel 4914  df-cnv 4915  df-co 4916  df-dm 4917  df-rn 4918  df-res 4919  df-ima 4920  df-iota 5447  df-fun 5485  df-fn 5486  df-f 5487  df-f1 5488  df-fo 5489  df-f1o 5490  df-fv 5491  df-riota 6578  df-recs 6662
  Copyright terms: Public domain W3C validator