Metamath Proof Explorer

Theorem zornn0g

Description: Variant of Zorn's lemma zorng in which (/) , the union of the empty chain, is not required to be an element of A . (Contributed by Jeff Madsen, 5-Jan-2011) (Revised by Mario Carneiro, 9-May-2015)

Ref Expression
Assertion zornn0g 
|- ( ( A e. dom card /\ A =/= (/) /\ A. z ( ( z C_ A /\ z =/= (/) /\ [C.] Or z ) -> U. z e. A ) ) -> E. x e. A A. y e. A -. x C. y )

Proof

Step Hyp Ref Expression
1 simp2 
 |-  ( ( A e. dom card /\ A =/= (/) /\ A. z ( ( z C_ A /\ z =/= (/) /\ [C.] Or z ) -> U. z e. A ) ) -> A =/= (/) )
2 simp1 
 |-  ( ( A e. dom card /\ A =/= (/) /\ A. z ( ( z C_ A /\ z =/= (/) /\ [C.] Or z ) -> U. z e. A ) ) -> A e. dom card )
3 snfi 
 |-  { (/) } e. Fin
4 finnum 
 |-  ( { (/) } e. Fin -> { (/) } e. dom card )
5 3 4 ax-mp 
 |-  { (/) } e. dom card
6 unnum 
 |-  ( ( A e. dom card /\ { (/) } e. dom card ) -> ( A u. { (/) } ) e. dom card )
7 2 5 6 sylancl 
 |-  ( ( A e. dom card /\ A =/= (/) /\ A. z ( ( z C_ A /\ z =/= (/) /\ [C.] Or z ) -> U. z e. A ) ) -> ( A u. { (/) } ) e. dom card )
8 uncom 
 |-  ( A u. { (/) } ) = ( { (/) } u. A )
9 8 sseq2i 
 |-  ( w C_ ( A u. { (/) } ) <-> w C_ ( { (/) } u. A ) )
10 ssundif 
 |-  ( w C_ ( { (/) } u. A ) <-> ( w \ { (/) } ) C_ A )
11 9 10 bitri 
 |-  ( w C_ ( A u. { (/) } ) <-> ( w \ { (/) } ) C_ A )
12 difss 
 |-  ( w \ { (/) } ) C_ w
13 soss 
 |-  ( ( w \ { (/) } ) C_ w -> ( [C.] Or w -> [C.] Or ( w \ { (/) } ) ) )
14 12 13 ax-mp 
 |-  ( [C.] Or w -> [C.] Or ( w \ { (/) } ) )
15 ssdif0 
 |-  ( w C_ { (/) } <-> ( w \ { (/) } ) = (/) )
16 uni0b 
 |-  ( U. w = (/) <-> w C_ { (/) } )
17 16 biimpri 
 |-  ( w C_ { (/) } -> U. w = (/) )
18 17 eleq1d 
 |-  ( w C_ { (/) } -> ( U. w e. ( A u. { (/) } ) <-> (/) e. ( A u. { (/) } ) ) )
19 15 18 sylbir 
 |-  ( ( w \ { (/) } ) = (/) -> ( U. w e. ( A u. { (/) } ) <-> (/) e. ( A u. { (/) } ) ) )
20 19 imbi2d 
 |-  ( ( w \ { (/) } ) = (/) -> ( ( A. z ( ( z C_ A /\ z =/= (/) /\ [C.] Or z ) -> U. z e. A ) -> U. w e. ( A u. { (/) } ) ) <-> ( A. z ( ( z C_ A /\ z =/= (/) /\ [C.] Or z ) -> U. z e. A ) -> (/) e. ( A u. { (/) } ) ) ) )
21 vex 
 |-  w e. _V
22 21 difexi 
 |-  ( w \ { (/) } ) e. _V
23 sseq1 
 |-  ( z = ( w \ { (/) } ) -> ( z C_ A <-> ( w \ { (/) } ) C_ A ) )
24 neeq1 
 |-  ( z = ( w \ { (/) } ) -> ( z =/= (/) <-> ( w \ { (/) } ) =/= (/) ) )
25 soeq2 
 |-  ( z = ( w \ { (/) } ) -> ( [C.] Or z <-> [C.] Or ( w \ { (/) } ) ) )
26 23 24 25 3anbi123d 
 |-  ( z = ( w \ { (/) } ) -> ( ( z C_ A /\ z =/= (/) /\ [C.] Or z ) <-> ( ( w \ { (/) } ) C_ A /\ ( w \ { (/) } ) =/= (/) /\ [C.] Or ( w \ { (/) } ) ) ) )
27 unieq 
 |-  ( z = ( w \ { (/) } ) -> U. z = U. ( w \ { (/) } ) )
28 27 eleq1d 
 |-  ( z = ( w \ { (/) } ) -> ( U. z e. A <-> U. ( w \ { (/) } ) e. A ) )
29 26 28 imbi12d 
 |-  ( z = ( w \ { (/) } ) -> ( ( ( z C_ A /\ z =/= (/) /\ [C.] Or z ) -> U. z e. A ) <-> ( ( ( w \ { (/) } ) C_ A /\ ( w \ { (/) } ) =/= (/) /\ [C.] Or ( w \ { (/) } ) ) -> U. ( w \ { (/) } ) e. A ) ) )
30 22 29 spcv 
 |-  ( A. z ( ( z C_ A /\ z =/= (/) /\ [C.] Or z ) -> U. z e. A ) -> ( ( ( w \ { (/) } ) C_ A /\ ( w \ { (/) } ) =/= (/) /\ [C.] Or ( w \ { (/) } ) ) -> U. ( w \ { (/) } ) e. A ) )
31 30 com12 
 |-  ( ( ( w \ { (/) } ) C_ A /\ ( w \ { (/) } ) =/= (/) /\ [C.] Or ( w \ { (/) } ) ) -> ( A. z ( ( z C_ A /\ z =/= (/) /\ [C.] Or z ) -> U. z e. A ) -> U. ( w \ { (/) } ) e. A ) )
32 31 3expa 
 |-  ( ( ( ( w \ { (/) } ) C_ A /\ ( w \ { (/) } ) =/= (/) ) /\ [C.] Or ( w \ { (/) } ) ) -> ( A. z ( ( z C_ A /\ z =/= (/) /\ [C.] Or z ) -> U. z e. A ) -> U. ( w \ { (/) } ) e. A ) )
33 32 an32s 
 |-  ( ( ( ( w \ { (/) } ) C_ A /\ [C.] Or ( w \ { (/) } ) ) /\ ( w \ { (/) } ) =/= (/) ) -> ( A. z ( ( z C_ A /\ z =/= (/) /\ [C.] Or z ) -> U. z e. A ) -> U. ( w \ { (/) } ) e. A ) )
34 unidif0 
 |-  U. ( w \ { (/) } ) = U. w
35 34 eleq1i 
 |-  ( U. ( w \ { (/) } ) e. A <-> U. w e. A )
36 elun1 
 |-  ( U. w e. A -> U. w e. ( A u. { (/) } ) )
37 35 36 sylbi 
 |-  ( U. ( w \ { (/) } ) e. A -> U. w e. ( A u. { (/) } ) )
38 33 37 syl6 
 |-  ( ( ( ( w \ { (/) } ) C_ A /\ [C.] Or ( w \ { (/) } ) ) /\ ( w \ { (/) } ) =/= (/) ) -> ( A. z ( ( z C_ A /\ z =/= (/) /\ [C.] Or z ) -> U. z e. A ) -> U. w e. ( A u. { (/) } ) ) )
39 0ex 
 |-  (/) e. _V
40 39 snid 
 |-  (/) e. { (/) }
41 elun2 
 |-  ( (/) e. { (/) } -> (/) e. ( A u. { (/) } ) )
42 40 41 ax-mp 
 |-  (/) e. ( A u. { (/) } )
43 42 2a1i 
 |-  ( ( ( w \ { (/) } ) C_ A /\ [C.] Or ( w \ { (/) } ) ) -> ( A. z ( ( z C_ A /\ z =/= (/) /\ [C.] Or z ) -> U. z e. A ) -> (/) e. ( A u. { (/) } ) ) )
44 20 38 43 pm2.61ne 
 |-  ( ( ( w \ { (/) } ) C_ A /\ [C.] Or ( w \ { (/) } ) ) -> ( A. z ( ( z C_ A /\ z =/= (/) /\ [C.] Or z ) -> U. z e. A ) -> U. w e. ( A u. { (/) } ) ) )
45 14 44 sylan2 
 |-  ( ( ( w \ { (/) } ) C_ A /\ [C.] Or w ) -> ( A. z ( ( z C_ A /\ z =/= (/) /\ [C.] Or z ) -> U. z e. A ) -> U. w e. ( A u. { (/) } ) ) )
46 11 45 sylanb 
 |-  ( ( w C_ ( A u. { (/) } ) /\ [C.] Or w ) -> ( A. z ( ( z C_ A /\ z =/= (/) /\ [C.] Or z ) -> U. z e. A ) -> U. w e. ( A u. { (/) } ) ) )
47 46 com12 
 |-  ( A. z ( ( z C_ A /\ z =/= (/) /\ [C.] Or z ) -> U. z e. A ) -> ( ( w C_ ( A u. { (/) } ) /\ [C.] Or w ) -> U. w e. ( A u. { (/) } ) ) )
48 47 alrimiv 
 |-  ( A. z ( ( z C_ A /\ z =/= (/) /\ [C.] Or z ) -> U. z e. A ) -> A. w ( ( w C_ ( A u. { (/) } ) /\ [C.] Or w ) -> U. w e. ( A u. { (/) } ) ) )
49 48 3ad2ant3 
 |-  ( ( A e. dom card /\ A =/= (/) /\ A. z ( ( z C_ A /\ z =/= (/) /\ [C.] Or z ) -> U. z e. A ) ) -> A. w ( ( w C_ ( A u. { (/) } ) /\ [C.] Or w ) -> U. w e. ( A u. { (/) } ) ) )
50 zorng 
 |-  ( ( ( A u. { (/) } ) e. dom card /\ A. w ( ( w C_ ( A u. { (/) } ) /\ [C.] Or w ) -> U. w e. ( A u. { (/) } ) ) ) -> E. x e. ( A u. { (/) } ) A. y e. ( A u. { (/) } ) -. x C. y )
51 7 49 50 syl2anc 
 |-  ( ( A e. dom card /\ A =/= (/) /\ A. z ( ( z C_ A /\ z =/= (/) /\ [C.] Or z ) -> U. z e. A ) ) -> E. x e. ( A u. { (/) } ) A. y e. ( A u. { (/) } ) -. x C. y )
52 ssun1 
 |-  A C_ ( A u. { (/) } )
53 ssralv 
 |-  ( A C_ ( A u. { (/) } ) -> ( A. y e. ( A u. { (/) } ) -. x C. y -> A. y e. A -. x C. y ) )
54 52 53 ax-mp 
 |-  ( A. y e. ( A u. { (/) } ) -. x C. y -> A. y e. A -. x C. y )
55 54 reximi 
 |-  ( E. x e. ( A u. { (/) } ) A. y e. ( A u. { (/) } ) -. x C. y -> E. x e. ( A u. { (/) } ) A. y e. A -. x C. y )
56 rexun 
 |-  ( E. x e. ( A u. { (/) } ) A. y e. A -. x C. y <-> ( E. x e. A A. y e. A -. x C. y \/ E. x e. { (/) } A. y e. A -. x C. y ) )
57 simpr 
 |-  ( ( A =/= (/) /\ E. x e. A A. y e. A -. x C. y ) -> E. x e. A A. y e. A -. x C. y )
58 simpr 
 |-  ( ( A =/= (/) /\ E. x e. { (/) } A. y e. A -. x C. y ) -> E. x e. { (/) } A. y e. A -. x C. y )
59 psseq1 
 |-  ( x = (/) -> ( x C. y <-> (/) C. y ) )
60 0pss 
 |-  ( (/) C. y <-> y =/= (/) )
61 59 60 bitrdi 
 |-  ( x = (/) -> ( x C. y <-> y =/= (/) ) )
62 61 notbid 
 |-  ( x = (/) -> ( -. x C. y <-> -. y =/= (/) ) )
63 nne 
 |-  ( -. y =/= (/) <-> y = (/) )
64 62 63 bitrdi 
 |-  ( x = (/) -> ( -. x C. y <-> y = (/) ) )
65 64 ralbidv 
 |-  ( x = (/) -> ( A. y e. A -. x C. y <-> A. y e. A y = (/) ) )
66 39 65 rexsn 
 |-  ( E. x e. { (/) } A. y e. A -. x C. y <-> A. y e. A y = (/) )
67 eqsn 
 |-  ( A =/= (/) -> ( A = { (/) } <-> A. y e. A y = (/) ) )
68 67 biimpar 
 |-  ( ( A =/= (/) /\ A. y e. A y = (/) ) -> A = { (/) } )
69 66 68 sylan2b 
 |-  ( ( A =/= (/) /\ E. x e. { (/) } A. y e. A -. x C. y ) -> A = { (/) } )
70 58 69 rexeqtrrdv 
 |-  ( ( A =/= (/) /\ E. x e. { (/) } A. y e. A -. x C. y ) -> E. x e. A A. y e. A -. x C. y )
71 57 70 jaodan 
 |-  ( ( A =/= (/) /\ ( E. x e. A A. y e. A -. x C. y \/ E. x e. { (/) } A. y e. A -. x C. y ) ) -> E. x e. A A. y e. A -. x C. y )
72 56 71 sylan2b 
 |-  ( ( A =/= (/) /\ E. x e. ( A u. { (/) } ) A. y e. A -. x C. y ) -> E. x e. A A. y e. A -. x C. y )
73 55 72 sylan2 
 |-  ( ( A =/= (/) /\ E. x e. ( A u. { (/) } ) A. y e. ( A u. { (/) } ) -. x C. y ) -> E. x e. A A. y e. A -. x C. y )
74 1 51 73 syl2anc 
 |-  ( ( A e. dom card /\ A =/= (/) /\ A. z ( ( z C_ A /\ z =/= (/) /\ [C.] Or z ) -> U. z e. A ) ) -> E. x e. A A. y e. A -. x C. y )