![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > zorng | Structured version Visualization version GIF version |
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 9541 avoids the Axiom of Choice by assuming that 𝐴 is well-orderable. (Contributed by NM, 12-Aug-2004.) (Revised by Mario Carneiro, 9-May-2015.) |
Ref | Expression |
---|---|
zorng | ⊢ ((𝐴 ∈ dom card ∧ ∀𝑧((𝑧 ⊆ 𝐴 ∧ [⊊] Or 𝑧) → ∪ 𝑧 ∈ 𝐴)) → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | risset 3200 | . . . . . 6 ⊢ (∪ 𝑧 ∈ 𝐴 ↔ ∃𝑥 ∈ 𝐴 𝑥 = ∪ 𝑧) | |
2 | eqimss2 3799 | . . . . . . . . 9 ⊢ (𝑥 = ∪ 𝑧 → ∪ 𝑧 ⊆ 𝑥) | |
3 | unissb 4621 | . . . . . . . . 9 ⊢ (∪ 𝑧 ⊆ 𝑥 ↔ ∀𝑢 ∈ 𝑧 𝑢 ⊆ 𝑥) | |
4 | 2, 3 | sylib 208 | . . . . . . . 8 ⊢ (𝑥 = ∪ 𝑧 → ∀𝑢 ∈ 𝑧 𝑢 ⊆ 𝑥) |
5 | vex 3343 | . . . . . . . . . . . 12 ⊢ 𝑥 ∈ V | |
6 | 5 | brrpss 7106 | . . . . . . . . . . 11 ⊢ (𝑢 [⊊] 𝑥 ↔ 𝑢 ⊊ 𝑥) |
7 | 6 | orbi1i 543 | . . . . . . . . . 10 ⊢ ((𝑢 [⊊] 𝑥 ∨ 𝑢 = 𝑥) ↔ (𝑢 ⊊ 𝑥 ∨ 𝑢 = 𝑥)) |
8 | sspss 3848 | . . . . . . . . . 10 ⊢ (𝑢 ⊆ 𝑥 ↔ (𝑢 ⊊ 𝑥 ∨ 𝑢 = 𝑥)) | |
9 | 7, 8 | bitr4i 267 | . . . . . . . . 9 ⊢ ((𝑢 [⊊] 𝑥 ∨ 𝑢 = 𝑥) ↔ 𝑢 ⊆ 𝑥) |
10 | 9 | ralbii 3118 | . . . . . . . 8 ⊢ (∀𝑢 ∈ 𝑧 (𝑢 [⊊] 𝑥 ∨ 𝑢 = 𝑥) ↔ ∀𝑢 ∈ 𝑧 𝑢 ⊆ 𝑥) |
11 | 4, 10 | sylibr 224 | . . . . . . 7 ⊢ (𝑥 = ∪ 𝑧 → ∀𝑢 ∈ 𝑧 (𝑢 [⊊] 𝑥 ∨ 𝑢 = 𝑥)) |
12 | 11 | reximi 3149 | . . . . . 6 ⊢ (∃𝑥 ∈ 𝐴 𝑥 = ∪ 𝑧 → ∃𝑥 ∈ 𝐴 ∀𝑢 ∈ 𝑧 (𝑢 [⊊] 𝑥 ∨ 𝑢 = 𝑥)) |
13 | 1, 12 | sylbi 207 | . . . . 5 ⊢ (∪ 𝑧 ∈ 𝐴 → ∃𝑥 ∈ 𝐴 ∀𝑢 ∈ 𝑧 (𝑢 [⊊] 𝑥 ∨ 𝑢 = 𝑥)) |
14 | 13 | imim2i 16 | . . . 4 ⊢ (((𝑧 ⊆ 𝐴 ∧ [⊊] Or 𝑧) → ∪ 𝑧 ∈ 𝐴) → ((𝑧 ⊆ 𝐴 ∧ [⊊] Or 𝑧) → ∃𝑥 ∈ 𝐴 ∀𝑢 ∈ 𝑧 (𝑢 [⊊] 𝑥 ∨ 𝑢 = 𝑥))) |
15 | 14 | alimi 1888 | . . 3 ⊢ (∀𝑧((𝑧 ⊆ 𝐴 ∧ [⊊] Or 𝑧) → ∪ 𝑧 ∈ 𝐴) → ∀𝑧((𝑧 ⊆ 𝐴 ∧ [⊊] Or 𝑧) → ∃𝑥 ∈ 𝐴 ∀𝑢 ∈ 𝑧 (𝑢 [⊊] 𝑥 ∨ 𝑢 = 𝑥))) |
16 | porpss 7107 | . . . 4 ⊢ [⊊] Po 𝐴 | |
17 | zorn2g 9537 | . . . 4 ⊢ ((𝐴 ∈ dom card ∧ [⊊] Po 𝐴 ∧ ∀𝑧((𝑧 ⊆ 𝐴 ∧ [⊊] Or 𝑧) → ∃𝑥 ∈ 𝐴 ∀𝑢 ∈ 𝑧 (𝑢 [⊊] 𝑥 ∨ 𝑢 = 𝑥))) → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 [⊊] 𝑦) | |
18 | 16, 17 | mp3an2 1561 | . . 3 ⊢ ((𝐴 ∈ dom card ∧ ∀𝑧((𝑧 ⊆ 𝐴 ∧ [⊊] Or 𝑧) → ∃𝑥 ∈ 𝐴 ∀𝑢 ∈ 𝑧 (𝑢 [⊊] 𝑥 ∨ 𝑢 = 𝑥))) → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 [⊊] 𝑦) |
19 | 15, 18 | sylan2 492 | . 2 ⊢ ((𝐴 ∈ dom card ∧ ∀𝑧((𝑧 ⊆ 𝐴 ∧ [⊊] Or 𝑧) → ∪ 𝑧 ∈ 𝐴)) → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 [⊊] 𝑦) |
20 | vex 3343 | . . . . . 6 ⊢ 𝑦 ∈ V | |
21 | 20 | brrpss 7106 | . . . . 5 ⊢ (𝑥 [⊊] 𝑦 ↔ 𝑥 ⊊ 𝑦) |
22 | 21 | notbii 309 | . . . 4 ⊢ (¬ 𝑥 [⊊] 𝑦 ↔ ¬ 𝑥 ⊊ 𝑦) |
23 | 22 | ralbii 3118 | . . 3 ⊢ (∀𝑦 ∈ 𝐴 ¬ 𝑥 [⊊] 𝑦 ↔ ∀𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦) |
24 | 23 | rexbii 3179 | . 2 ⊢ (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 [⊊] 𝑦 ↔ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦) |
25 | 19, 24 | sylib 208 | 1 ⊢ ((𝐴 ∈ dom card ∧ ∀𝑧((𝑧 ⊆ 𝐴 ∧ [⊊] Or 𝑧) → ∪ 𝑧 ∈ 𝐴)) → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∨ wo 382 ∧ wa 383 ∀wal 1630 = wceq 1632 ∈ wcel 2139 ∀wral 3050 ∃wrex 3051 ⊆ wss 3715 ⊊ wpss 3716 ∪ cuni 4588 class class class wbr 4804 Po wpo 5185 Or wor 5186 dom cdm 5266 [⊊] crpss 7102 cardccrd 8971 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1871 ax-4 1886 ax-5 1988 ax-6 2054 ax-7 2090 ax-8 2141 ax-9 2148 ax-10 2168 ax-11 2183 ax-12 2196 ax-13 2391 ax-ext 2740 ax-rep 4923 ax-sep 4933 ax-nul 4941 ax-pow 4992 ax-pr 5055 ax-un 7115 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3or 1073 df-3an 1074 df-tru 1635 df-ex 1854 df-nf 1859 df-sb 2047 df-eu 2611 df-mo 2612 df-clab 2747 df-cleq 2753 df-clel 2756 df-nfc 2891 df-ne 2933 df-ral 3055 df-rex 3056 df-reu 3057 df-rmo 3058 df-rab 3059 df-v 3342 df-sbc 3577 df-csb 3675 df-dif 3718 df-un 3720 df-in 3722 df-ss 3729 df-pss 3731 df-nul 4059 df-if 4231 df-pw 4304 df-sn 4322 df-pr 4324 df-tp 4326 df-op 4328 df-uni 4589 df-int 4628 df-iun 4674 df-br 4805 df-opab 4865 df-mpt 4882 df-tr 4905 df-id 5174 df-eprel 5179 df-po 5187 df-so 5188 df-fr 5225 df-se 5226 df-we 5227 df-xp 5272 df-rel 5273 df-cnv 5274 df-co 5275 df-dm 5276 df-rn 5277 df-res 5278 df-ima 5279 df-pred 5841 df-ord 5887 df-on 5888 df-suc 5890 df-iota 6012 df-fun 6051 df-fn 6052 df-f 6053 df-f1 6054 df-fo 6055 df-f1o 6056 df-fv 6057 df-isom 6058 df-riota 6775 df-rpss 7103 df-wrecs 7577 df-recs 7638 df-en 8124 df-card 8975 |
This theorem is referenced by: zornn0g 9539 zorn 9541 |
Copyright terms: Public domain | W3C validator |