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

Proof

Step Hyp Ref Expression
1 simp2 ( ( 𝐴 ∈ dom card ∧ 𝐴 ≠ ∅ ∧ ∀ 𝑧 ( ( 𝑧𝐴𝑧 ≠ ∅ ∧ [] Or 𝑧 ) → 𝑧𝐴 ) ) → 𝐴 ≠ ∅ )
2 simp1 ( ( 𝐴 ∈ dom card ∧ 𝐴 ≠ ∅ ∧ ∀ 𝑧 ( ( 𝑧𝐴𝑧 ≠ ∅ ∧ [] Or 𝑧 ) → 𝑧𝐴 ) ) → 𝐴 ∈ dom card )
3 snfi { ∅ } ∈ Fin
4 finnum ( { ∅ } ∈ Fin → { ∅ } ∈ dom card )
5 3 4 ax-mp { ∅ } ∈ dom card
6 unnum ( ( 𝐴 ∈ dom card ∧ { ∅ } ∈ dom card ) → ( 𝐴 ∪ { ∅ } ) ∈ dom card )
7 2 5 6 sylancl ( ( 𝐴 ∈ dom card ∧ 𝐴 ≠ ∅ ∧ ∀ 𝑧 ( ( 𝑧𝐴𝑧 ≠ ∅ ∧ [] Or 𝑧 ) → 𝑧𝐴 ) ) → ( 𝐴 ∪ { ∅ } ) ∈ dom card )
8 uncom ( 𝐴 ∪ { ∅ } ) = ( { ∅ } ∪ 𝐴 )
9 8 sseq2i ( 𝑤 ⊆ ( 𝐴 ∪ { ∅ } ) ↔ 𝑤 ⊆ ( { ∅ } ∪ 𝐴 ) )
10 ssundif ( 𝑤 ⊆ ( { ∅ } ∪ 𝐴 ) ↔ ( 𝑤 ∖ { ∅ } ) ⊆ 𝐴 )
11 9 10 bitri ( 𝑤 ⊆ ( 𝐴 ∪ { ∅ } ) ↔ ( 𝑤 ∖ { ∅ } ) ⊆ 𝐴 )
12 difss ( 𝑤 ∖ { ∅ } ) ⊆ 𝑤
13 soss ( ( 𝑤 ∖ { ∅ } ) ⊆ 𝑤 → ( [] Or 𝑤 → [] Or ( 𝑤 ∖ { ∅ } ) ) )
14 12 13 ax-mp ( [] Or 𝑤 → [] Or ( 𝑤 ∖ { ∅ } ) )
15 ssdif0 ( 𝑤 ⊆ { ∅ } ↔ ( 𝑤 ∖ { ∅ } ) = ∅ )
16 uni0b ( 𝑤 = ∅ ↔ 𝑤 ⊆ { ∅ } )
17 16 biimpri ( 𝑤 ⊆ { ∅ } → 𝑤 = ∅ )
18 17 eleq1d ( 𝑤 ⊆ { ∅ } → ( 𝑤 ∈ ( 𝐴 ∪ { ∅ } ) ↔ ∅ ∈ ( 𝐴 ∪ { ∅ } ) ) )
19 15 18 sylbir ( ( 𝑤 ∖ { ∅ } ) = ∅ → ( 𝑤 ∈ ( 𝐴 ∪ { ∅ } ) ↔ ∅ ∈ ( 𝐴 ∪ { ∅ } ) ) )
20 19 imbi2d ( ( 𝑤 ∖ { ∅ } ) = ∅ → ( ( ∀ 𝑧 ( ( 𝑧𝐴𝑧 ≠ ∅ ∧ [] Or 𝑧 ) → 𝑧𝐴 ) → 𝑤 ∈ ( 𝐴 ∪ { ∅ } ) ) ↔ ( ∀ 𝑧 ( ( 𝑧𝐴𝑧 ≠ ∅ ∧ [] Or 𝑧 ) → 𝑧𝐴 ) → ∅ ∈ ( 𝐴 ∪ { ∅ } ) ) ) )
21 vex 𝑤 ∈ V
22 21 difexi ( 𝑤 ∖ { ∅ } ) ∈ V
23 sseq1 ( 𝑧 = ( 𝑤 ∖ { ∅ } ) → ( 𝑧𝐴 ↔ ( 𝑤 ∖ { ∅ } ) ⊆ 𝐴 ) )
24 neeq1 ( 𝑧 = ( 𝑤 ∖ { ∅ } ) → ( 𝑧 ≠ ∅ ↔ ( 𝑤 ∖ { ∅ } ) ≠ ∅ ) )
25 soeq2 ( 𝑧 = ( 𝑤 ∖ { ∅ } ) → ( [] Or 𝑧 ↔ [] Or ( 𝑤 ∖ { ∅ } ) ) )
26 23 24 25 3anbi123d ( 𝑧 = ( 𝑤 ∖ { ∅ } ) → ( ( 𝑧𝐴𝑧 ≠ ∅ ∧ [] Or 𝑧 ) ↔ ( ( 𝑤 ∖ { ∅ } ) ⊆ 𝐴 ∧ ( 𝑤 ∖ { ∅ } ) ≠ ∅ ∧ [] Or ( 𝑤 ∖ { ∅ } ) ) ) )
27 unieq ( 𝑧 = ( 𝑤 ∖ { ∅ } ) → 𝑧 = ( 𝑤 ∖ { ∅ } ) )
28 27 eleq1d ( 𝑧 = ( 𝑤 ∖ { ∅ } ) → ( 𝑧𝐴 ( 𝑤 ∖ { ∅ } ) ∈ 𝐴 ) )
29 26 28 imbi12d ( 𝑧 = ( 𝑤 ∖ { ∅ } ) → ( ( ( 𝑧𝐴𝑧 ≠ ∅ ∧ [] Or 𝑧 ) → 𝑧𝐴 ) ↔ ( ( ( 𝑤 ∖ { ∅ } ) ⊆ 𝐴 ∧ ( 𝑤 ∖ { ∅ } ) ≠ ∅ ∧ [] Or ( 𝑤 ∖ { ∅ } ) ) → ( 𝑤 ∖ { ∅ } ) ∈ 𝐴 ) ) )
30 22 29 spcv ( ∀ 𝑧 ( ( 𝑧𝐴𝑧 ≠ ∅ ∧ [] Or 𝑧 ) → 𝑧𝐴 ) → ( ( ( 𝑤 ∖ { ∅ } ) ⊆ 𝐴 ∧ ( 𝑤 ∖ { ∅ } ) ≠ ∅ ∧ [] Or ( 𝑤 ∖ { ∅ } ) ) → ( 𝑤 ∖ { ∅ } ) ∈ 𝐴 ) )
31 30 com12 ( ( ( 𝑤 ∖ { ∅ } ) ⊆ 𝐴 ∧ ( 𝑤 ∖ { ∅ } ) ≠ ∅ ∧ [] Or ( 𝑤 ∖ { ∅ } ) ) → ( ∀ 𝑧 ( ( 𝑧𝐴𝑧 ≠ ∅ ∧ [] Or 𝑧 ) → 𝑧𝐴 ) → ( 𝑤 ∖ { ∅ } ) ∈ 𝐴 ) )
32 31 3expa ( ( ( ( 𝑤 ∖ { ∅ } ) ⊆ 𝐴 ∧ ( 𝑤 ∖ { ∅ } ) ≠ ∅ ) ∧ [] Or ( 𝑤 ∖ { ∅ } ) ) → ( ∀ 𝑧 ( ( 𝑧𝐴𝑧 ≠ ∅ ∧ [] Or 𝑧 ) → 𝑧𝐴 ) → ( 𝑤 ∖ { ∅ } ) ∈ 𝐴 ) )
33 32 an32s ( ( ( ( 𝑤 ∖ { ∅ } ) ⊆ 𝐴 ∧ [] Or ( 𝑤 ∖ { ∅ } ) ) ∧ ( 𝑤 ∖ { ∅ } ) ≠ ∅ ) → ( ∀ 𝑧 ( ( 𝑧𝐴𝑧 ≠ ∅ ∧ [] Or 𝑧 ) → 𝑧𝐴 ) → ( 𝑤 ∖ { ∅ } ) ∈ 𝐴 ) )
34 unidif0 ( 𝑤 ∖ { ∅ } ) = 𝑤
35 34 eleq1i ( ( 𝑤 ∖ { ∅ } ) ∈ 𝐴 𝑤𝐴 )
36 elun1 ( 𝑤𝐴 𝑤 ∈ ( 𝐴 ∪ { ∅ } ) )
37 35 36 sylbi ( ( 𝑤 ∖ { ∅ } ) ∈ 𝐴 𝑤 ∈ ( 𝐴 ∪ { ∅ } ) )
38 33 37 syl6 ( ( ( ( 𝑤 ∖ { ∅ } ) ⊆ 𝐴 ∧ [] Or ( 𝑤 ∖ { ∅ } ) ) ∧ ( 𝑤 ∖ { ∅ } ) ≠ ∅ ) → ( ∀ 𝑧 ( ( 𝑧𝐴𝑧 ≠ ∅ ∧ [] Or 𝑧 ) → 𝑧𝐴 ) → 𝑤 ∈ ( 𝐴 ∪ { ∅ } ) ) )
39 0ex ∅ ∈ V
40 39 snid ∅ ∈ { ∅ }
41 elun2 ( ∅ ∈ { ∅ } → ∅ ∈ ( 𝐴 ∪ { ∅ } ) )
42 40 41 ax-mp ∅ ∈ ( 𝐴 ∪ { ∅ } )
43 42 2a1i ( ( ( 𝑤 ∖ { ∅ } ) ⊆ 𝐴 ∧ [] Or ( 𝑤 ∖ { ∅ } ) ) → ( ∀ 𝑧 ( ( 𝑧𝐴𝑧 ≠ ∅ ∧ [] Or 𝑧 ) → 𝑧𝐴 ) → ∅ ∈ ( 𝐴 ∪ { ∅ } ) ) )
44 20 38 43 pm2.61ne ( ( ( 𝑤 ∖ { ∅ } ) ⊆ 𝐴 ∧ [] Or ( 𝑤 ∖ { ∅ } ) ) → ( ∀ 𝑧 ( ( 𝑧𝐴𝑧 ≠ ∅ ∧ [] Or 𝑧 ) → 𝑧𝐴 ) → 𝑤 ∈ ( 𝐴 ∪ { ∅ } ) ) )
45 14 44 sylan2 ( ( ( 𝑤 ∖ { ∅ } ) ⊆ 𝐴 ∧ [] Or 𝑤 ) → ( ∀ 𝑧 ( ( 𝑧𝐴𝑧 ≠ ∅ ∧ [] Or 𝑧 ) → 𝑧𝐴 ) → 𝑤 ∈ ( 𝐴 ∪ { ∅ } ) ) )
46 11 45 sylanb ( ( 𝑤 ⊆ ( 𝐴 ∪ { ∅ } ) ∧ [] Or 𝑤 ) → ( ∀ 𝑧 ( ( 𝑧𝐴𝑧 ≠ ∅ ∧ [] Or 𝑧 ) → 𝑧𝐴 ) → 𝑤 ∈ ( 𝐴 ∪ { ∅ } ) ) )
47 46 com12 ( ∀ 𝑧 ( ( 𝑧𝐴𝑧 ≠ ∅ ∧ [] Or 𝑧 ) → 𝑧𝐴 ) → ( ( 𝑤 ⊆ ( 𝐴 ∪ { ∅ } ) ∧ [] Or 𝑤 ) → 𝑤 ∈ ( 𝐴 ∪ { ∅ } ) ) )
48 47 alrimiv ( ∀ 𝑧 ( ( 𝑧𝐴𝑧 ≠ ∅ ∧ [] Or 𝑧 ) → 𝑧𝐴 ) → ∀ 𝑤 ( ( 𝑤 ⊆ ( 𝐴 ∪ { ∅ } ) ∧ [] Or 𝑤 ) → 𝑤 ∈ ( 𝐴 ∪ { ∅ } ) ) )
49 48 3ad2ant3 ( ( 𝐴 ∈ dom card ∧ 𝐴 ≠ ∅ ∧ ∀ 𝑧 ( ( 𝑧𝐴𝑧 ≠ ∅ ∧ [] Or 𝑧 ) → 𝑧𝐴 ) ) → ∀ 𝑤 ( ( 𝑤 ⊆ ( 𝐴 ∪ { ∅ } ) ∧ [] Or 𝑤 ) → 𝑤 ∈ ( 𝐴 ∪ { ∅ } ) ) )
50 zorng ( ( ( 𝐴 ∪ { ∅ } ) ∈ dom card ∧ ∀ 𝑤 ( ( 𝑤 ⊆ ( 𝐴 ∪ { ∅ } ) ∧ [] Or 𝑤 ) → 𝑤 ∈ ( 𝐴 ∪ { ∅ } ) ) ) → ∃ 𝑥 ∈ ( 𝐴 ∪ { ∅ } ) ∀ 𝑦 ∈ ( 𝐴 ∪ { ∅ } ) ¬ 𝑥𝑦 )
51 7 49 50 syl2anc ( ( 𝐴 ∈ dom card ∧ 𝐴 ≠ ∅ ∧ ∀ 𝑧 ( ( 𝑧𝐴𝑧 ≠ ∅ ∧ [] Or 𝑧 ) → 𝑧𝐴 ) ) → ∃ 𝑥 ∈ ( 𝐴 ∪ { ∅ } ) ∀ 𝑦 ∈ ( 𝐴 ∪ { ∅ } ) ¬ 𝑥𝑦 )
52 ssun1 𝐴 ⊆ ( 𝐴 ∪ { ∅ } )
53 ssralv ( 𝐴 ⊆ ( 𝐴 ∪ { ∅ } ) → ( ∀ 𝑦 ∈ ( 𝐴 ∪ { ∅ } ) ¬ 𝑥𝑦 → ∀ 𝑦𝐴 ¬ 𝑥𝑦 ) )
54 52 53 ax-mp ( ∀ 𝑦 ∈ ( 𝐴 ∪ { ∅ } ) ¬ 𝑥𝑦 → ∀ 𝑦𝐴 ¬ 𝑥𝑦 )
55 54 reximi ( ∃ 𝑥 ∈ ( 𝐴 ∪ { ∅ } ) ∀ 𝑦 ∈ ( 𝐴 ∪ { ∅ } ) ¬ 𝑥𝑦 → ∃ 𝑥 ∈ ( 𝐴 ∪ { ∅ } ) ∀ 𝑦𝐴 ¬ 𝑥𝑦 )
56 rexun ( ∃ 𝑥 ∈ ( 𝐴 ∪ { ∅ } ) ∀ 𝑦𝐴 ¬ 𝑥𝑦 ↔ ( ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥𝑦 ∨ ∃ 𝑥 ∈ { ∅ } ∀ 𝑦𝐴 ¬ 𝑥𝑦 ) )
57 simpr ( ( 𝐴 ≠ ∅ ∧ ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥𝑦 ) → ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥𝑦 )
58 simpr ( ( 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ { ∅ } ∀ 𝑦𝐴 ¬ 𝑥𝑦 ) → ∃ 𝑥 ∈ { ∅ } ∀ 𝑦𝐴 ¬ 𝑥𝑦 )
59 psseq1 ( 𝑥 = ∅ → ( 𝑥𝑦 ↔ ∅ ⊊ 𝑦 ) )
60 0pss ( ∅ ⊊ 𝑦𝑦 ≠ ∅ )
61 59 60 bitrdi ( 𝑥 = ∅ → ( 𝑥𝑦𝑦 ≠ ∅ ) )
62 61 notbid ( 𝑥 = ∅ → ( ¬ 𝑥𝑦 ↔ ¬ 𝑦 ≠ ∅ ) )
63 nne ( ¬ 𝑦 ≠ ∅ ↔ 𝑦 = ∅ )
64 62 63 bitrdi ( 𝑥 = ∅ → ( ¬ 𝑥𝑦𝑦 = ∅ ) )
65 64 ralbidv ( 𝑥 = ∅ → ( ∀ 𝑦𝐴 ¬ 𝑥𝑦 ↔ ∀ 𝑦𝐴 𝑦 = ∅ ) )
66 39 65 rexsn ( ∃ 𝑥 ∈ { ∅ } ∀ 𝑦𝐴 ¬ 𝑥𝑦 ↔ ∀ 𝑦𝐴 𝑦 = ∅ )
67 eqsn ( 𝐴 ≠ ∅ → ( 𝐴 = { ∅ } ↔ ∀ 𝑦𝐴 𝑦 = ∅ ) )
68 67 biimpar ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑦𝐴 𝑦 = ∅ ) → 𝐴 = { ∅ } )
69 66 68 sylan2b ( ( 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ { ∅ } ∀ 𝑦𝐴 ¬ 𝑥𝑦 ) → 𝐴 = { ∅ } )
70 69 rexeqdv ( ( 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ { ∅ } ∀ 𝑦𝐴 ¬ 𝑥𝑦 ) → ( ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥𝑦 ↔ ∃ 𝑥 ∈ { ∅ } ∀ 𝑦𝐴 ¬ 𝑥𝑦 ) )
71 58 70 mpbird ( ( 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ { ∅ } ∀ 𝑦𝐴 ¬ 𝑥𝑦 ) → ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥𝑦 )
72 57 71 jaodan ( ( 𝐴 ≠ ∅ ∧ ( ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥𝑦 ∨ ∃ 𝑥 ∈ { ∅ } ∀ 𝑦𝐴 ¬ 𝑥𝑦 ) ) → ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥𝑦 )
73 56 72 sylan2b ( ( 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ( 𝐴 ∪ { ∅ } ) ∀ 𝑦𝐴 ¬ 𝑥𝑦 ) → ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥𝑦 )
74 55 73 sylan2 ( ( 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ( 𝐴 ∪ { ∅ } ) ∀ 𝑦 ∈ ( 𝐴 ∪ { ∅ } ) ¬ 𝑥𝑦 ) → ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥𝑦 )
75 1 51 74 syl2anc ( ( 𝐴 ∈ dom card ∧ 𝐴 ≠ ∅ ∧ ∀ 𝑧 ( ( 𝑧𝐴𝑧 ≠ ∅ ∧ [] Or 𝑧 ) → 𝑧𝐴 ) ) → ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥𝑦 )