Metamath Proof Explorer


Theorem zornn0g

Description: Variant of Zorn's lemma zorng in which (/) , the union of the empty chain, is not required to be an element of A . (Contributed by Jeff Madsen, 5-Jan-2011) (Revised by Mario Carneiro, 9-May-2015)

Ref Expression
Assertion zornn0g AdomcardAzzAz[⊂]OrzzAxAyA¬xy

Proof

Step Hyp Ref Expression
1 simp2 AdomcardAzzAz[⊂]OrzzAA
2 simp1 AdomcardAzzAz[⊂]OrzzAAdomcard
3 snfi Fin
4 finnum Findomcard
5 3 4 ax-mp domcard
6 unnum AdomcarddomcardAdomcard
7 2 5 6 sylancl AdomcardAzzAz[⊂]OrzzAAdomcard
8 uncom A=A
9 8 sseq2i wAwA
10 ssundif wAwA
11 9 10 bitri wAwA
12 difss ww
13 soss ww[⊂]Orw[⊂]Orw
14 12 13 ax-mp [⊂]Orw[⊂]Orw
15 ssdif0 ww=
16 uni0b w=w
17 16 biimpri ww=
18 17 eleq1d wwAA
19 15 18 sylbir w=wAA
20 19 imbi2d w=zzAz[⊂]OrzzAwAzzAz[⊂]OrzzAA
21 vex wV
22 21 difexi wV
23 sseq1 z=wzAwA
24 neeq1 z=wzw
25 soeq2 z=w[⊂]Orz[⊂]Orw
26 23 24 25 3anbi123d z=wzAz[⊂]OrzwAw[⊂]Orw
27 unieq z=wz=w
28 27 eleq1d z=wzAwA
29 26 28 imbi12d z=wzAz[⊂]OrzzAwAw[⊂]OrwwA
30 22 29 spcv zzAz[⊂]OrzzAwAw[⊂]OrwwA
31 30 com12 wAw[⊂]OrwzzAz[⊂]OrzzAwA
32 31 3expa wAw[⊂]OrwzzAz[⊂]OrzzAwA
33 32 an32s wA[⊂]OrwwzzAz[⊂]OrzzAwA
34 unidif0 w=w
35 34 eleq1i wAwA
36 elun1 wAwA
37 35 36 sylbi wAwA
38 33 37 syl6 wA[⊂]OrwwzzAz[⊂]OrzzAwA
39 0ex V
40 39 snid
41 elun2 A
42 40 41 ax-mp A
43 42 2a1i wA[⊂]OrwzzAz[⊂]OrzzAA
44 20 38 43 pm2.61ne wA[⊂]OrwzzAz[⊂]OrzzAwA
45 14 44 sylan2 wA[⊂]OrwzzAz[⊂]OrzzAwA
46 11 45 sylanb wA[⊂]OrwzzAz[⊂]OrzzAwA
47 46 com12 zzAz[⊂]OrzzAwA[⊂]OrwwA
48 47 alrimiv zzAz[⊂]OrzzAwwA[⊂]OrwwA
49 48 3ad2ant3 AdomcardAzzAz[⊂]OrzzAwwA[⊂]OrwwA
50 zorng AdomcardwwA[⊂]OrwwAxAyA¬xy
51 7 49 50 syl2anc AdomcardAzzAz[⊂]OrzzAxAyA¬xy
52 ssun1 AA
53 ssralv AAyA¬xyyA¬xy
54 52 53 ax-mp yA¬xyyA¬xy
55 54 reximi xAyA¬xyxAyA¬xy
56 rexun xAyA¬xyxAyA¬xyxyA¬xy
57 simpr AxAyA¬xyxAyA¬xy
58 simpr AxyA¬xyxyA¬xy
59 psseq1 x=xyy
60 0pss yy
61 59 60 bitrdi x=xyy
62 61 notbid x=¬xy¬y
63 nne ¬yy=
64 62 63 bitrdi x=¬xyy=
65 64 ralbidv x=yA¬xyyAy=
66 39 65 rexsn xyA¬xyyAy=
67 eqsn AA=yAy=
68 67 biimpar AyAy=A=
69 66 68 sylan2b AxyA¬xyA=
70 69 rexeqdv AxyA¬xyxAyA¬xyxyA¬xy
71 58 70 mpbird AxyA¬xyxAyA¬xy
72 57 71 jaodan AxAyA¬xyxyA¬xyxAyA¬xy
73 56 72 sylan2b AxAyA¬xyxAyA¬xy
74 55 73 sylan2 AxAyA¬xyxAyA¬xy
75 1 51 74 syl2anc AdomcardAzzAz[⊂]OrzzAxAyA¬xy