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 syl6bb ⊢ ( 𝑥 = ∅ → ( 𝑥 ⊊ 𝑦 ↔ 𝑦 ≠ ∅ ) )
62 61 notbid ⊢ ( 𝑥 = ∅ → ( ¬ 𝑥 ⊊ 𝑦 ↔ ¬ 𝑦 ≠ ∅ ) )
63 nne ⊢ ( ¬ 𝑦 ≠ ∅ ↔ 𝑦 = ∅ )
64 62 63 syl6bb ⊢ ( 𝑥 = ∅ → ( ¬ 𝑥 ⊊ 𝑦 ↔ 𝑦 = ∅ ) )
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 𝑧 ) → ∪ 𝑧 ∈ 𝐴 ) ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦 )