MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  zornn0g Structured version   Visualization version   GIF version

Theorem zornn0g 9664
Description: Variant of Zorn's lemma zorng 9663 in which , the union of the empty chain, is not required to be an element of 𝐴. (Contributed by Jeff Madsen, 5-Jan-2011.) (Revised by Mario Carneiro, 9-May-2015.)
Assertion
Ref Expression
zornn0g ((𝐴 ∈ dom card ∧ 𝐴 ≠ ∅ ∧ ∀𝑧((𝑧𝐴𝑧 ≠ ∅ ∧ [] Or 𝑧) → 𝑧𝐴)) → ∃𝑥𝐴𝑦𝐴 ¬ 𝑥𝑦)
Distinct variable group:   𝑥,𝑦,𝑧,𝐴

Proof of Theorem zornn0g
Dummy variable 𝑤 is distinct from all other variables.
StepHypRef Expression
1 simp2 1128 . 2 ((𝐴 ∈ dom card ∧ 𝐴 ≠ ∅ ∧ ∀𝑧((𝑧𝐴𝑧 ≠ ∅ ∧ [] Or 𝑧) → 𝑧𝐴)) → 𝐴 ≠ ∅)
2 simp1 1127 . . . 4 ((𝐴 ∈ dom card ∧ 𝐴 ≠ ∅ ∧ ∀𝑧((𝑧𝐴𝑧 ≠ ∅ ∧ [] Or 𝑧) → 𝑧𝐴)) → 𝐴 ∈ dom card)
3 snfi 8328 . . . . 5 {∅} ∈ Fin
4 finnum 9109 . . . . 5 ({∅} ∈ Fin → {∅} ∈ dom card)
53, 4ax-mp 5 . . . 4 {∅} ∈ dom card
6 unnum 9359 . . . 4 ((𝐴 ∈ dom card ∧ {∅} ∈ dom card) → (𝐴 ∪ {∅}) ∈ dom card)
72, 5, 6sylancl 580 . . 3 ((𝐴 ∈ dom card ∧ 𝐴 ≠ ∅ ∧ ∀𝑧((𝑧𝐴𝑧 ≠ ∅ ∧ [] Or 𝑧) → 𝑧𝐴)) → (𝐴 ∪ {∅}) ∈ dom card)
8 uncom 3980 . . . . . . . . 9 (𝐴 ∪ {∅}) = ({∅} ∪ 𝐴)
98sseq2i 3849 . . . . . . . 8 (𝑤 ⊆ (𝐴 ∪ {∅}) ↔ 𝑤 ⊆ ({∅} ∪ 𝐴))
10 ssundif 4276 . . . . . . . 8 (𝑤 ⊆ ({∅} ∪ 𝐴) ↔ (𝑤 ∖ {∅}) ⊆ 𝐴)
119, 10bitri 267 . . . . . . 7 (𝑤 ⊆ (𝐴 ∪ {∅}) ↔ (𝑤 ∖ {∅}) ⊆ 𝐴)
12 difss 3960 . . . . . . . . 9 (𝑤 ∖ {∅}) ⊆ 𝑤
13 soss 5295 . . . . . . . . 9 ((𝑤 ∖ {∅}) ⊆ 𝑤 → ( [] Or 𝑤 → [] Or (𝑤 ∖ {∅})))
1412, 13ax-mp 5 . . . . . . . 8 ( [] Or 𝑤 → [] Or (𝑤 ∖ {∅}))
15 ssdif0 4172 . . . . . . . . . . 11 (𝑤 ⊆ {∅} ↔ (𝑤 ∖ {∅}) = ∅)
16 uni0b 4700 . . . . . . . . . . . . 13 ( 𝑤 = ∅ ↔ 𝑤 ⊆ {∅})
1716biimpri 220 . . . . . . . . . . . 12 (𝑤 ⊆ {∅} → 𝑤 = ∅)
1817eleq1d 2844 . . . . . . . . . . 11 (𝑤 ⊆ {∅} → ( 𝑤 ∈ (𝐴 ∪ {∅}) ↔ ∅ ∈ (𝐴 ∪ {∅})))
1915, 18sylbir 227 . . . . . . . . . 10 ((𝑤 ∖ {∅}) = ∅ → ( 𝑤 ∈ (𝐴 ∪ {∅}) ↔ ∅ ∈ (𝐴 ∪ {∅})))
2019imbi2d 332 . . . . . . . . 9 ((𝑤 ∖ {∅}) = ∅ → ((∀𝑧((𝑧𝐴𝑧 ≠ ∅ ∧ [] Or 𝑧) → 𝑧𝐴) → 𝑤 ∈ (𝐴 ∪ {∅})) ↔ (∀𝑧((𝑧𝐴𝑧 ≠ ∅ ∧ [] Or 𝑧) → 𝑧𝐴) → ∅ ∈ (𝐴 ∪ {∅}))))
21 vex 3401 . . . . . . . . . . . . . . 15 𝑤 ∈ V
2221difexi 5048 . . . . . . . . . . . . . 14 (𝑤 ∖ {∅}) ∈ V
23 sseq1 3845 . . . . . . . . . . . . . . . 16 (𝑧 = (𝑤 ∖ {∅}) → (𝑧𝐴 ↔ (𝑤 ∖ {∅}) ⊆ 𝐴))
24 neeq1 3031 . . . . . . . . . . . . . . . 16 (𝑧 = (𝑤 ∖ {∅}) → (𝑧 ≠ ∅ ↔ (𝑤 ∖ {∅}) ≠ ∅))
25 soeq2 5297 . . . . . . . . . . . . . . . 16 (𝑧 = (𝑤 ∖ {∅}) → ( [] Or 𝑧 ↔ [] Or (𝑤 ∖ {∅})))
2623, 24, 253anbi123d 1509 . . . . . . . . . . . . . . 15 (𝑧 = (𝑤 ∖ {∅}) → ((𝑧𝐴𝑧 ≠ ∅ ∧ [] Or 𝑧) ↔ ((𝑤 ∖ {∅}) ⊆ 𝐴 ∧ (𝑤 ∖ {∅}) ≠ ∅ ∧ [] Or (𝑤 ∖ {∅}))))
27 unieq 4681 . . . . . . . . . . . . . . . 16 (𝑧 = (𝑤 ∖ {∅}) → 𝑧 = (𝑤 ∖ {∅}))
2827eleq1d 2844 . . . . . . . . . . . . . . 15 (𝑧 = (𝑤 ∖ {∅}) → ( 𝑧𝐴 (𝑤 ∖ {∅}) ∈ 𝐴))
2926, 28imbi12d 336 . . . . . . . . . . . . . 14 (𝑧 = (𝑤 ∖ {∅}) → (((𝑧𝐴𝑧 ≠ ∅ ∧ [] Or 𝑧) → 𝑧𝐴) ↔ (((𝑤 ∖ {∅}) ⊆ 𝐴 ∧ (𝑤 ∖ {∅}) ≠ ∅ ∧ [] Or (𝑤 ∖ {∅})) → (𝑤 ∖ {∅}) ∈ 𝐴)))
3022, 29spcv 3501 . . . . . . . . . . . . 13 (∀𝑧((𝑧𝐴𝑧 ≠ ∅ ∧ [] Or 𝑧) → 𝑧𝐴) → (((𝑤 ∖ {∅}) ⊆ 𝐴 ∧ (𝑤 ∖ {∅}) ≠ ∅ ∧ [] Or (𝑤 ∖ {∅})) → (𝑤 ∖ {∅}) ∈ 𝐴))
3130com12 32 . . . . . . . . . . . 12 (((𝑤 ∖ {∅}) ⊆ 𝐴 ∧ (𝑤 ∖ {∅}) ≠ ∅ ∧ [] Or (𝑤 ∖ {∅})) → (∀𝑧((𝑧𝐴𝑧 ≠ ∅ ∧ [] Or 𝑧) → 𝑧𝐴) → (𝑤 ∖ {∅}) ∈ 𝐴))
32313expa 1108 . . . . . . . . . . 11 ((((𝑤 ∖ {∅}) ⊆ 𝐴 ∧ (𝑤 ∖ {∅}) ≠ ∅) ∧ [] Or (𝑤 ∖ {∅})) → (∀𝑧((𝑧𝐴𝑧 ≠ ∅ ∧ [] Or 𝑧) → 𝑧𝐴) → (𝑤 ∖ {∅}) ∈ 𝐴))
3332an32s 642 . . . . . . . . . 10 ((((𝑤 ∖ {∅}) ⊆ 𝐴 ∧ [] Or (𝑤 ∖ {∅})) ∧ (𝑤 ∖ {∅}) ≠ ∅) → (∀𝑧((𝑧𝐴𝑧 ≠ ∅ ∧ [] Or 𝑧) → 𝑧𝐴) → (𝑤 ∖ {∅}) ∈ 𝐴))
34 unidif0 5074 . . . . . . . . . . . 12 (𝑤 ∖ {∅}) = 𝑤
3534eleq1i 2850 . . . . . . . . . . 11 ( (𝑤 ∖ {∅}) ∈ 𝐴 𝑤𝐴)
36 elun1 4003 . . . . . . . . . . 11 ( 𝑤𝐴 𝑤 ∈ (𝐴 ∪ {∅}))
3735, 36sylbi 209 . . . . . . . . . 10 ( (𝑤 ∖ {∅}) ∈ 𝐴 𝑤 ∈ (𝐴 ∪ {∅}))
3833, 37syl6 35 . . . . . . . . 9 ((((𝑤 ∖ {∅}) ⊆ 𝐴 ∧ [] Or (𝑤 ∖ {∅})) ∧ (𝑤 ∖ {∅}) ≠ ∅) → (∀𝑧((𝑧𝐴𝑧 ≠ ∅ ∧ [] Or 𝑧) → 𝑧𝐴) → 𝑤 ∈ (𝐴 ∪ {∅})))
39 0ex 5028 . . . . . . . . . . . 12 ∅ ∈ V
4039snid 4430 . . . . . . . . . . 11 ∅ ∈ {∅}
41 elun2 4004 . . . . . . . . . . 11 (∅ ∈ {∅} → ∅ ∈ (𝐴 ∪ {∅}))
4240, 41ax-mp 5 . . . . . . . . . 10 ∅ ∈ (𝐴 ∪ {∅})
43422a1i 12 . . . . . . . . 9 (((𝑤 ∖ {∅}) ⊆ 𝐴 ∧ [] Or (𝑤 ∖ {∅})) → (∀𝑧((𝑧𝐴𝑧 ≠ ∅ ∧ [] Or 𝑧) → 𝑧𝐴) → ∅ ∈ (𝐴 ∪ {∅})))
4420, 38, 43pm2.61ne 3055 . . . . . . . 8 (((𝑤 ∖ {∅}) ⊆ 𝐴 ∧ [] Or (𝑤 ∖ {∅})) → (∀𝑧((𝑧𝐴𝑧 ≠ ∅ ∧ [] Or 𝑧) → 𝑧𝐴) → 𝑤 ∈ (𝐴 ∪ {∅})))
4514, 44sylan2 586 . . . . . . 7 (((𝑤 ∖ {∅}) ⊆ 𝐴 ∧ [] Or 𝑤) → (∀𝑧((𝑧𝐴𝑧 ≠ ∅ ∧ [] Or 𝑧) → 𝑧𝐴) → 𝑤 ∈ (𝐴 ∪ {∅})))
4611, 45sylanb 576 . . . . . 6 ((𝑤 ⊆ (𝐴 ∪ {∅}) ∧ [] Or 𝑤) → (∀𝑧((𝑧𝐴𝑧 ≠ ∅ ∧ [] Or 𝑧) → 𝑧𝐴) → 𝑤 ∈ (𝐴 ∪ {∅})))
4746com12 32 . . . . 5 (∀𝑧((𝑧𝐴𝑧 ≠ ∅ ∧ [] Or 𝑧) → 𝑧𝐴) → ((𝑤 ⊆ (𝐴 ∪ {∅}) ∧ [] Or 𝑤) → 𝑤 ∈ (𝐴 ∪ {∅})))
4847alrimiv 1970 . . . 4 (∀𝑧((𝑧𝐴𝑧 ≠ ∅ ∧ [] Or 𝑧) → 𝑧𝐴) → ∀𝑤((𝑤 ⊆ (𝐴 ∪ {∅}) ∧ [] Or 𝑤) → 𝑤 ∈ (𝐴 ∪ {∅})))
49483ad2ant3 1126 . . 3 ((𝐴 ∈ dom card ∧ 𝐴 ≠ ∅ ∧ ∀𝑧((𝑧𝐴𝑧 ≠ ∅ ∧ [] Or 𝑧) → 𝑧𝐴)) → ∀𝑤((𝑤 ⊆ (𝐴 ∪ {∅}) ∧ [] Or 𝑤) → 𝑤 ∈ (𝐴 ∪ {∅})))
50 zorng 9663 . . 3 (((𝐴 ∪ {∅}) ∈ dom card ∧ ∀𝑤((𝑤 ⊆ (𝐴 ∪ {∅}) ∧ [] Or 𝑤) → 𝑤 ∈ (𝐴 ∪ {∅}))) → ∃𝑥 ∈ (𝐴 ∪ {∅})∀𝑦 ∈ (𝐴 ∪ {∅}) ¬ 𝑥𝑦)
517, 49, 50syl2anc 579 . 2 ((𝐴 ∈ dom card ∧ 𝐴 ≠ ∅ ∧ ∀𝑧((𝑧𝐴𝑧 ≠ ∅ ∧ [] Or 𝑧) → 𝑧𝐴)) → ∃𝑥 ∈ (𝐴 ∪ {∅})∀𝑦 ∈ (𝐴 ∪ {∅}) ¬ 𝑥𝑦)
52 ssun1 3999 . . . . 5 𝐴 ⊆ (𝐴 ∪ {∅})
53 ssralv 3885 . . . . 5 (𝐴 ⊆ (𝐴 ∪ {∅}) → (∀𝑦 ∈ (𝐴 ∪ {∅}) ¬ 𝑥𝑦 → ∀𝑦𝐴 ¬ 𝑥𝑦))
5452, 53ax-mp 5 . . . 4 (∀𝑦 ∈ (𝐴 ∪ {∅}) ¬ 𝑥𝑦 → ∀𝑦𝐴 ¬ 𝑥𝑦)
5554reximi 3192 . . 3 (∃𝑥 ∈ (𝐴 ∪ {∅})∀𝑦 ∈ (𝐴 ∪ {∅}) ¬ 𝑥𝑦 → ∃𝑥 ∈ (𝐴 ∪ {∅})∀𝑦𝐴 ¬ 𝑥𝑦)
56 rexun 4016 . . . 4 (∃𝑥 ∈ (𝐴 ∪ {∅})∀𝑦𝐴 ¬ 𝑥𝑦 ↔ (∃𝑥𝐴𝑦𝐴 ¬ 𝑥𝑦 ∨ ∃𝑥 ∈ {∅}∀𝑦𝐴 ¬ 𝑥𝑦))
57 simpr 479 . . . . 5 ((𝐴 ≠ ∅ ∧ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥𝑦) → ∃𝑥𝐴𝑦𝐴 ¬ 𝑥𝑦)
58 simpr 479 . . . . . 6 ((𝐴 ≠ ∅ ∧ ∃𝑥 ∈ {∅}∀𝑦𝐴 ¬ 𝑥𝑦) → ∃𝑥 ∈ {∅}∀𝑦𝐴 ¬ 𝑥𝑦)
59 psseq1 3916 . . . . . . . . . . . . 13 (𝑥 = ∅ → (𝑥𝑦 ↔ ∅ ⊊ 𝑦))
60 0pss 4239 . . . . . . . . . . . . 13 (∅ ⊊ 𝑦𝑦 ≠ ∅)
6159, 60syl6bb 279 . . . . . . . . . . . 12 (𝑥 = ∅ → (𝑥𝑦𝑦 ≠ ∅))
6261notbid 310 . . . . . . . . . . 11 (𝑥 = ∅ → (¬ 𝑥𝑦 ↔ ¬ 𝑦 ≠ ∅))
63 nne 2973 . . . . . . . . . . 11 𝑦 ≠ ∅ ↔ 𝑦 = ∅)
6462, 63syl6bb 279 . . . . . . . . . 10 (𝑥 = ∅ → (¬ 𝑥𝑦𝑦 = ∅))
6564ralbidv 3168 . . . . . . . . 9 (𝑥 = ∅ → (∀𝑦𝐴 ¬ 𝑥𝑦 ↔ ∀𝑦𝐴 𝑦 = ∅))
6639, 65rexsn 4451 . . . . . . . 8 (∃𝑥 ∈ {∅}∀𝑦𝐴 ¬ 𝑥𝑦 ↔ ∀𝑦𝐴 𝑦 = ∅)
67 eqsn 4593 . . . . . . . . 9 (𝐴 ≠ ∅ → (𝐴 = {∅} ↔ ∀𝑦𝐴 𝑦 = ∅))
6867biimpar 471 . . . . . . . 8 ((𝐴 ≠ ∅ ∧ ∀𝑦𝐴 𝑦 = ∅) → 𝐴 = {∅})
6966, 68sylan2b 587 . . . . . . 7 ((𝐴 ≠ ∅ ∧ ∃𝑥 ∈ {∅}∀𝑦𝐴 ¬ 𝑥𝑦) → 𝐴 = {∅})
7069rexeqdv 3341 . . . . . 6 ((𝐴 ≠ ∅ ∧ ∃𝑥 ∈ {∅}∀𝑦𝐴 ¬ 𝑥𝑦) → (∃𝑥𝐴𝑦𝐴 ¬ 𝑥𝑦 ↔ ∃𝑥 ∈ {∅}∀𝑦𝐴 ¬ 𝑥𝑦))
7158, 70mpbird 249 . . . . 5 ((𝐴 ≠ ∅ ∧ ∃𝑥 ∈ {∅}∀𝑦𝐴 ¬ 𝑥𝑦) → ∃𝑥𝐴𝑦𝐴 ¬ 𝑥𝑦)
7257, 71jaodan 943 . . . 4 ((𝐴 ≠ ∅ ∧ (∃𝑥𝐴𝑦𝐴 ¬ 𝑥𝑦 ∨ ∃𝑥 ∈ {∅}∀𝑦𝐴 ¬ 𝑥𝑦)) → ∃𝑥𝐴𝑦𝐴 ¬ 𝑥𝑦)
7356, 72sylan2b 587 . . 3 ((𝐴 ≠ ∅ ∧ ∃𝑥 ∈ (𝐴 ∪ {∅})∀𝑦𝐴 ¬ 𝑥𝑦) → ∃𝑥𝐴𝑦𝐴 ¬ 𝑥𝑦)
7455, 73sylan2 586 . 2 ((𝐴 ≠ ∅ ∧ ∃𝑥 ∈ (𝐴 ∪ {∅})∀𝑦 ∈ (𝐴 ∪ {∅}) ¬ 𝑥𝑦) → ∃𝑥𝐴𝑦𝐴 ¬ 𝑥𝑦)
751, 51, 74syl2anc 579 1 ((𝐴 ∈ dom card ∧ 𝐴 ≠ ∅ ∧ ∀𝑧((𝑧𝐴𝑧 ≠ ∅ ∧ [] Or 𝑧) → 𝑧𝐴)) → ∃𝑥𝐴𝑦𝐴 ¬ 𝑥𝑦)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 386  wo 836  w3a 1071  wal 1599   = wceq 1601  wcel 2107  wne 2969  wral 3090  wrex 3091  cdif 3789  cun 3790  wss 3792  wpss 3793  c0 4141  {csn 4398   cuni 4673   Or wor 5275  dom cdm 5357   [] crpss 7215  Fincfn 8243  cardccrd 9096
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-rep 5008  ax-sep 5019  ax-nul 5027  ax-pow 5079  ax-pr 5140  ax-un 7228
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-ral 3095  df-rex 3096  df-reu 3097  df-rmo 3098  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-pss 3808  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-tp 4403  df-op 4405  df-uni 4674  df-int 4713  df-iun 4757  df-br 4889  df-opab 4951  df-mpt 4968  df-tr 4990  df-id 5263  df-eprel 5268  df-po 5276  df-so 5277  df-fr 5316  df-se 5317  df-we 5318  df-xp 5363  df-rel 5364  df-cnv 5365  df-co 5366  df-dm 5367  df-rn 5368  df-res 5369  df-ima 5370  df-pred 5935  df-ord 5981  df-on 5982  df-lim 5983  df-suc 5984  df-iota 6101  df-fun 6139  df-fn 6140  df-f 6141  df-f1 6142  df-fo 6143  df-f1o 6144  df-fv 6145  df-isom 6146  df-riota 6885  df-ov 6927  df-oprab 6928  df-mpt2 6929  df-rpss 7216  df-om 7346  df-wrecs 7691  df-recs 7753  df-rdg 7791  df-1o 7845  df-oadd 7849  df-er 8028  df-en 8244  df-dom 8245  df-fin 8247  df-card 9100  df-cda 9327
This theorem is referenced by:  zornn0  9667  pgpfac1lem5  18876  lbsextlem4  19569  filssufilg  22134
  Copyright terms: Public domain W3C validator