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 69 rexeqdv
 |-  ( ( A =/= (/) /\ E. x e. { (/) } 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 ) )
71 58 70 mpbird
 |-  ( ( A =/= (/) /\ E. x e. { (/) } A. y e. A -. x C. y ) -> E. x e. A A. y e. A -. x C. y )
72 57 71 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 )
73 56 72 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 )
74 55 73 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 )
75 1 51 74 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 )