ufinffr

Description: An infinite subset is contained in a free ultrafilter. (Contributed by Jeff Hankins, 6-Dec-2009) (Revised by Mario Carneiro, 4-Dec-2013)

		Ref	Expression
	Assertion	ufinffr	$⊢ (X \in B \land A \subseteq X \land ω ≼ A) \to \exists f \in UFil (X) (A \in f \land ⋂ f = \emptyset)$

Proof

Step	Hyp	Ref	Expression
1		ominf	$⊢ \neg ω \in Fin$
2		domfi	$⊢ (A \in Fin \land ω ≼ A) \to ω \in Fin$
3	2	expcom	$⊢ ω ≼ A \to (A \in Fin \to ω \in Fin)$
4	1 3	mtoi	$⊢ ω ≼ A \to \neg A \in Fin$
5		cfinfil	$⊢ (X \in B \land A \subseteq X \land \neg A \in Fin) \to \{x \in 𝒫 X \| A ∖ x \in Fin\} \in Fil (X)$
6	4 5	syl3an3	$⊢ (X \in B \land A \subseteq X \land ω ≼ A) \to \{x \in 𝒫 X \| A ∖ x \in Fin\} \in Fil (X)$
7		filssufil	$⊢ \{x \in 𝒫 X \| A ∖ x \in Fin\} \in Fil (X) \to \exists f \in UFil (X) \{x \in 𝒫 X \| A ∖ x \in Fin\} \subseteq f$
8	6 7	syl	$⊢ (X \in B \land A \subseteq X \land ω ≼ A) \to \exists f \in UFil (X) \{x \in 𝒫 X \| A ∖ x \in Fin\} \subseteq f$
9		difeq2	$⊢ x = A \to A ∖ x = A ∖ A$
10		difid	$⊢ A ∖ A = \emptyset$
11	9 10	syl6eq	$⊢ x = A \to A ∖ x = \emptyset$
12	11	eleq1d	$⊢ x = A \to (A ∖ x \in Fin \leftrightarrow \emptyset \in Fin)$
13		elpw2g	$⊢ X \in B \to (A \in 𝒫 X \leftrightarrow A \subseteq X)$
14	13	biimpar	$⊢ (X \in B \land A \subseteq X) \to A \in 𝒫 X$
15	14	3adant3	$⊢ (X \in B \land A \subseteq X \land ω ≼ A) \to A \in 𝒫 X$
16		0fin	$⊢ \emptyset \in Fin$
17	16	a1i	$⊢ (X \in B \land A \subseteq X \land ω ≼ A) \to \emptyset \in Fin$
18	12 15 17	elrabd	$⊢ (X \in B \land A \subseteq X \land ω ≼ A) \to A \in \{x \in 𝒫 X \| A ∖ x \in Fin\}$
19		ssel	$⊢ \{x \in 𝒫 X \| A ∖ x \in Fin\} \subseteq f \to (A \in \{x \in 𝒫 X \| A ∖ x \in Fin\} \to A \in f)$
20	18 19	syl5com	$⊢ (X \in B \land A \subseteq X \land ω ≼ A) \to (\{x \in 𝒫 X \| A ∖ x \in Fin\} \subseteq f \to A \in f)$
21		intss	$⊢ \{x \in 𝒫 X \| A ∖ x \in Fin\} \subseteq f \to ⋂ f \subseteq ⋂ \{x \in 𝒫 X \| A ∖ x \in Fin\}$
22		neldifsn	$⊢ \neg y \in (A ∖ \{y\})$
23		elinti	$⊢ y \in ⋂ \{x \in 𝒫 X \| A ∖ x \in Fin\} \to (A ∖ \{y\} \in \{x \in 𝒫 X \| A ∖ x \in Fin\} \to y \in (A ∖ \{y\}))$
24	22 23	mtoi	$⊢ y \in ⋂ \{x \in 𝒫 X \| A ∖ x \in Fin\} \to \neg A ∖ \{y\} \in \{x \in 𝒫 X \| A ∖ x \in Fin\}$
25		difeq2	$⊢ x = A ∖ \{y\} \to A ∖ x = A ∖ (A ∖ \{y\})$
26	25	eleq1d	$⊢ x = A ∖ \{y\} \to (A ∖ x \in Fin \leftrightarrow A ∖ (A ∖ \{y\}) \in Fin)$
27		simp2	$⊢ (X \in B \land A \subseteq X \land ω ≼ A) \to A \subseteq X$
28	27	ssdifssd	$⊢ (X \in B \land A \subseteq X \land ω ≼ A) \to A ∖ \{y\} \subseteq X$
29		elpw2g	$⊢ X \in B \to (A ∖ \{y\} \in 𝒫 X \leftrightarrow A ∖ \{y\} \subseteq X)$
30	29	3ad2ant1	$⊢ (X \in B \land A \subseteq X \land ω ≼ A) \to (A ∖ \{y\} \in 𝒫 X \leftrightarrow A ∖ \{y\} \subseteq X)$
31	28 30	mpbird	$⊢ (X \in B \land A \subseteq X \land ω ≼ A) \to A ∖ \{y\} \in 𝒫 X$
32		snfi	$⊢ \{y\} \in Fin$
33		eldif	$⊢ x \in (A ∖ (A ∖ \{y\})) \leftrightarrow (x \in A \land \neg x \in (A ∖ \{y\}))$
34		eldif	$⊢ x \in (A ∖ \{y\}) \leftrightarrow (x \in A \land \neg x \in \{y\})$
35	34	notbii	$⊢ \neg x \in (A ∖ \{y\}) \leftrightarrow \neg (x \in A \land \neg x \in \{y\})$
36		iman	$⊢ (x \in A \to x \in \{y\}) \leftrightarrow \neg (x \in A \land \neg x \in \{y\})$
37	35 36	bitr4i	$⊢ \neg x \in (A ∖ \{y\}) \leftrightarrow (x \in A \to x \in \{y\})$
38	37	anbi2i	$⊢ (x \in A \land \neg x \in (A ∖ \{y\})) \leftrightarrow (x \in A \land (x \in A \to x \in \{y\}))$
39	33 38	bitri	$⊢ x \in (A ∖ (A ∖ \{y\})) \leftrightarrow (x \in A \land (x \in A \to x \in \{y\}))$
40		pm3.35	$⊢ (x \in A \land (x \in A \to x \in \{y\})) \to x \in \{y\}$
41	39 40	sylbi	$⊢ x \in (A ∖ (A ∖ \{y\})) \to x \in \{y\}$
42	41	ssriv	$⊢ A ∖ (A ∖ \{y\}) \subseteq \{y\}$
43		ssfi	$⊢ (\{y\} \in Fin \land A ∖ (A ∖ \{y\}) \subseteq \{y\}) \to A ∖ (A ∖ \{y\}) \in Fin$
44	32 42 43	mp2an	$⊢ A ∖ (A ∖ \{y\}) \in Fin$
45	44	a1i	$⊢ (X \in B \land A \subseteq X \land ω ≼ A) \to A ∖ (A ∖ \{y\}) \in Fin$
46	26 31 45	elrabd	$⊢ (X \in B \land A \subseteq X \land ω ≼ A) \to A ∖ \{y\} \in \{x \in 𝒫 X \| A ∖ x \in Fin\}$
47	24 46	nsyl3	$⊢ (X \in B \land A \subseteq X \land ω ≼ A) \to \neg y \in ⋂ \{x \in 𝒫 X \| A ∖ x \in Fin\}$
48	47	eq0rdv	$⊢ (X \in B \land A \subseteq X \land ω ≼ A) \to ⋂ \{x \in 𝒫 X \| A ∖ x \in Fin\} = \emptyset$
49	48	sseq2d	$⊢ (X \in B \land A \subseteq X \land ω ≼ A) \to (⋂ f \subseteq ⋂ \{x \in 𝒫 X \| A ∖ x \in Fin\} \leftrightarrow ⋂ f \subseteq \emptyset)$
50	21 49	syl5ib	$⊢ (X \in B \land A \subseteq X \land ω ≼ A) \to (\{x \in 𝒫 X \| A ∖ x \in Fin\} \subseteq f \to ⋂ f \subseteq \emptyset)$
51		ss0	$⊢ ⋂ f \subseteq \emptyset \to ⋂ f = \emptyset$
52	50 51	syl6	$⊢ (X \in B \land A \subseteq X \land ω ≼ A) \to (\{x \in 𝒫 X \| A ∖ x \in Fin\} \subseteq f \to ⋂ f = \emptyset)$
53	20 52	jcad	$⊢ (X \in B \land A \subseteq X \land ω ≼ A) \to (\{x \in 𝒫 X \| A ∖ x \in Fin\} \subseteq f \to (A \in f \land ⋂ f = \emptyset))$
54	53	reximdv	$⊢ (X \in B \land A \subseteq X \land ω ≼ A) \to (\exists f \in UFil (X) \{x \in 𝒫 X \| A ∖ x \in Fin\} \subseteq f \to \exists f \in UFil (X) (A \in f \land ⋂ f = \emptyset))$
55	8 54	mpd	$⊢ (X \in B \land A \subseteq X \land ω ≼ A) \to \exists f \in UFil (X) (A \in f \land ⋂ f = \emptyset)$

Metamath Proof Explorer

Theorem ufinffr

Proof