Metamath Proof Explorer

Theorem zorn2lem7

Description: Lemma for zorn2 . (Contributed by NM, 6-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 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 )

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 ween 
 |-  ( A e. dom card <-> E. w w We A )
6 1 2 3 zorn2lem4 
 |-  ( ( R Po A /\ w We A ) -> E. x e. On D = (/) )
7 imaeq2 
 |-  ( x = y -> ( F " x ) = ( F " y ) )
8 7 raleqdv 
 |-  ( x = y -> ( A. g e. ( F " x ) g R z <-> A. g e. ( F " y ) g R z ) )
9 8 rabbidv 
 |-  ( x = y -> { z e. A | A. g e. ( F " x ) g R z } = { z e. A | A. g e. ( F " y ) g R z } )
10 9 3 4 3eqtr4g 
 |-  ( x = y -> D = H )
11 10 eqeq1d 
 |-  ( x = y -> ( D = (/) <-> H = (/) ) )
12 11 onminex 
 |-  ( E. x e. On D = (/) -> E. x e. On ( D = (/) /\ A. y e. x -. H = (/) ) )
13 df-ne 
 |-  ( H =/= (/) <-> -. H = (/) )
14 13 ralbii 
 |-  ( A. y e. x H =/= (/) <-> A. y e. x -. H = (/) )
15 14 anbi2i 
 |-  ( ( D = (/) /\ A. y e. x H =/= (/) ) <-> ( D = (/) /\ A. y e. x -. H = (/) ) )
16 15 rexbii 
 |-  ( E. x e. On ( D = (/) /\ A. y e. x H =/= (/) ) <-> E. x e. On ( D = (/) /\ A. y e. x -. H = (/) ) )
17 12 16 sylibr 
 |-  ( E. x e. On D = (/) -> E. x e. On ( D = (/) /\ A. y e. x H =/= (/) ) )
18 1 2 3 4 zorn2lem5 
 |-  ( ( ( w We A /\ x e. On ) /\ A. y e. x H =/= (/) ) -> ( F " x ) C_ A )
19 18 a1i 
 |-  ( R Po A -> ( ( ( w We A /\ x e. On ) /\ A. y e. x H =/= (/) ) -> ( F " x ) C_ A ) )
20 1 2 3 4 zorn2lem6 
 |-  ( R Po A -> ( ( ( w We A /\ x e. On ) /\ A. y e. x H =/= (/) ) -> R Or ( F " x ) ) )
21 19 20 jcad 
 |-  ( R Po A -> ( ( ( w We A /\ x e. On ) /\ A. y e. x H =/= (/) ) -> ( ( F " x ) C_ A /\ R Or ( F " x ) ) ) )
22 1 tfr1 
 |-  F Fn On
23 fnfun 
 |-  ( F Fn On -> Fun F )
24 vex 
 |-  x e. _V
25 24 funimaex 
 |-  ( Fun F -> ( F " x ) e. _V )
26 22 23 25 mp2b 
 |-  ( F " x ) e. _V
27 sseq1 
 |-  ( s = ( F " x ) -> ( s C_ A <-> ( F " x ) C_ A ) )
28 soeq2 
 |-  ( s = ( F " x ) -> ( R Or s <-> R Or ( F " x ) ) )
29 27 28 anbi12d 
 |-  ( s = ( F " x ) -> ( ( s C_ A /\ R Or s ) <-> ( ( F " x ) C_ A /\ R Or ( F " x ) ) ) )
30 raleq 
 |-  ( s = ( F " x ) -> ( A. r e. s ( r R a \/ r = a ) <-> A. r e. ( F " x ) ( r R a \/ r = a ) ) )
31 30 rexbidv 
 |-  ( 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 ) ) )
32 29 31 imbi12d 
 |-  ( 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 ) ) ) )
33 26 32 spcv 
 |-  ( 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 ) ) )
34 21 33 sylan9 
 |-  ( ( 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 ) ) )
35 34 adantld 
 |-  ( ( 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 ) ) )
36 35 imp 
 |-  ( ( ( 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 
 |-  -. b e. (/)
38 18 sseld 
 |-  ( ( ( w We A /\ x e. On ) /\ A. y e. x H =/= (/) ) -> ( r e. ( F " x ) -> r e. A ) )
39 3anass 
 |-  ( ( r e. A /\ a e. A /\ b e. A ) <-> ( r e. A /\ ( a e. A /\ b e. A ) ) )
40 potr 
 |-  ( ( R Po A /\ ( r e. A /\ a e. A /\ b e. A ) ) -> ( ( r R a /\ a R b ) -> r R b ) )
41 39 40 sylan2br 
 |-  ( ( R Po A /\ ( r e. A /\ ( a e. A /\ b e. A ) ) ) -> ( ( r R a /\ a R b ) -> r R b ) )
42 41 expcomd 
 |-  ( ( R Po A /\ ( r e. A /\ ( a e. A /\ b e. A ) ) ) -> ( a R b -> ( r R a -> r R b ) ) )
43 42 imp 
 |-  ( ( ( R Po A /\ ( r e. A /\ ( a e. A /\ b e. A ) ) ) /\ a R b ) -> ( r R a -> r R b ) )
44 breq1 
 |-  ( r = a -> ( r R b <-> a R b ) )
45 44 biimprcd 
 |-  ( a R b -> ( r = a -> r R b ) )
46 45 adantl 
 |-  ( ( ( R Po A /\ ( r e. A /\ ( a e. A /\ b e. A ) ) ) /\ a R b ) -> ( r = a -> r R b ) )
47 43 46 jaod 
 |-  ( ( ( R Po A /\ ( r e. A /\ ( a e. A /\ b e. A ) ) ) /\ a R b ) -> ( ( r R a \/ r = a ) -> r R b ) )
48 47 exp42 
 |-  ( R Po A -> ( r e. A -> ( ( a e. A /\ b e. A ) -> ( a R b -> ( ( r R a \/ r = a ) -> r R b ) ) ) ) )
49 38 48 sylan9r 
 |-  ( ( 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 ) ) ) ) )
50 49 com24 
 |-  ( ( 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 ) ) ) ) )
51 50 com23 
 |-  ( ( 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 ) ) ) ) )
52 51 imp31 
 |-  ( ( ( ( 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 ) ) )
53 52 a2d 
 |-  ( ( ( ( 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 ) ) )
54 53 ralimdv2 
 |-  ( ( ( ( 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 
 |-  ( r = g -> ( r R b <-> g R b ) )
56 55 cbvralvw 
 |-  ( A. r e. ( F " x ) r R b <-> A. g e. ( F " x ) g R b )
57 breq2 
 |-  ( z = b -> ( g R z <-> g R b ) )
58 57 ralbidv 
 |-  ( z = b -> ( A. g e. ( F " x ) g R z <-> A. g e. ( F " x ) g R b ) )
59 58 elrab 
 |-  ( b e. { z e. A | A. g e. ( F " x ) g R z } <-> ( b e. A /\ A. g e. ( F " x ) g R b ) )
60 3 eqeq1i 
 |-  ( D = (/) <-> { z e. A | A. g e. ( F " x ) g R z } = (/) )
61 eleq2 
 |-  ( { 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. (/) ) )
62 60 61 sylbi 
 |-  ( D = (/) -> ( b e. { z e. A | A. g e. ( F " x ) g R z } <-> b e. (/) ) )
63 59 62 bitr3id 
 |-  ( D = (/) -> ( ( b e. A /\ A. g e. ( F " x ) g R b ) <-> b e. (/) ) )
64 63 biimpd 
 |-  ( D = (/) -> ( ( b e. A /\ A. g e. ( F " x ) g R b ) -> b e. (/) ) )
65 64 expdimp 
 |-  ( ( D = (/) /\ b e. A ) -> ( A. g e. ( F " x ) g R b -> b e. (/) ) )
66 56 65 syl5bi 
 |-  ( ( D = (/) /\ b e. A ) -> ( A. r e. ( F " x ) r R b -> b e. (/) ) )
67 54 66 sylan9r 
 |-  ( ( ( 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. (/) ) )
68 67 exp32 
 |-  ( ( 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. (/) ) ) ) )
69 68 com34 
 |-  ( ( 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. (/) ) ) ) )
70 69 imp31 
 |-  ( ( ( ( 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. (/) ) )
71 37 70 mtoi 
 |-  ( ( ( ( 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 )
72 71 exp42 
 |-  ( ( 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 ) ) ) )
73 72 exp4a 
 |-  ( ( 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 ) ) ) ) )
74 73 com34 
 |-  ( ( 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 ) ) ) ) )
75 74 ex 
 |-  ( 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 ) ) ) ) ) )
76 75 com4r 
 |-  ( 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 ) ) ) ) ) )
77 76 pm2.43a 
 |-  ( 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 ) ) ) ) )
78 77 impd 
 |-  ( 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 ) ) ) )
79 78 com4l 
 |-  ( ( 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 ) ) ) )
80 79 impd 
 |-  ( ( 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 ) ) )
81 80 ralrimdv 
 |-  ( ( 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 ) )
82 81 expd 
 |-  ( ( 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 ) ) )
83 82 reximdvai 
 |-  ( ( 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 ) )
84 83 exp32 
 |-  ( 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 ) ) ) )
85 84 com12 
 |-  ( 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 ) ) ) )
86 85 adantr 
 |-  ( ( 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 ) ) ) )
87 86 imp32 
 |-  ( ( ( 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 ) )
88 36 87 mpd 
 |-  ( ( ( 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 )
89 88 exp45 
 |-  ( ( 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 ) ) ) )
90 89 com23 
 |-  ( ( 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 ) ) ) )
91 90 expdimp 
 |-  ( ( ( 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 ) ) ) )
92 91 imp4a 
 |-  ( ( ( 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 ) ) )
93 92 com3l 
 |-  ( 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 ) ) )
94 93 rexlimiv 
 |-  ( 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 ) )
95 6 17 94 3syl 
 |-  ( ( 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 ) )
96 95 adantlr 
 |-  ( ( ( 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 ) )
97 96 pm2.43i 
 |-  ( ( ( 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 )
98 97 expcom 
 |-  ( 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 ) )
99 98 exlimiv 
 |-  ( 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 ) )
100 5 99 sylbi 
 |-  ( 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 ) )
101 100 3impib 
 |-  ( ( 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 )