filssufilg

Description: A filter is contained in some ultrafilter. This version of filssufil contains the choice as a hypothesis (in the assumption that ~P ~P X is well-orderable). (Contributed by Mario Carneiro, 24-May-2015) (Revised by Stefan O'Rear, 2-Aug-2015)

		Ref	Expression
	Assertion	filssufilg	$⊢ (F \in Fil (X) \land 𝒫 𝒫 X \in dom card) \to \exists f \in UFil (X) F \subseteq f$

Proof

Step	Hyp	Ref	Expression
1		simpr	$⊢ (F \in Fil (X) \land 𝒫 𝒫 X \in dom card) \to 𝒫 𝒫 X \in dom card$
2		rabss	$⊢ \{g \in Fil (X) \| F \subseteq g\} \subseteq 𝒫 𝒫 X \leftrightarrow \forall g \in Fil (X) (F \subseteq g \to g \in 𝒫 𝒫 X)$
3		filsspw	$⊢ g \in Fil (X) \to g \subseteq 𝒫 X$
4		velpw	$⊢ g \in 𝒫 𝒫 X \leftrightarrow g \subseteq 𝒫 X$
5	3 4	sylibr	$⊢ g \in Fil (X) \to g \in 𝒫 𝒫 X$
6	5	a1d	$⊢ g \in Fil (X) \to (F \subseteq g \to g \in 𝒫 𝒫 X)$
7	2 6	mprgbir	$⊢ \{g \in Fil (X) \| F \subseteq g\} \subseteq 𝒫 𝒫 X$
8		ssnum	$⊢ (𝒫 𝒫 X \in dom card \land \{g \in Fil (X) \| F \subseteq g\} \subseteq 𝒫 𝒫 X) \to \{g \in Fil (X) \| F \subseteq g\} \in dom card$
9	1 7 8	sylancl	$⊢ (F \in Fil (X) \land 𝒫 𝒫 X \in dom card) \to \{g \in Fil (X) \| F \subseteq g\} \in dom card$
10		ssid	$⊢ F \subseteq F$
11	10	jctr	$⊢ F \in Fil (X) \to (F \in Fil (X) \land F \subseteq F)$
12		sseq2	$⊢ g = F \to (F \subseteq g \leftrightarrow F \subseteq F)$
13	12	elrab	$⊢ F \in \{g \in Fil (X) \| F \subseteq g\} \leftrightarrow (F \in Fil (X) \land F \subseteq F)$
14	11 13	sylibr	$⊢ F \in Fil (X) \to F \in \{g \in Fil (X) \| F \subseteq g\}$
15	14	ne0d	$⊢ F \in Fil (X) \to \{g \in Fil (X) \| F \subseteq g\} \neq \emptyset$
16	15	adantr	$⊢ (F \in Fil (X) \land 𝒫 𝒫 X \in dom card) \to \{g \in Fil (X) \| F \subseteq g\} \neq \emptyset$
17		sseq2	$⊢ g = ⋃ x \to (F \subseteq g \leftrightarrow F \subseteq ⋃ x)$
18		simpr1	$⊢ (F \in Fil (X) \land (x \subseteq \{g \in Fil (X) \| F \subseteq g\} \land x \neq \emptyset \land [\subset] Or x)) \to x \subseteq \{g \in Fil (X) \| F \subseteq g\}$
19		ssrab	$⊢ x \subseteq \{g \in Fil (X) \| F \subseteq g\} \leftrightarrow (x \subseteq Fil (X) \land \forall g \in x F \subseteq g)$
20	18 19	sylib	$⊢ (F \in Fil (X) \land (x \subseteq \{g \in Fil (X) \| F \subseteq g\} \land x \neq \emptyset \land [\subset] Or x)) \to (x \subseteq Fil (X) \land \forall g \in x F \subseteq g)$
21	20	simpld	$⊢ (F \in Fil (X) \land (x \subseteq \{g \in Fil (X) \| F \subseteq g\} \land x \neq \emptyset \land [\subset] Or x)) \to x \subseteq Fil (X)$
22		simpr2	$⊢ (F \in Fil (X) \land (x \subseteq \{g \in Fil (X) \| F \subseteq g\} \land x \neq \emptyset \land [\subset] Or x)) \to x \neq \emptyset$
23		simpr3	$⊢ (F \in Fil (X) \land (x \subseteq \{g \in Fil (X) \| F \subseteq g\} \land x \neq \emptyset \land [\subset] Or x)) \to [\subset] Or x$
24		sorpssun	$⊢ ([\subset] Or x \land (g \in x \land h \in x)) \to g \cup h \in x$
25	24	ralrimivva	$⊢ [\subset] Or x \to \forall g \in x \forall h \in x g \cup h \in x$
26	23 25	syl	$⊢ (F \in Fil (X) \land (x \subseteq \{g \in Fil (X) \| F \subseteq g\} \land x \neq \emptyset \land [\subset] Or x)) \to \forall g \in x \forall h \in x g \cup h \in x$
27		filuni	$⊢ (x \subseteq Fil (X) \land x \neq \emptyset \land \forall g \in x \forall h \in x g \cup h \in x) \to ⋃ x \in Fil (X)$
28	21 22 26 27	syl3anc	$⊢ (F \in Fil (X) \land (x \subseteq \{g \in Fil (X) \| F \subseteq g\} \land x \neq \emptyset \land [\subset] Or x)) \to ⋃ x \in Fil (X)$
29		n0	$⊢ x \neq \emptyset \leftrightarrow \exists h h \in x$
30		ssel2	$⊢ (x \subseteq \{g \in Fil (X) \| F \subseteq g\} \land h \in x) \to h \in \{g \in Fil (X) \| F \subseteq g\}$
31		sseq2	$⊢ g = h \to (F \subseteq g \leftrightarrow F \subseteq h)$
32	31	elrab	$⊢ h \in \{g \in Fil (X) \| F \subseteq g\} \leftrightarrow (h \in Fil (X) \land F \subseteq h)$
33	30 32	sylib	$⊢ (x \subseteq \{g \in Fil (X) \| F \subseteq g\} \land h \in x) \to (h \in Fil (X) \land F \subseteq h)$
34	33	simprd	$⊢ (x \subseteq \{g \in Fil (X) \| F \subseteq g\} \land h \in x) \to F \subseteq h$
35		ssuni	$⊢ (F \subseteq h \land h \in x) \to F \subseteq ⋃ x$
36	34 35	sylancom	$⊢ (x \subseteq \{g \in Fil (X) \| F \subseteq g\} \land h \in x) \to F \subseteq ⋃ x$
37	36	ex	$⊢ x \subseteq \{g \in Fil (X) \| F \subseteq g\} \to (h \in x \to F \subseteq ⋃ x)$
38	37	exlimdv	$⊢ x \subseteq \{g \in Fil (X) \| F \subseteq g\} \to (\exists h h \in x \to F \subseteq ⋃ x)$
39	29 38	biimtrid	$⊢ x \subseteq \{g \in Fil (X) \| F \subseteq g\} \to (x \neq \emptyset \to F \subseteq ⋃ x)$
40	18 22 39	sylc	$⊢ (F \in Fil (X) \land (x \subseteq \{g \in Fil (X) \| F \subseteq g\} \land x \neq \emptyset \land [\subset] Or x)) \to F \subseteq ⋃ x$
41	17 28 40	elrabd	$⊢ (F \in Fil (X) \land (x \subseteq \{g \in Fil (X) \| F \subseteq g\} \land x \neq \emptyset \land [\subset] Or x)) \to ⋃ x \in \{g \in Fil (X) \| F \subseteq g\}$
42	41	ex	$⊢ F \in Fil (X) \to ((x \subseteq \{g \in Fil (X) \| F \subseteq g\} \land x \neq \emptyset \land [\subset] Or x) \to ⋃ x \in \{g \in Fil (X) \| F \subseteq g\})$
43	42	alrimiv	$⊢ F \in Fil (X) \to \forall x ((x \subseteq \{g \in Fil (X) \| F \subseteq g\} \land x \neq \emptyset \land [\subset] Or x) \to ⋃ x \in \{g \in Fil (X) \| F \subseteq g\})$
44	43	adantr	$⊢ (F \in Fil (X) \land 𝒫 𝒫 X \in dom card) \to \forall x ((x \subseteq \{g \in Fil (X) \| F \subseteq g\} \land x \neq \emptyset \land [\subset] Or x) \to ⋃ x \in \{g \in Fil (X) \| F \subseteq g\})$
45		zornn0g	$⊢ (\{g \in Fil (X) \| F \subseteq g\} \in dom card \land \{g \in Fil (X) \| F \subseteq g\} \neq \emptyset \land \forall x ((x \subseteq \{g \in Fil (X) \| F \subseteq g\} \land x \neq \emptyset \land [\subset] Or x) \to ⋃ x \in \{g \in Fil (X) \| F \subseteq g\})) \to \exists f \in \{g \in Fil (X) \| F \subseteq g\} \forall h \in \{g \in Fil (X) \| F \subseteq g\} \neg f \subset h$
46	9 16 44 45	syl3anc	$⊢ (F \in Fil (X) \land 𝒫 𝒫 X \in dom card) \to \exists f \in \{g \in Fil (X) \| F \subseteq g\} \forall h \in \{g \in Fil (X) \| F \subseteq g\} \neg f \subset h$
47		sseq2	$⊢ g = f \to (F \subseteq g \leftrightarrow F \subseteq f)$
48	47	elrab	$⊢ f \in \{g \in Fil (X) \| F \subseteq g\} \leftrightarrow (f \in Fil (X) \land F \subseteq f)$
49	31	ralrab	$⊢ \forall h \in \{g \in Fil (X) \| F \subseteq g\} \neg f \subset h \leftrightarrow \forall h \in Fil (X) (F \subseteq h \to \neg f \subset h)$
50		simpll	$⊢ ((f \in Fil (X) \land F \subseteq f) \land \forall h \in Fil (X) (F \subseteq h \to \neg f \subset h)) \to f \in Fil (X)$
51		sstr2	$⊢ F \subseteq f \to (f \subseteq h \to F \subseteq h)$
52	51	imim1d	$⊢ F \subseteq f \to ((F \subseteq h \to \neg f \subset h) \to (f \subseteq h \to \neg f \subset h))$
53		df-pss	$⊢ f \subset h \leftrightarrow (f \subseteq h \land f \neq h)$
54	53	simplbi2	$⊢ f \subseteq h \to (f \neq h \to f \subset h)$
55	54	necon1bd	$⊢ f \subseteq h \to (\neg f \subset h \to f = h)$
56	55	a2i	$⊢ (f \subseteq h \to \neg f \subset h) \to (f \subseteq h \to f = h)$
57	52 56	syl6	$⊢ F \subseteq f \to ((F \subseteq h \to \neg f \subset h) \to (f \subseteq h \to f = h))$
58	57	ralimdv	$⊢ F \subseteq f \to (\forall h \in Fil (X) (F \subseteq h \to \neg f \subset h) \to \forall h \in Fil (X) (f \subseteq h \to f = h))$
59	58	imp	$⊢ (F \subseteq f \land \forall h \in Fil (X) (F \subseteq h \to \neg f \subset h)) \to \forall h \in Fil (X) (f \subseteq h \to f = h)$
60	59	adantll	$⊢ ((f \in Fil (X) \land F \subseteq f) \land \forall h \in Fil (X) (F \subseteq h \to \neg f \subset h)) \to \forall h \in Fil (X) (f \subseteq h \to f = h)$
61		isufil2	$⊢ f \in UFil (X) \leftrightarrow (f \in Fil (X) \land \forall h \in Fil (X) (f \subseteq h \to f = h))$
62	50 60 61	sylanbrc	$⊢ ((f \in Fil (X) \land F \subseteq f) \land \forall h \in Fil (X) (F \subseteq h \to \neg f \subset h)) \to f \in UFil (X)$
63		simplr	$⊢ ((f \in Fil (X) \land F \subseteq f) \land \forall h \in Fil (X) (F \subseteq h \to \neg f \subset h)) \to F \subseteq f$
64	62 63	jca	$⊢ ((f \in Fil (X) \land F \subseteq f) \land \forall h \in Fil (X) (F \subseteq h \to \neg f \subset h)) \to (f \in UFil (X) \land F \subseteq f)$
65	48 49 64	syl2anb	$⊢ (f \in \{g \in Fil (X) \| F \subseteq g\} \land \forall h \in \{g \in Fil (X) \| F \subseteq g\} \neg f \subset h) \to (f \in UFil (X) \land F \subseteq f)$
66	65	reximi2	$⊢ \exists f \in \{g \in Fil (X) \| F \subseteq g\} \forall h \in \{g \in Fil (X) \| F \subseteq g\} \neg f \subset h \to \exists f \in UFil (X) F \subseteq f$
67	46 66	syl	$⊢ (F \in Fil (X) \land 𝒫 𝒫 X \in dom card) \to \exists f \in UFil (X) F \subseteq f$

Metamath Proof Explorer

Theorem filssufilg

Proof