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 ( ( 𝐴 ∈ dom card ∧ ∀ 𝑧 ( ( 𝑧 ⊆ 𝐴 ∧ [⊊] Or 𝑧 ) → ∪ 𝑧 ∈ 𝐴 ) ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦 )

Proof

Step Hyp Ref Expression
1 risset ⊢ ( ∪ 𝑧 ∈ 𝐴 ↔ ∃ 𝑥 ∈ 𝐴 𝑥 = ∪ 𝑧 )
2 eqimss2 ⊢ ( 𝑥 = ∪ 𝑧 → ∪ 𝑧 ⊆ 𝑥 )
3 unissb ⊢ ( ∪ 𝑧 ⊆ 𝑥 ↔ ∀ 𝑢 ∈ 𝑧 𝑢 ⊆ 𝑥 )
4 2 3 sylib ⊢ ( 𝑥 = ∪ 𝑧 → ∀ 𝑢 ∈ 𝑧 𝑢 ⊆ 𝑥 )
5 vex ⊢ 𝑥 ∈ V
6 5 brrpss ⊢ ( 𝑢 [⊊] 𝑥 ↔ 𝑢 ⊊ 𝑥 )
7 6 orbi1i ⊢ ( ( 𝑢 [⊊] 𝑥 ∨ 𝑢 = 𝑥 ) ↔ ( 𝑢 ⊊ 𝑥 ∨ 𝑢 = 𝑥 ) )
8 sspss ⊢ ( 𝑢 ⊆ 𝑥 ↔ ( 𝑢 ⊊ 𝑥 ∨ 𝑢 = 𝑥 ) )
9 7 8 bitr4i ⊢ ( ( 𝑢 [⊊] 𝑥 ∨ 𝑢 = 𝑥 ) ↔ 𝑢 ⊆ 𝑥 )
10 9 ralbii ⊢ ( ∀ 𝑢 ∈ 𝑧 ( 𝑢 [⊊] 𝑥 ∨ 𝑢 = 𝑥 ) ↔ ∀ 𝑢 ∈ 𝑧 𝑢 ⊆ 𝑥 )
11 4 10 sylibr ⊢ ( 𝑥 = ∪ 𝑧 → ∀ 𝑢 ∈ 𝑧 ( 𝑢 [⊊] 𝑥 ∨ 𝑢 = 𝑥 ) )
12 11 reximi ⊢ ( ∃ 𝑥 ∈ 𝐴 𝑥 = ∪ 𝑧 → ∃ 𝑥 ∈ 𝐴 ∀ 𝑢 ∈ 𝑧 ( 𝑢 [⊊] 𝑥 ∨ 𝑢 = 𝑥 ) )
13 1 12 sylbi ⊢ ( ∪ 𝑧 ∈ 𝐴 → ∃ 𝑥 ∈ 𝐴 ∀ 𝑢 ∈ 𝑧 ( 𝑢 [⊊] 𝑥 ∨ 𝑢 = 𝑥 ) )
14 13 imim2i ⊢ ( ( ( 𝑧 ⊆ 𝐴 ∧ [⊊] Or 𝑧 ) → ∪ 𝑧 ∈ 𝐴 ) → ( ( 𝑧 ⊆ 𝐴 ∧ [⊊] Or 𝑧 ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑢 ∈ 𝑧 ( 𝑢 [⊊] 𝑥 ∨ 𝑢 = 𝑥 ) ) )
15 14 alimi ⊢ ( ∀ 𝑧 ( ( 𝑧 ⊆ 𝐴 ∧ [⊊] Or 𝑧 ) → ∪ 𝑧 ∈ 𝐴 ) → ∀ 𝑧 ( ( 𝑧 ⊆ 𝐴 ∧ [⊊] Or 𝑧 ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑢 ∈ 𝑧 ( 𝑢 [⊊] 𝑥 ∨ 𝑢 = 𝑥 ) ) )
16 porpss ⊢ [⊊] Po 𝐴
17 zorn2g ⊢ ( ( 𝐴 ∈ dom card ∧ [⊊] Po 𝐴 ∧ ∀ 𝑧 ( ( 𝑧 ⊆ 𝐴 ∧ [⊊] Or 𝑧 ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑢 ∈ 𝑧 ( 𝑢 [⊊] 𝑥 ∨ 𝑢 = 𝑥 ) ) ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 [⊊] 𝑦 )
18 16 17 mp3an2 ⊢ ( ( 𝐴 ∈ dom card ∧ ∀ 𝑧 ( ( 𝑧 ⊆ 𝐴 ∧ [⊊] Or 𝑧 ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑢 ∈ 𝑧 ( 𝑢 [⊊] 𝑥 ∨ 𝑢 = 𝑥 ) ) ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 [⊊] 𝑦 )
19 15 18 sylan2 ⊢ ( ( 𝐴 ∈ dom card ∧ ∀ 𝑧 ( ( 𝑧 ⊆ 𝐴 ∧ [⊊] Or 𝑧 ) → ∪ 𝑧 ∈ 𝐴 ) ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 [⊊] 𝑦 )
20 vex ⊢ 𝑦 ∈ V
21 20 brrpss ⊢ ( 𝑥 [⊊] 𝑦 ↔ 𝑥 ⊊ 𝑦 )
22 21 notbii ⊢ ( ¬ 𝑥 [⊊] 𝑦 ↔ ¬ 𝑥 ⊊ 𝑦 )
23 22 ralbii ⊢ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 [⊊] 𝑦 ↔ ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦 )
24 23 rexbii ⊢ ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 [⊊] 𝑦 ↔ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦 )
25 19 24 sylib ⊢ ( ( 𝐴 ∈ dom card ∧ ∀ 𝑧 ( ( 𝑧 ⊆ 𝐴 ∧ [⊊] Or 𝑧 ) → ∪ 𝑧 ∈ 𝐴 ) ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦 )