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	$⊢ (A \in dom card \land A \neq \emptyset \land \forall z ((z \subseteq A \land z \neq \emptyset \land [\subset] Or z) \to ⋃ z \in A)) \to \exists x \in A \forall y \in A \neg x \subset y$

Proof

Step	Hyp	Ref	Expression
1		simp2	$⊢ (A \in dom card \land A \neq \emptyset \land \forall z ((z \subseteq A \land z \neq \emptyset \land [\subset] Or z) \to ⋃ z \in A)) \to A \neq \emptyset$
2		simp1	$⊢ (A \in dom card \land A \neq \emptyset \land \forall z ((z \subseteq A \land z \neq \emptyset \land [\subset] Or z) \to ⋃ z \in A)) \to A \in dom card$
3		snfi	$⊢ \{\emptyset\} \in Fin$
4		finnum	$⊢ \{\emptyset\} \in Fin \to \{\emptyset\} \in dom card$
5	3 4	ax-mp	$⊢ \{\emptyset\} \in dom card$
6		unnum	$⊢ (A \in dom card \land \{\emptyset\} \in dom card) \to A \cup \{\emptyset\} \in dom card$
7	2 5 6	sylancl	$⊢ (A \in dom card \land A \neq \emptyset \land \forall z ((z \subseteq A \land z \neq \emptyset \land [\subset] Or z) \to ⋃ z \in A)) \to A \cup \{\emptyset\} \in dom card$
8		uncom	$⊢ A \cup \{\emptyset\} = \{\emptyset\} \cup A$
9	8	sseq2i	$⊢ w \subseteq A \cup \{\emptyset\} \leftrightarrow w \subseteq \{\emptyset\} \cup A$
10		ssundif	$⊢ w \subseteq \{\emptyset\} \cup A \leftrightarrow w ∖ \{\emptyset\} \subseteq A$
11	9 10	bitri	$⊢ w \subseteq A \cup \{\emptyset\} \leftrightarrow w ∖ \{\emptyset\} \subseteq A$
12		difss	$⊢ w ∖ \{\emptyset\} \subseteq w$
13		soss	$⊢ w ∖ \{\emptyset\} \subseteq w \to ([\subset] Or w \to [\subset] Or (w ∖ \{\emptyset\}))$
14	12 13	ax-mp	$⊢ [\subset] Or w \to [\subset] Or (w ∖ \{\emptyset\})$
15		ssdif0	$⊢ w \subseteq \{\emptyset\} \leftrightarrow w ∖ \{\emptyset\} = \emptyset$
16		uni0b	$⊢ ⋃ w = \emptyset \leftrightarrow w \subseteq \{\emptyset\}$
17	16	biimpri	$⊢ w \subseteq \{\emptyset\} \to ⋃ w = \emptyset$
18	17	eleq1d	$⊢ w \subseteq \{\emptyset\} \to (⋃ w \in (A \cup \{\emptyset\}) \leftrightarrow \emptyset \in (A \cup \{\emptyset\}))$
19	15 18	sylbir	$⊢ w ∖ \{\emptyset\} = \emptyset \to (⋃ w \in (A \cup \{\emptyset\}) \leftrightarrow \emptyset \in (A \cup \{\emptyset\}))$
20	19	imbi2d	$⊢ w ∖ \{\emptyset\} = \emptyset \to ((\forall z ((z \subseteq A \land z \neq \emptyset \land [\subset] Or z) \to ⋃ z \in A) \to ⋃ w \in (A \cup \{\emptyset\})) \leftrightarrow (\forall z ((z \subseteq A \land z \neq \emptyset \land [\subset] Or z) \to ⋃ z \in A) \to \emptyset \in (A \cup \{\emptyset\})))$
21		vex	$⊢ w \in V$
22	21	difexi	$⊢ w ∖ \{\emptyset\} \in V$
23		sseq1	$⊢ z = w ∖ \{\emptyset\} \to (z \subseteq A \leftrightarrow w ∖ \{\emptyset\} \subseteq A)$
24		neeq1	$⊢ z = w ∖ \{\emptyset\} \to (z \neq \emptyset \leftrightarrow w ∖ \{\emptyset\} \neq \emptyset)$
25		soeq2	$⊢ z = w ∖ \{\emptyset\} \to ([\subset] Or z \leftrightarrow [\subset] Or (w ∖ \{\emptyset\}))$
26	23 24 25	3anbi123d	$⊢ z = w ∖ \{\emptyset\} \to ((z \subseteq A \land z \neq \emptyset \land [\subset] Or z) \leftrightarrow (w ∖ \{\emptyset\} \subseteq A \land w ∖ \{\emptyset\} \neq \emptyset \land [\subset] Or (w ∖ \{\emptyset\})))$
27		unieq	$⊢ z = w ∖ \{\emptyset\} \to ⋃ z = ⋃ (w ∖ \{\emptyset\})$
28	27	eleq1d	$⊢ z = w ∖ \{\emptyset\} \to (⋃ z \in A \leftrightarrow ⋃ (w ∖ \{\emptyset\}) \in A)$
29	26 28	imbi12d	$⊢ z = w ∖ \{\emptyset\} \to (((z \subseteq A \land z \neq \emptyset \land [\subset] Or z) \to ⋃ z \in A) \leftrightarrow ((w ∖ \{\emptyset\} \subseteq A \land w ∖ \{\emptyset\} \neq \emptyset \land [\subset] Or (w ∖ \{\emptyset\})) \to ⋃ (w ∖ \{\emptyset\}) \in A))$
30	22 29	spcv	$⊢ \forall z ((z \subseteq A \land z \neq \emptyset \land [\subset] Or z) \to ⋃ z \in A) \to ((w ∖ \{\emptyset\} \subseteq A \land w ∖ \{\emptyset\} \neq \emptyset \land [\subset] Or (w ∖ \{\emptyset\})) \to ⋃ (w ∖ \{\emptyset\}) \in A)$
31	30	com12	$⊢ (w ∖ \{\emptyset\} \subseteq A \land w ∖ \{\emptyset\} \neq \emptyset \land [\subset] Or (w ∖ \{\emptyset\})) \to (\forall z ((z \subseteq A \land z \neq \emptyset \land [\subset] Or z) \to ⋃ z \in A) \to ⋃ (w ∖ \{\emptyset\}) \in A)$
32	31	3expa	$⊢ ((w ∖ \{\emptyset\} \subseteq A \land w ∖ \{\emptyset\} \neq \emptyset) \land [\subset] Or (w ∖ \{\emptyset\})) \to (\forall z ((z \subseteq A \land z \neq \emptyset \land [\subset] Or z) \to ⋃ z \in A) \to ⋃ (w ∖ \{\emptyset\}) \in A)$
33	32	an32s	$⊢ ((w ∖ \{\emptyset\} \subseteq A \land [\subset] Or (w ∖ \{\emptyset\})) \land w ∖ \{\emptyset\} \neq \emptyset) \to (\forall z ((z \subseteq A \land z \neq \emptyset \land [\subset] Or z) \to ⋃ z \in A) \to ⋃ (w ∖ \{\emptyset\}) \in A)$
34		unidif0	$⊢ ⋃ (w ∖ \{\emptyset\}) = ⋃ w$
35	34	eleq1i	$⊢ ⋃ (w ∖ \{\emptyset\}) \in A \leftrightarrow ⋃ w \in A$
36		elun1	$⊢ ⋃ w \in A \to ⋃ w \in (A \cup \{\emptyset\})$
37	35 36	sylbi	$⊢ ⋃ (w ∖ \{\emptyset\}) \in A \to ⋃ w \in (A \cup \{\emptyset\})$
38	33 37	syl6	$⊢ ((w ∖ \{\emptyset\} \subseteq A \land [\subset] Or (w ∖ \{\emptyset\})) \land w ∖ \{\emptyset\} \neq \emptyset) \to (\forall z ((z \subseteq A \land z \neq \emptyset \land [\subset] Or z) \to ⋃ z \in A) \to ⋃ w \in (A \cup \{\emptyset\}))$
39		0ex	$⊢ \emptyset \in V$
40	39	snid	$⊢ \emptyset \in \{\emptyset\}$
41		elun2	$⊢ \emptyset \in \{\emptyset\} \to \emptyset \in (A \cup \{\emptyset\})$
42	40 41	ax-mp	$⊢ \emptyset \in (A \cup \{\emptyset\})$
43	42	2a1i	$⊢ (w ∖ \{\emptyset\} \subseteq A \land [\subset] Or (w ∖ \{\emptyset\})) \to (\forall z ((z \subseteq A \land z \neq \emptyset \land [\subset] Or z) \to ⋃ z \in A) \to \emptyset \in (A \cup \{\emptyset\}))$
44	20 38 43	pm2.61ne	$⊢ (w ∖ \{\emptyset\} \subseteq A \land [\subset] Or (w ∖ \{\emptyset\})) \to (\forall z ((z \subseteq A \land z \neq \emptyset \land [\subset] Or z) \to ⋃ z \in A) \to ⋃ w \in (A \cup \{\emptyset\}))$
45	14 44	sylan2	$⊢ (w ∖ \{\emptyset\} \subseteq A \land [\subset] Or w) \to (\forall z ((z \subseteq A \land z \neq \emptyset \land [\subset] Or z) \to ⋃ z \in A) \to ⋃ w \in (A \cup \{\emptyset\}))$
46	11 45	sylanb	$⊢ (w \subseteq A \cup \{\emptyset\} \land [\subset] Or w) \to (\forall z ((z \subseteq A \land z \neq \emptyset \land [\subset] Or z) \to ⋃ z \in A) \to ⋃ w \in (A \cup \{\emptyset\}))$
47	46	com12	$⊢ \forall z ((z \subseteq A \land z \neq \emptyset \land [\subset] Or z) \to ⋃ z \in A) \to ((w \subseteq A \cup \{\emptyset\} \land [\subset] Or w) \to ⋃ w \in (A \cup \{\emptyset\}))$
48	47	alrimiv	$⊢ \forall z ((z \subseteq A \land z \neq \emptyset \land [\subset] Or z) \to ⋃ z \in A) \to \forall w ((w \subseteq A \cup \{\emptyset\} \land [\subset] Or w) \to ⋃ w \in (A \cup \{\emptyset\}))$
49	48	3ad2ant3	$⊢ (A \in dom card \land A \neq \emptyset \land \forall z ((z \subseteq A \land z \neq \emptyset \land [\subset] Or z) \to ⋃ z \in A)) \to \forall w ((w \subseteq A \cup \{\emptyset\} \land [\subset] Or w) \to ⋃ w \in (A \cup \{\emptyset\}))$
50		zorng	$⊢ (A \cup \{\emptyset\} \in dom card \land \forall w ((w \subseteq A \cup \{\emptyset\} \land [\subset] Or w) \to ⋃ w \in (A \cup \{\emptyset\}))) \to \exists x \in (A \cup \{\emptyset\}) \forall y \in (A \cup \{\emptyset\}) \neg x \subset y$
51	7 49 50	syl2anc	$⊢ (A \in dom card \land A \neq \emptyset \land \forall z ((z \subseteq A \land z \neq \emptyset \land [\subset] Or z) \to ⋃ z \in A)) \to \exists x \in (A \cup \{\emptyset\}) \forall y \in (A \cup \{\emptyset\}) \neg x \subset y$
52		ssun1	$⊢ A \subseteq A \cup \{\emptyset\}$
53		ssralv	$⊢ A \subseteq A \cup \{\emptyset\} \to (\forall y \in (A \cup \{\emptyset\}) \neg x \subset y \to \forall y \in A \neg x \subset y)$
54	52 53	ax-mp	$⊢ \forall y \in (A \cup \{\emptyset\}) \neg x \subset y \to \forall y \in A \neg x \subset y$
55	54	reximi	$⊢ \exists x \in (A \cup \{\emptyset\}) \forall y \in (A \cup \{\emptyset\}) \neg x \subset y \to \exists x \in (A \cup \{\emptyset\}) \forall y \in A \neg x \subset y$
56		rexun	$⊢ \exists x \in (A \cup \{\emptyset\}) \forall y \in A \neg x \subset y \leftrightarrow (\exists x \in A \forall y \in A \neg x \subset y \lor \exists x \in \{\emptyset\} \forall y \in A \neg x \subset y)$
57		simpr	$⊢ (A \neq \emptyset \land \exists x \in A \forall y \in A \neg x \subset y) \to \exists x \in A \forall y \in A \neg x \subset y$
58		simpr	$⊢ (A \neq \emptyset \land \exists x \in \{\emptyset\} \forall y \in A \neg x \subset y) \to \exists x \in \{\emptyset\} \forall y \in A \neg x \subset y$
59		psseq1	$⊢ x = \emptyset \to (x \subset y \leftrightarrow \emptyset \subset y)$
60		0pss	$⊢ \emptyset \subset y \leftrightarrow y \neq \emptyset$
61	59 60	bitrdi	$⊢ x = \emptyset \to (x \subset y \leftrightarrow y \neq \emptyset)$
62	61	notbid	$⊢ x = \emptyset \to (\neg x \subset y \leftrightarrow \neg y \neq \emptyset)$
63		nne	$⊢ \neg y \neq \emptyset \leftrightarrow y = \emptyset$
64	62 63	bitrdi	$⊢ x = \emptyset \to (\neg x \subset y \leftrightarrow y = \emptyset)$
65	64	ralbidv	$⊢ x = \emptyset \to (\forall y \in A \neg x \subset y \leftrightarrow \forall y \in A y = \emptyset)$
66	39 65	rexsn	$⊢ \exists x \in \{\emptyset\} \forall y \in A \neg x \subset y \leftrightarrow \forall y \in A y = \emptyset$
67		eqsn	$⊢ A \neq \emptyset \to (A = \{\emptyset\} \leftrightarrow \forall y \in A y = \emptyset)$
68	67	biimpar	$⊢ (A \neq \emptyset \land \forall y \in A y = \emptyset) \to A = \{\emptyset\}$
69	66 68	sylan2b	$⊢ (A \neq \emptyset \land \exists x \in \{\emptyset\} \forall y \in A \neg x \subset y) \to A = \{\emptyset\}$
70	58 69	rexeqtrrdv	$⊢ (A \neq \emptyset \land \exists x \in \{\emptyset\} \forall y \in A \neg x \subset y) \to \exists x \in A \forall y \in A \neg x \subset y$
71	57 70	jaodan	$⊢ (A \neq \emptyset \land (\exists x \in A \forall y \in A \neg x \subset y \lor \exists x \in \{\emptyset\} \forall y \in A \neg x \subset y)) \to \exists x \in A \forall y \in A \neg x \subset y$
72	56 71	sylan2b	$⊢ (A \neq \emptyset \land \exists x \in (A \cup \{\emptyset\}) \forall y \in A \neg x \subset y) \to \exists x \in A \forall y \in A \neg x \subset y$
73	55 72	sylan2	$⊢ (A \neq \emptyset \land \exists x \in (A \cup \{\emptyset\}) \forall y \in (A \cup \{\emptyset\}) \neg x \subset y) \to \exists x \in A \forall y \in A \neg x \subset y$
74	1 51 73	syl2anc	$⊢ (A \in dom card \land A \neq \emptyset \land \forall z ((z \subseteq A \land z \neq \emptyset \land [\subset] Or z) \to ⋃ z \in A)) \to \exists x \in A \forall y \in A \neg x \subset y$

Metamath Proof Explorer

Theorem zornn0g

Proof