Metamath Proof Explorer

Theorem zorn2lem6

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

Ref Expression
Hypotheses 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 zorn2lem6 
|- ( R Po A -> ( ( ( w We A /\ x e. On ) /\ A. y e. x H =/= (/) ) -> R Or ( F " x ) ) )

Proof

Step Hyp Ref Expression
1 zorn2lem.3 
 |-  F = recs ( ( f e. _V |-> ( iota_ v e. C A. u e. C -. u w v ) ) )
2 zorn2lem.4 
 |-  C = { z e. A | A. g e. ran f g R z }
3 zorn2lem.5 
 |-  D = { z e. A | A. g e. ( F " x ) g R z }
4 zorn2lem.7 
 |-  H = { z e. A | A. g e. ( F " y ) g R z }
5 poss 
 |-  ( ( F " x ) C_ A -> ( R Po A -> R Po ( F " x ) ) )
6 1 2 3 4 zorn2lem5 
 |-  ( ( ( w We A /\ x e. On ) /\ A. y e. x H =/= (/) ) -> ( F " x ) C_ A )
7 5 6 syl11 
 |-  ( R Po A -> ( ( ( w We A /\ x e. On ) /\ A. y e. x H =/= (/) ) -> R Po ( F " x ) ) )
8 1 tfr1 
 |-  F Fn On
9 fnfun 
 |-  ( F Fn On -> Fun F )
10 fvelima 
 |-  ( ( Fun F /\ s e. ( F " x ) ) -> E. b e. x ( F ` b ) = s )
11 df-rex 
 |-  ( E. b e. x ( F ` b ) = s <-> E. b ( b e. x /\ ( F ` b ) = s ) )
12 10 11 sylib 
 |-  ( ( Fun F /\ s e. ( F " x ) ) -> E. b ( b e. x /\ ( F ` b ) = s ) )
13 12 ex 
 |-  ( Fun F -> ( s e. ( F " x ) -> E. b ( b e. x /\ ( F ` b ) = s ) ) )
14 fvelima 
 |-  ( ( Fun F /\ r e. ( F " x ) ) -> E. a e. x ( F ` a ) = r )
15 df-rex 
 |-  ( E. a e. x ( F ` a ) = r <-> E. a ( a e. x /\ ( F ` a ) = r ) )
16 14 15 sylib 
 |-  ( ( Fun F /\ r e. ( F " x ) ) -> E. a ( a e. x /\ ( F ` a ) = r ) )
17 16 ex 
 |-  ( Fun F -> ( r e. ( F " x ) -> E. a ( a e. x /\ ( F ` a ) = r ) ) )
18 13 17 anim12d 
 |-  ( 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 ) ) ) )
19 8 9 18 mp2b 
 |-  ( ( s e. ( F " x ) /\ r e. ( F " x ) ) -> ( E. b ( b e. x /\ ( F ` b ) = s ) /\ E. a ( a e. x /\ ( F ` a ) = r ) ) )
20 an4 
 |-  ( ( ( b e. x /\ a e. x ) /\ ( ( F ` b ) = s /\ ( F ` a ) = r ) ) <-> ( ( b e. x /\ ( F ` b ) = s ) /\ ( a e. x /\ ( F ` a ) = r ) ) )
21 20 2exbii 
 |-  ( 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 ) ) )
22 exdistrv 
 |-  ( 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 ) ) )
23 21 22 bitri 
 |-  ( 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 ) ) )
24 19 23 sylibr 
 |-  ( ( s e. ( F " x ) /\ r e. ( F " x ) ) -> E. b E. a ( ( b e. x /\ a e. x ) /\ ( ( F ` b ) = s /\ ( F ` a ) = r ) ) )
25 4 neeq1i 
 |-  ( H =/= (/) <-> { z e. A | A. g e. ( F " y ) g R z } =/= (/) )
26 25 ralbii 
 |-  ( A. y e. x H =/= (/) <-> A. y e. x { z e. A | A. g e. ( F " y ) g R z } =/= (/) )
27 imaeq2 
 |-  ( y = b -> ( F " y ) = ( F " b ) )
28 27 raleqdv 
 |-  ( y = b -> ( A. g e. ( F " y ) g R z <-> A. g e. ( F " b ) g R z ) )
29 28 rabbidv 
 |-  ( y = b -> { z e. A | A. g e. ( F " y ) g R z } = { z e. A | A. g e. ( F " b ) g R z } )
30 29 neeq1d 
 |-  ( y = b -> ( { z e. A | A. g e. ( F " y ) g R z } =/= (/) <-> { z e. A | A. g e. ( F " b ) g R z } =/= (/) ) )
31 30 rspccv 
 |-  ( 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 } =/= (/) ) )
32 imaeq2 
 |-  ( y = a -> ( F " y ) = ( F " a ) )
33 32 raleqdv 
 |-  ( y = a -> ( A. g e. ( F " y ) g R z <-> A. g e. ( F " a ) g R z ) )
34 33 rabbidv 
 |-  ( y = a -> { z e. A | A. g e. ( F " y ) g R z } = { z e. A | A. g e. ( F " a ) g R z } )
35 34 neeq1d 
 |-  ( y = a -> ( { z e. A | A. g e. ( F " y ) g R z } =/= (/) <-> { z e. A | A. g e. ( F " a ) g R z } =/= (/) ) )
36 35 rspccv 
 |-  ( 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 } =/= (/) ) )
37 31 36 anim12d 
 |-  ( 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 } =/= (/) ) ) )
38 26 37 sylbi 
 |-  ( 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 } =/= (/) ) ) )
39 onelon 
 |-  ( ( x e. On /\ b e. x ) -> b e. On )
40 onelon 
 |-  ( ( x e. On /\ a e. x ) -> a e. On )
41 39 40 anim12dan 
 |-  ( ( x e. On /\ ( b e. x /\ a e. x ) ) -> ( b e. On /\ a e. On ) )
42 41 ex 
 |-  ( x e. On -> ( ( b e. x /\ a e. x ) -> ( b e. On /\ a e. On ) ) )
43 eloni 
 |-  ( b e. On -> Ord b )
44 eloni 
 |-  ( a e. On -> Ord a )
45 ordtri3or 
 |-  ( ( Ord b /\ Ord a ) -> ( b e. a \/ b = a \/ a e. b ) )
46 43 44 45 syl2an 
 |-  ( ( b e. On /\ a e. On ) -> ( b e. a \/ b = a \/ a e. b ) )
47 eqid 
 |-  { z e. A | A. g e. ( F " a ) g R z } = { z e. A | A. g e. ( F " a ) g R z }
48 1 2 47 zorn2lem2 
 |-  ( ( 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 ) ) )
49 48 adantll 
 |-  ( ( ( 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 ) ) )
50 breq12 
 |-  ( ( ( F ` b ) = s /\ ( F ` a ) = r ) -> ( ( F ` b ) R ( F ` a ) <-> s R r ) )
51 50 biimpcd 
 |-  ( ( F ` b ) R ( F ` a ) -> ( ( ( F ` b ) = s /\ ( F ` a ) = r ) -> s R r ) )
52 49 51 syl6 
 |-  ( ( ( 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 ) ) )
53 52 com23 
 |-  ( ( ( 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 ) ) )
54 53 adantrrl 
 |-  ( ( ( 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 ) ) )
55 54 imp 
 |-  ( ( ( ( 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 ) )
56 fveq2 
 |-  ( b = a -> ( F ` b ) = ( F ` a ) )
57 eqeq12 
 |-  ( ( ( F ` b ) = s /\ ( F ` a ) = r ) -> ( ( F ` b ) = ( F ` a ) <-> s = r ) )
58 56 57 imbitrid 
 |-  ( ( ( F ` b ) = s /\ ( F ` a ) = r ) -> ( b = a -> s = r ) )
59 58 adantl 
 |-  ( ( ( ( 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 ) )
60 eqid 
 |-  { z e. A | A. g e. ( F " b ) g R z } = { z e. A | A. g e. ( F " b ) g R z }
61 1 2 60 zorn2lem2 
 |-  ( ( 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 ) ) )
62 61 adantlr 
 |-  ( ( ( 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 ) ) )
63 breq12 
 |-  ( ( ( F ` a ) = r /\ ( F ` b ) = s ) -> ( ( F ` a ) R ( F ` b ) <-> r R s ) )
64 63 ancoms 
 |-  ( ( ( F ` b ) = s /\ ( F ` a ) = r ) -> ( ( F ` a ) R ( F ` b ) <-> r R s ) )
65 64 biimpcd 
 |-  ( ( F ` a ) R ( F ` b ) -> ( ( ( F ` b ) = s /\ ( F ` a ) = r ) -> r R s ) )
66 62 65 syl6 
 |-  ( ( ( 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 ) ) )
67 66 com23 
 |-  ( ( ( 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 ) ) )
68 67 adantrrr 
 |-  ( ( ( 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 ) ) )
69 68 imp 
 |-  ( ( ( ( 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 ) )
70 55 59 69 3orim123d 
 |-  ( ( ( ( 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 ) ) )
71 46 70 syl5 
 |-  ( ( ( ( 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 ) ) )
72 71 exp31 
 |-  ( ( 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 ) ) ) ) )
73 72 com4r 
 |-  ( ( 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 ) ) ) ) )
74 42 42 73 syl6c 
 |-  ( 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 ) ) ) ) )
75 74 exp4a 
 |-  ( 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 ) ) ) ) ) )
76 75 com3r 
 |-  ( 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 ) ) ) ) ) )
77 76 imp 
 |-  ( ( 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 ) ) ) ) )
78 77 a2d 
 |-  ( ( 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 ) ) ) ) )
79 38 78 syl5 
 |-  ( ( 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 ) ) ) ) )
80 79 imp4b 
 |-  ( ( ( 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 ) ) )
81 80 exlimdvv 
 |-  ( ( ( 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 ) ) )
82 24 81 syl5 
 |-  ( ( ( 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 ) ) )
83 82 ralrimivv 
 |-  ( ( ( 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 ) )
84 7 83 jca2 
 |-  ( 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 ) ) ) )
85 df-so 
 |-  ( 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 ) ) )
86 84 85 imbitrrdi 
 |-  ( R Po A -> ( ( ( w We A /\ x e. On ) /\ A. y e. x H =/= (/) ) -> R Or ( F " x ) ) )