Metamath Proof Explorer

Theorem zorng

Description: Zorn's Lemma. If the union of every chain (with respect to inclusion) in a set belongs to the set, then the set contains a maximal element. Theorem 6M of Enderton p. 151. This version of zorn avoids the Axiom of Choice by assuming that A is well-orderable. (Contributed by NM, 12-Aug-2004) (Revised by Mario Carneiro, 9-May-2015)

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

Proof

Step Hyp Ref Expression
1 risset 
 |-  ( U. z e. A <-> E. x e. A x = U. z )
2 eqimss2 
 |-  ( x = U. z -> U. z C_ x )
3 unissb 
 |-  ( U. z C_ x <-> A. u e. z u C_ x )
4 2 3 sylib 
 |-  ( x = U. z -> A. u e. z u C_ x )
5 vex 
 |-  x e. _V
6 5 brrpss 
 |-  ( u [C.] x <-> u C. x )
7 6 orbi1i 
 |-  ( ( u [C.] x \/ u = x ) <-> ( u C. x \/ u = x ) )
8 sspss 
 |-  ( u C_ x <-> ( u C. x \/ u = x ) )
9 7 8 bitr4i 
 |-  ( ( u [C.] x \/ u = x ) <-> u C_ x )
10 9 ralbii 
 |-  ( A. u e. z ( u [C.] x \/ u = x ) <-> A. u e. z u C_ x )
11 4 10 sylibr 
 |-  ( x = U. z -> A. u e. z ( u [C.] x \/ u = x ) )
12 11 reximi 
 |-  ( E. x e. A x = U. z -> E. x e. A A. u e. z ( u [C.] x \/ u = x ) )
13 1 12 sylbi 
 |-  ( U. z e. A -> E. x e. A A. u e. z ( u [C.] x \/ u = x ) )
14 13 imim2i 
 |-  ( ( ( z C_ A /\ [C.] Or z ) -> U. z e. A ) -> ( ( z C_ A /\ [C.] Or z ) -> E. x e. A A. u e. z ( u [C.] x \/ u = x ) ) )
15 14 alimi 
 |-  ( A. z ( ( z C_ A /\ [C.] Or z ) -> U. z e. A ) -> A. z ( ( z C_ A /\ [C.] Or z ) -> E. x e. A A. u e. z ( u [C.] x \/ u = x ) ) )
16 porpss 
 |-  [C.] Po A
17 zorn2g 
 |-  ( ( A e. dom card /\ [C.] Po A /\ A. z ( ( z C_ A /\ [C.] Or z ) -> E. x e. A A. u e. z ( u [C.] x \/ u = x ) ) ) -> E. x e. A A. y e. A -. x [C.] y )
18 16 17 mp3an2 
 |-  ( ( A e. dom card /\ A. z ( ( z C_ A /\ [C.] Or z ) -> E. x e. A A. u e. z ( u [C.] x \/ u = x ) ) ) -> E. x e. A A. y e. A -. x [C.] y )
19 15 18 sylan2 
 |-  ( ( A e. dom card /\ A. z ( ( z C_ A /\ [C.] Or z ) -> U. z e. A ) ) -> E. x e. A A. y e. A -. x [C.] y )
20 vex 
 |-  y e. _V
21 20 brrpss 
 |-  ( x [C.] y <-> x C. y )
22 21 notbii 
 |-  ( -. x [C.] y <-> -. x C. y )
23 22 ralbii 
 |-  ( A. y e. A -. x [C.] y <-> A. y e. A -. x C. y )
24 23 rexbii 
 |-  ( E. x e. A A. y e. A -. x [C.] y <-> E. x e. A A. y e. A -. x C. y )
25 19 24 sylib 
 |-  ( ( A e. dom card /\ A. z ( ( z C_ A /\ [C.] Or z ) -> U. z e. A ) ) -> E. x e. A A. y e. A -. x C. y )