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∈dom⁡card∧∀zz⊆A∧[⊂]Orz→⋃z∈A→∃x∈A∀y∈A¬x⊂y

Proof

Step Hyp Ref Expression
1 risset ⊢⋃z∈A↔∃x∈Ax=⋃z
2 eqimss2 ⊢x=⋃z→⋃z⊆x
3 unissb ⊢⋃z⊆x↔∀u∈zu⊆x
4 2 3 sylib ⊢x=⋃z→∀u∈zu⊆x
5 vex ⊢x∈V
6 5 brrpss ⊢u[⊂]x↔u⊂x
7 6 orbi1i ⊢u[⊂]x∨u=x↔u⊂x∨u=x
8 sspss ⊢u⊆x↔u⊂x∨u=x
9 7 8 bitr4i ⊢u[⊂]x∨u=x↔u⊆x
10 9 ralbii ⊢∀u∈zu[⊂]x∨u=x↔∀u∈zu⊆x
11 4 10 sylibr ⊢x=⋃z→∀u∈zu[⊂]x∨u=x
12 11 reximi ⊢∃x∈Ax=⋃z→∃x∈A∀u∈zu[⊂]x∨u=x
13 1 12 sylbi ⊢⋃z∈A→∃x∈A∀u∈zu[⊂]x∨u=x
14 13 imim2i ⊢z⊆A∧[⊂]Orz→⋃z∈A→z⊆A∧[⊂]Orz→∃x∈A∀u∈zu[⊂]x∨u=x
15 14 alimi ⊢∀zz⊆A∧[⊂]Orz→⋃z∈A→∀zz⊆A∧[⊂]Orz→∃x∈A∀u∈zu[⊂]x∨u=x
16 porpss ⊢[⊂]PoA
17 zorn2g ⊢A∈dom⁡card∧[⊂]PoA∧∀zz⊆A∧[⊂]Orz→∃x∈A∀u∈zu[⊂]x∨u=x→∃x∈A∀y∈A¬x[⊂]y
18 16 17 mp3an2 ⊢A∈dom⁡card∧∀zz⊆A∧[⊂]Orz→∃x∈A∀u∈zu[⊂]x∨u=x→∃x∈A∀y∈A¬x[⊂]y
19 15 18 sylan2 ⊢A∈dom⁡card∧∀zz⊆A∧[⊂]Orz→⋃z∈A→∃x∈A∀y∈A¬x[⊂]y
20 vex ⊢y∈V
21 20 brrpss ⊢x[⊂]y↔x⊂y
22 21 notbii ⊢¬x[⊂]y↔¬x⊂y
23 22 ralbii ⊢∀y∈A¬x[⊂]y↔∀y∈A¬x⊂y
24 23 rexbii ⊢∃x∈A∀y∈A¬x[⊂]y↔∃x∈A∀y∈A¬x⊂y
25 19 24 sylib ⊢A∈dom⁡card∧∀zz⊆A∧[⊂]Orz→⋃z∈A→∃x∈A∀y∈A¬x⊂y