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

Theorem zorn2lem6 8771
Description: Lemma for zorn2 8776. (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 8770 . . . . 5  |-  ( ( ( w  We  A  /\  x  e.  On )  /\  A. y  e.  x  H  =/=  (/) )  -> 
( F " x
)  C_  A )
6 poss 4741 . . . . 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 31 . . 3  |-  ( R  Po  A  ->  (
( ( w  We  A  /\  x  e.  On )  /\  A. y  e.  x  H  =/=  (/) )  ->  R  Po  ( F " x
) ) )
91tfr1 6956 . . . . . . . 8  |-  F  Fn  On
10 fnfun 5606 . . . . . . . 8  |-  ( F  Fn  On  ->  Fun  F )
11 fvelima 5842 . . . . . . . . . . 11  |-  ( ( Fun  F  /\  s  e.  ( F " x
) )  ->  E. b  e.  x  ( F `  b )  =  s )
12 df-rex 2801 . . . . . . . . . . 11  |-  ( E. b  e.  x  ( F `  b )  =  s  <->  E. b
( b  e.  x  /\  ( F `  b
)  =  s ) )
1311, 12sylib 196 . . . . . . . . . 10  |-  ( ( Fun  F  /\  s  e.  ( F " x
) )  ->  E. b
( b  e.  x  /\  ( F `  b
)  =  s ) )
1413ex 434 . . . . . . . . 9  |-  ( Fun 
F  ->  ( s  e.  ( F " x
)  ->  E. b
( b  e.  x  /\  ( F `  b
)  =  s ) ) )
15 fvelima 5842 . . . . . . . . . . 11  |-  ( ( Fun  F  /\  r  e.  ( F " x
) )  ->  E. a  e.  x  ( F `  a )  =  r )
16 df-rex 2801 . . . . . . . . . . 11  |-  ( E. a  e.  x  ( F `  a )  =  r  <->  E. a
( a  e.  x  /\  ( F `  a
)  =  r ) )
1715, 16sylib 196 . . . . . . . . . 10  |-  ( ( Fun  F  /\  r  e.  ( F " x
) )  ->  E. a
( a  e.  x  /\  ( F `  a
)  =  r ) )
1817ex 434 . . . . . . . . 9  |-  ( Fun 
F  ->  ( r  e.  ( F " x
)  ->  E. a
( a  e.  x  /\  ( F `  a
)  =  r ) ) )
1914, 18anim12d 563 . . . . . . . 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 820 . . . . . . . . 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 1636 . . . . . . . 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 1941 . . . . . . . 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 249 . . . . . . 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 212 . . . . . 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 2733 . . . . . . . . . . 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 5263 . . . . . . . . . . . . . . 15  |-  ( y  =  b  ->  ( F " y )  =  ( F " b
) )
2928raleqdv 3019 . . . . . . . . . . . . . 14  |-  ( y  =  b  ->  ( A. g  e.  ( F " y ) g R z  <->  A. g  e.  ( F " b
) g R z ) )
3029rabbidv 3060 . . . . . . . . . . . . 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 2725 . . . . . . . . . . . 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 3166 . . . . . . . . . . 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 5263 . . . . . . . . . . . . . . 15  |-  ( y  =  a  ->  ( F " y )  =  ( F " a
) )
3433raleqdv 3019 . . . . . . . . . . . . . 14  |-  ( y  =  a  ->  ( A. g  e.  ( F " y ) g R z  <->  A. g  e.  ( F " a
) g R z ) )
3534rabbidv 3060 . . . . . . . . . . . . 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 2725 . . . . . . . . . . . 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 3166 . . . . . . . . . . 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 563 . . . . . . . . . 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 195 . . . . . . . . 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 4842 . . . . . . . . . . . . . . . 16  |-  ( ( x  e.  On  /\  b  e.  x )  ->  b  e.  On )
41 onelon 4842 . . . . . . . . . . . . . . . 16  |-  ( ( x  e.  On  /\  a  e.  x )  ->  a  e.  On )
4240, 41anim12dan 833 . . . . . . . . . . . . . . 15  |-  ( ( x  e.  On  /\  ( b  e.  x  /\  a  e.  x
) )  ->  (
b  e.  On  /\  a  e.  On )
)
4342ex 434 . . . . . . . . . . . . . 14  |-  ( x  e.  On  ->  (
( b  e.  x  /\  a  e.  x
)  ->  ( b  e.  On  /\  a  e.  On ) ) )
44 eloni 4827 . . . . . . . . . . . . . . . . . 18  |-  ( b  e.  On  ->  Ord  b )
45 eloni 4827 . . . . . . . . . . . . . . . . . 18  |-  ( a  e.  On  ->  Ord  a )
46 ordtri3or 4849 . . . . . . . . . . . . . . . . . 18  |-  ( ( Ord  b  /\  Ord  a )  ->  (
b  e.  a  \/  b  =  a  \/  a  e.  b ) )
4744, 45, 46syl2an 477 . . . . . . . . . . . . . . . . 17  |-  ( ( b  e.  On  /\  a  e.  On )  ->  ( b  e.  a  \/  b  =  a  \/  a  e.  b ) )
48 eqid 2451 . . . . . . . . . . . . . . . . . . . . . . . 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 8767 . . . . . . . . . . . . . . . . . . . . . . 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 713 . . . . . . . . . . . . . . . . . . . . . 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 4395 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( F `  b
)  =  s  /\  ( F `  a )  =  r )  -> 
( ( F `  b ) R ( F `  a )  <-> 
s R r ) )
5251biimpcd 224 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( F `  b ) R ( F `  a )  ->  (
( ( F `  b )  =  s  /\  ( F `  a )  =  r )  ->  s R
r ) )
5350, 52syl6 33 . . . . . . . . . . . . . . . . . . . . 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 78 . . . . . . . . . . . . . . . . . . . 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 723 . . . . . . . . . . . . . . . . . . 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 429 . . . . . . . . . . . . . . . . . 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 5789 . . . . . . . . . . . . . . . . . . . 20  |-  ( b  =  a  ->  ( F `  b )  =  ( F `  a ) )
58 eqeq12 2470 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( F `  b
)  =  s  /\  ( F `  a )  =  r )  -> 
( ( F `  b )  =  ( F `  a )  <-> 
s  =  r ) )
5957, 58syl5ib 219 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( F `  b
)  =  s  /\  ( F `  a )  =  r )  -> 
( b  =  a  ->  s  =  r ) )
6059adantl 466 . . . . . . . . . . . . . . . . . 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 2451 . . . . . . . . . . . . . . . . . . . . . . . 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 8767 . . . . . . . . . . . . . . . . . . . . . . 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 714 . . . . . . . . . . . . . . . . . . . . . 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 4395 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( F `  a
)  =  r  /\  ( F `  b )  =  s )  -> 
( ( F `  a ) R ( F `  b )  <-> 
r R s ) )
6564ancoms 453 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( F `  b
)  =  s  /\  ( F `  a )  =  r )  -> 
( ( F `  a ) R ( F `  b )  <-> 
r R s ) )
6665biimpcd 224 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( F `  a ) R ( F `  b )  ->  (
( ( F `  b )  =  s  /\  ( F `  a )  =  r )  ->  r R
s ) )
6763, 66syl6 33 . . . . . . . . . . . . . . . . . . . . 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 78 . . . . . . . . . . . . . . . . . . . 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 724 . . . . . . . . . . . . . . . . . . 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 429 . . . . . . . . . . . . . . . . . 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 1298 . . . . . . . . . . . . . . . . 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 32 . . . . . . . . . . . . . . . 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 604 . . . . . . . . . . . . . . 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 86 . . . . . . . . . . . . . 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 64 . . . . . . . . . . . . 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 606 . . . . . . . . . . . 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 79 . . . . . . . . . . 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 429 . . . . . . . . . 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 26 . . . . . . . . 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 32 . . . . . . . 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 590 . . . . . . 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 1692 . . . . . 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 32 . . . . 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 2903 . . . 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 533 . 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 4740 . 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 227 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 184    /\ wa 369    \/ w3o 964    = wceq 1370   E.wex 1587    e. wcel 1758    =/= wne 2644   A.wral 2795   E.wrex 2796   {crab 2799   _Vcvv 3068    C_ wss 3426   (/)c0 3735   class class class wbr 4390    |-> cmpt 4448    Po wpo 4737    Or wor 4738    We wwe 4776   Ord word 4816   Oncon0 4817   ran crn 4939   "cima 4941   Fun wfun 5510    Fn wfn 5511   ` cfv 5516   iota_crio 6150  recscrecs 6931
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-rep 4501  ax-sep 4511  ax-nul 4519  ax-pow 4568  ax-pr 4629  ax-un 6472
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-ral 2800  df-rex 2801  df-reu 2802  df-rmo 2803  df-rab 2804  df-v 3070  df-sbc 3285  df-csb 3387  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-pss 3442  df-nul 3736  df-if 3890  df-sn 3976  df-pr 3978  df-tp 3980  df-op 3982  df-uni 4190  df-iun 4271  df-br 4391  df-opab 4449  df-mpt 4450  df-tr 4484  df-eprel 4730  df-id 4734  df-po 4739  df-so 4740  df-fr 4777  df-we 4779  df-ord 4820  df-on 4821  df-suc 4823  df-xp 4944  df-rel 4945  df-cnv 4946  df-co 4947  df-dm 4948  df-rn 4949  df-res 4950  df-ima 4951  df-iota 5479  df-fun 5518  df-fn 5519  df-f 5520  df-f1 5521  df-fo 5522  df-f1o 5523  df-fv 5524  df-riota 6151  df-recs 6932
This theorem is referenced by:  zorn2lem7  8772
  Copyright terms: Public domain W3C validator