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 ∧ ∀ z z ⊆ A ∧ [⊂] Or z → ⋃ z ∈ A → ∃ x ∈ A ∀ y ∈ A ¬ x ⊂ y

Proof

Step Hyp Ref Expression
1 risset ⊢ ⋃ z ∈ A ↔ ∃ x ∈ A x = ⋃ z
2 eqimss2 ⊢ x = ⋃ z → ⋃ z ⊆ x
3 unissb ⊢ ⋃ z ⊆ x ↔ ∀ u ∈ z u ⊆ x
4 2 3 sylib ⊢ x = ⋃ z → ∀ u ∈ z u ⊆ 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 ∈ z u [⊂] x ∨ u = x ↔ ∀ u ∈ z u ⊆ x
11 4 10 sylibr ⊢ x = ⋃ z → ∀ u ∈ z u [⊂] x ∨ u = x
12 11 reximi ⊢ ∃ x ∈ A x = ⋃ z → ∃ x ∈ A ∀ u ∈ z u [⊂] x ∨ u = x
13 1 12 sylbi ⊢ ⋃ z ∈ A → ∃ x ∈ A ∀ u ∈ z u [⊂] x ∨ u = x
14 13 imim2i ⊢ z ⊆ A ∧ [⊂] Or z → ⋃ z ∈ A → z ⊆ A ∧ [⊂] Or z → ∃ x ∈ A ∀ u ∈ z u [⊂] x ∨ u = x
15 14 alimi ⊢ ∀ z z ⊆ A ∧ [⊂] Or z → ⋃ z ∈ A → ∀ z z ⊆ A ∧ [⊂] Or z → ∃ x ∈ A ∀ u ∈ z u [⊂] x ∨ u = x
16 porpss ⊢ [⊂] Po A
17 zorn2g ⊢ A ∈ dom ⁡ card ∧ [⊂] Po A ∧ ∀ z z ⊆ A ∧ [⊂] Or z → ∃ x ∈ A ∀ u ∈ z u [⊂] x ∨ u = x → ∃ x ∈ A ∀ y ∈ A ¬ x [⊂] y
18 16 17 mp3an2 ⊢ A ∈ dom ⁡ card ∧ ∀ z z ⊆ A ∧ [⊂] Or z → ∃ x ∈ A ∀ u ∈ z u [⊂] x ∨ u = x → ∃ x ∈ A ∀ y ∈ A ¬ x [⊂] y
19 15 18 sylan2 ⊢ A ∈ dom ⁡ card ∧ ∀ z z ⊆ A ∧ [⊂] Or z → ⋃ 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 ∧ ∀ z z ⊆ A ∧ [⊂] Or z → ⋃ z ∈ A → ∃ x ∈ A ∀ y ∈ A ¬ x ⊂ y