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

Theorem zorn2lem6 8957
Description: Lemma for zorn2 8962. (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 8956 . . . . 5  |-  ( ( ( w  We  A  /\  x  e.  On )  /\  A. y  e.  x  H  =/=  (/) )  -> 
( F " x
)  C_  A )
6 poss 4776 . . . . 5  |-  ( ( F " x ) 
C_  A  ->  ( R  Po  A  ->  R  Po  ( F "
x ) ) )
75, 6syl 17 . . . 4  |-  ( ( ( w  We  A  /\  x  e.  On )  /\  A. y  e.  x  H  =/=  (/) )  -> 
( R  Po  A  ->  R  Po  ( F
" x ) ) )
87com12 32 . . 3  |-  ( R  Po  A  ->  (
( ( w  We  A  /\  x  e.  On )  /\  A. y  e.  x  H  =/=  (/) )  ->  R  Po  ( F " x
) ) )
91tfr1 7141 . . . . . . . 8  |-  F  Fn  On
10 fnfun 5695 . . . . . . . 8  |-  ( F  Fn  On  ->  Fun  F )
11 fvelima 5940 . . . . . . . . . . 11  |-  ( ( Fun  F  /\  s  e.  ( F " x
) )  ->  E. b  e.  x  ( F `  b )  =  s )
12 df-rex 2755 . . . . . . . . . . 11  |-  ( E. b  e.  x  ( F `  b )  =  s  <->  E. b
( b  e.  x  /\  ( F `  b
)  =  s ) )
1311, 12sylib 201 . . . . . . . . . 10  |-  ( ( Fun  F  /\  s  e.  ( F " x
) )  ->  E. b
( b  e.  x  /\  ( F `  b
)  =  s ) )
1413ex 440 . . . . . . . . 9  |-  ( Fun 
F  ->  ( s  e.  ( F " x
)  ->  E. b
( b  e.  x  /\  ( F `  b
)  =  s ) ) )
15 fvelima 5940 . . . . . . . . . . 11  |-  ( ( Fun  F  /\  r  e.  ( F " x
) )  ->  E. a  e.  x  ( F `  a )  =  r )
16 df-rex 2755 . . . . . . . . . . 11  |-  ( E. a  e.  x  ( F `  a )  =  r  <->  E. a
( a  e.  x  /\  ( F `  a
)  =  r ) )
1715, 16sylib 201 . . . . . . . . . 10  |-  ( ( Fun  F  /\  r  e.  ( F " x
) )  ->  E. a
( a  e.  x  /\  ( F `  a
)  =  r ) )
1817ex 440 . . . . . . . . 9  |-  ( Fun 
F  ->  ( r  e.  ( F " x
)  ->  E. a
( a  e.  x  /\  ( F `  a
)  =  r ) ) )
1914, 18anim12d 570 . . . . . . . 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 838 . . . . . . . . 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 1730 . . . . . . . 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 2089 . . . . . . . 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 257 . . . . . . 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 217 . . . . . 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 2700 . . . . . . . . . . 11  |-  ( H  =/=  (/)  <->  { z  e.  A  |  A. g  e.  ( F " y ) g R z }  =/=  (/) )
2726ralbii 2831 . . . . . . . . . 10  |-  ( A. y  e.  x  H  =/=  (/)  <->  A. y  e.  x  { z  e.  A  |  A. g  e.  ( F " y ) g R z }  =/=  (/) )
28 imaeq2 5183 . . . . . . . . . . . . . . 15  |-  ( y  =  b  ->  ( F " y )  =  ( F " b
) )
2928raleqdv 3005 . . . . . . . . . . . . . 14  |-  ( y  =  b  ->  ( A. g  e.  ( F " y ) g R z  <->  A. g  e.  ( F " b
) g R z ) )
3029rabbidv 3048 . . . . . . . . . . . . 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 2695 . . . . . . . . . . . 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 3159 . . . . . . . . . . 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 5183 . . . . . . . . . . . . . . 15  |-  ( y  =  a  ->  ( F " y )  =  ( F " a
) )
3433raleqdv 3005 . . . . . . . . . . . . . 14  |-  ( y  =  a  ->  ( A. g  e.  ( F " y ) g R z  <->  A. g  e.  ( F " a
) g R z ) )
3534rabbidv 3048 . . . . . . . . . . . . 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 2695 . . . . . . . . . . . 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 3159 . . . . . . . . . . 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 570 . . . . . . . . . 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 200 . . . . . . . . 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 5467 . . . . . . . . . . . . . . . 16  |-  ( ( x  e.  On  /\  b  e.  x )  ->  b  e.  On )
41 onelon 5467 . . . . . . . . . . . . . . . 16  |-  ( ( x  e.  On  /\  a  e.  x )  ->  a  e.  On )
4240, 41anim12dan 853 . . . . . . . . . . . . . . 15  |-  ( ( x  e.  On  /\  ( b  e.  x  /\  a  e.  x
) )  ->  (
b  e.  On  /\  a  e.  On )
)
4342ex 440 . . . . . . . . . . . . . 14  |-  ( x  e.  On  ->  (
( b  e.  x  /\  a  e.  x
)  ->  ( b  e.  On  /\  a  e.  On ) ) )
44 eloni 5452 . . . . . . . . . . . . . . . . . 18  |-  ( b  e.  On  ->  Ord  b )
45 eloni 5452 . . . . . . . . . . . . . . . . . 18  |-  ( a  e.  On  ->  Ord  a )
46 ordtri3or 5474 . . . . . . . . . . . . . . . . . 18  |-  ( ( Ord  b  /\  Ord  a )  ->  (
b  e.  a  \/  b  =  a  \/  a  e.  b ) )
4744, 45, 46syl2an 484 . . . . . . . . . . . . . . . . 17  |-  ( ( b  e.  On  /\  a  e.  On )  ->  ( b  e.  a  \/  b  =  a  \/  a  e.  b ) )
48 eqid 2462 . . . . . . . . . . . . . . . . . . . . . . . 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 8953 . . . . . . . . . . . . . . . . . . . . . . 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 725 . . . . . . . . . . . . . . . . . . . . . 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 4421 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( F `  b
)  =  s  /\  ( F `  a )  =  r )  -> 
( ( F `  b ) R ( F `  a )  <-> 
s R r ) )
5251biimpcd 232 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( F `  b ) R ( F `  a )  ->  (
( ( F `  b )  =  s  /\  ( F `  a )  =  r )  ->  s R
r ) )
5350, 52syl6 34 . . . . . . . . . . . . . . . . . . . . 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 81 . . . . . . . . . . . . . . . . . . . 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 735 . . . . . . . . . . . . . . . . . . 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 435 . . . . . . . . . . . . . . . . . 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 5888 . . . . . . . . . . . . . . . . . . . 20  |-  ( b  =  a  ->  ( F `  b )  =  ( F `  a ) )
58 eqeq12 2475 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( F `  b
)  =  s  /\  ( F `  a )  =  r )  -> 
( ( F `  b )  =  ( F `  a )  <-> 
s  =  r ) )
5957, 58syl5ib 227 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( F `  b
)  =  s  /\  ( F `  a )  =  r )  -> 
( b  =  a  ->  s  =  r ) )
6059adantl 472 . . . . . . . . . . . . . . . . . 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 2462 . . . . . . . . . . . . . . . . . . . . . . . 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 8953 . . . . . . . . . . . . . . . . . . . . . . 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 726 . . . . . . . . . . . . . . . . . . . . . 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 4421 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( F `  a
)  =  r  /\  ( F `  b )  =  s )  -> 
( ( F `  a ) R ( F `  b )  <-> 
r R s ) )
6564ancoms 459 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( F `  b
)  =  s  /\  ( F `  a )  =  r )  -> 
( ( F `  a ) R ( F `  b )  <-> 
r R s ) )
6665biimpcd 232 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( F `  a ) R ( F `  b )  ->  (
( ( F `  b )  =  s  /\  ( F `  a )  =  r )  ->  r R
s ) )
6763, 66syl6 34 . . . . . . . . . . . . . . . . . . . . 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 81 . . . . . . . . . . . . . . . . . . . 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 736 . . . . . . . . . . . . . . . . . . 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 435 . . . . . . . . . . . . . . . . . 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 1356 . . . . . . . . . . . . . . . . 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 33 . . . . . . . . . . . . . . . 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 613 . . . . . . . . . . . . . . 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 89 . . . . . . . . . . . . . 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 66 . . . . . . . . . . . . 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 615 . . . . . . . . . . . 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 82 . . . . . . . . . . 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 435 . . . . . . . . . 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 29 . . . . . . . . 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 33 . . . . . . . 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 599 . . . . . . 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 1791 . . . . . 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 33 . . . . 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 2820 . . . 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 540 . 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 4775 . 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 235 1  |-  ( R  Po  A  ->  (
( ( w  We  A  /\  x  e.  On )  /\  A. y  e.  x  H  =/=  (/) )  ->  R  Or  ( F " x
) ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 189    /\ wa 375    \/ w3o 990    = wceq 1455   E.wex 1674    e. wcel 1898    =/= wne 2633   A.wral 2749   E.wrex 2750   {crab 2753   _Vcvv 3057    C_ wss 3416   (/)c0 3743   class class class wbr 4416    |-> cmpt 4475    Po wpo 4772    Or wor 4773    We wwe 4811   ran crn 4854   "cima 4856   Ord word 5441   Oncon0 5442   Fun wfun 5595    Fn wfn 5596   ` cfv 5601   iota_crio 6276  recscrecs 7115
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-rep 4529  ax-sep 4539  ax-nul 4548  ax-pow 4595  ax-pr 4653  ax-un 6610
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rex 2755  df-reu 2756  df-rmo 2757  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3744  df-if 3894  df-sn 3981  df-pr 3983  df-tp 3985  df-op 3987  df-uni 4213  df-iun 4294  df-br 4417  df-opab 4476  df-mpt 4477  df-tr 4512  df-eprel 4764  df-id 4768  df-po 4774  df-so 4775  df-fr 4812  df-we 4814  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-pred 5399  df-ord 5445  df-on 5446  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-riota 6277  df-wrecs 7054  df-recs 7116
This theorem is referenced by:  zorn2lem7  8958
  Copyright terms: Public domain W3C validator