fixufil

Description: The condition describing a fixed ultrafilter always produces an ultrafilter. (Contributed by Jeff Hankins, 9-Dec-2009) (Revised by Mario Carneiro, 12-Dec-2013) (Revised by Stefan O'Rear, 29-Jul-2015)

		Ref	Expression
	Assertion	fixufil	$⊢ (X \in V \land A \in X) \to \{x \in 𝒫 X \| A \in x\} \in UFil (X)$

Proof

Step	Hyp	Ref	Expression
1		uffix	$⊢ (X \in V \land A \in X) \to (\{\{A\}\} \in fBas (X) \land \{x \in 𝒫 X \| A \in x\} = X filGen \{\{A\}\})$
2	1	simprd	$⊢ (X \in V \land A \in X) \to \{x \in 𝒫 X \| A \in x\} = X filGen \{\{A\}\}$
3	1	simpld	$⊢ (X \in V \land A \in X) \to \{\{A\}\} \in fBas (X)$
4		fgcl	$⊢ \{\{A\}\} \in fBas (X) \to X filGen \{\{A\}\} \in Fil (X)$
5	3 4	syl	$⊢ (X \in V \land A \in X) \to X filGen \{\{A\}\} \in Fil (X)$
6	2 5	eqeltrd	$⊢ (X \in V \land A \in X) \to \{x \in 𝒫 X \| A \in x\} \in Fil (X)$
7		undif2	$⊢ y \cup (X ∖ y) = y \cup X$
8		elpwi	$⊢ y \in 𝒫 X \to y \subseteq X$
9		ssequn1	$⊢ y \subseteq X \leftrightarrow y \cup X = X$
10	8 9	sylib	$⊢ y \in 𝒫 X \to y \cup X = X$
11	7 10	syl5req	$⊢ y \in 𝒫 X \to X = y \cup (X ∖ y)$
12	11	eleq2d	$⊢ y \in 𝒫 X \to (A \in X \leftrightarrow A \in (y \cup (X ∖ y)))$
13	12	biimpac	$⊢ (A \in X \land y \in 𝒫 X) \to A \in (y \cup (X ∖ y))$
14		elun	$⊢ A \in (y \cup (X ∖ y)) \leftrightarrow (A \in y \lor A \in (X ∖ y))$
15	13 14	sylib	$⊢ (A \in X \land y \in 𝒫 X) \to (A \in y \lor A \in (X ∖ y))$
16	15	adantll	$⊢ ((X \in V \land A \in X) \land y \in 𝒫 X) \to (A \in y \lor A \in (X ∖ y))$
17		ibar	$⊢ y \in 𝒫 X \to (A \in y \leftrightarrow (y \in 𝒫 X \land A \in y))$
18	17	adantl	$⊢ ((X \in V \land A \in X) \land y \in 𝒫 X) \to (A \in y \leftrightarrow (y \in 𝒫 X \land A \in y))$
19		difss	$⊢ X ∖ y \subseteq X$
20		elpw2g	$⊢ X \in V \to (X ∖ y \in 𝒫 X \leftrightarrow X ∖ y \subseteq X)$
21	19 20	mpbiri	$⊢ X \in V \to X ∖ y \in 𝒫 X$
22	21	ad2antrr	$⊢ ((X \in V \land A \in X) \land y \in 𝒫 X) \to X ∖ y \in 𝒫 X$
23	22	biantrurd	$⊢ ((X \in V \land A \in X) \land y \in 𝒫 X) \to (A \in (X ∖ y) \leftrightarrow (X ∖ y \in 𝒫 X \land A \in (X ∖ y)))$
24	18 23	orbi12d	$⊢ ((X \in V \land A \in X) \land y \in 𝒫 X) \to ((A \in y \lor A \in (X ∖ y)) \leftrightarrow ((y \in 𝒫 X \land A \in y) \lor (X ∖ y \in 𝒫 X \land A \in (X ∖ y))))$
25	16 24	mpbid	$⊢ ((X \in V \land A \in X) \land y \in 𝒫 X) \to ((y \in 𝒫 X \land A \in y) \lor (X ∖ y \in 𝒫 X \land A \in (X ∖ y)))$
26	25	ralrimiva	$⊢ (X \in V \land A \in X) \to \forall y \in 𝒫 X ((y \in 𝒫 X \land A \in y) \lor (X ∖ y \in 𝒫 X \land A \in (X ∖ y)))$
27		eleq2	$⊢ x = y \to (A \in x \leftrightarrow A \in y)$
28	27	elrab	$⊢ y \in \{x \in 𝒫 X \| A \in x\} \leftrightarrow (y \in 𝒫 X \land A \in y)$
29		eleq2	$⊢ x = X ∖ y \to (A \in x \leftrightarrow A \in (X ∖ y))$
30	29	elrab	$⊢ X ∖ y \in \{x \in 𝒫 X \| A \in x\} \leftrightarrow (X ∖ y \in 𝒫 X \land A \in (X ∖ y))$
31	28 30	orbi12i	$⊢ (y \in \{x \in 𝒫 X \| A \in x\} \lor X ∖ y \in \{x \in 𝒫 X \| A \in x\}) \leftrightarrow ((y \in 𝒫 X \land A \in y) \lor (X ∖ y \in 𝒫 X \land A \in (X ∖ y)))$
32	31	ralbii	$⊢ \forall y \in 𝒫 X (y \in \{x \in 𝒫 X \| A \in x\} \lor X ∖ y \in \{x \in 𝒫 X \| A \in x\}) \leftrightarrow \forall y \in 𝒫 X ((y \in 𝒫 X \land A \in y) \lor (X ∖ y \in 𝒫 X \land A \in (X ∖ y)))$
33	26 32	sylibr	$⊢ (X \in V \land A \in X) \to \forall y \in 𝒫 X (y \in \{x \in 𝒫 X \| A \in x\} \lor X ∖ y \in \{x \in 𝒫 X \| A \in x\})$
34		isufil	$⊢ \{x \in 𝒫 X \| A \in x\} \in UFil (X) \leftrightarrow (\{x \in 𝒫 X \| A \in x\} \in Fil (X) \land \forall y \in 𝒫 X (y \in \{x \in 𝒫 X \| A \in x\} \lor X ∖ y \in \{x \in 𝒫 X \| A \in x\}))$
35	6 33 34	sylanbrc	$⊢ (X \in V \land A \in X) \to \{x \in 𝒫 X \| A \in x\} \in UFil (X)$

Metamath Proof Explorer

Theorem fixufil

Proof