Theorem 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	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ) → { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } ∈ ( UFil ‘ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		uffix	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ) → ( { { 𝐴 } } ∈ ( fBas ‘ 𝑋 ) ∧ { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } = ( 𝑋 filGen { { 𝐴 } } ) ) )
2	1	simprd	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ) → { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } = ( 𝑋 filGen { { 𝐴 } } ) )
3	1	simpld	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ) → { { 𝐴 } } ∈ ( fBas ‘ 𝑋 ) )
4		fgcl	⊢ ( { { 𝐴 } } ∈ ( fBas ‘ 𝑋 ) → ( 𝑋 filGen { { 𝐴 } } ) ∈ ( Fil ‘ 𝑋 ) )
5	3 4	syl	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ) → ( 𝑋 filGen { { 𝐴 } } ) ∈ ( Fil ‘ 𝑋 ) )
6	2 5	eqeltrd	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ) → { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } ∈ ( Fil ‘ 𝑋 ) )
7		undif2	⊢ ( 𝑦 ∪ ( 𝑋 ∖ 𝑦 ) ) = ( 𝑦 ∪ 𝑋 )
8		elpwi	⊢ ( 𝑦 ∈ 𝒫 𝑋 → 𝑦 ⊆ 𝑋 )
9		ssequn1	⊢ ( 𝑦 ⊆ 𝑋 ↔ ( 𝑦 ∪ 𝑋 ) = 𝑋 )
10	8 9	sylib	⊢ ( 𝑦 ∈ 𝒫 𝑋 → ( 𝑦 ∪ 𝑋 ) = 𝑋 )
11	7 10	syl5req	⊢ ( 𝑦 ∈ 𝒫 𝑋 → 𝑋 = ( 𝑦 ∪ ( 𝑋 ∖ 𝑦 ) ) )
12	11	eleq2d	⊢ ( 𝑦 ∈ 𝒫 𝑋 → ( 𝐴 ∈ 𝑋 ↔ 𝐴 ∈ ( 𝑦 ∪ ( 𝑋 ∖ 𝑦 ) ) ) )
13	12	biimpac	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝒫 𝑋 ) → 𝐴 ∈ ( 𝑦 ∪ ( 𝑋 ∖ 𝑦 ) ) )
14		elun	⊢ ( 𝐴 ∈ ( 𝑦 ∪ ( 𝑋 ∖ 𝑦 ) ) ↔ ( 𝐴 ∈ 𝑦 ∨ 𝐴 ∈ ( 𝑋 ∖ 𝑦 ) ) )
15	13 14	sylib	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝒫 𝑋 ) → ( 𝐴 ∈ 𝑦 ∨ 𝐴 ∈ ( 𝑋 ∖ 𝑦 ) ) )
16	15	adantll	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝒫 𝑋 ) → ( 𝐴 ∈ 𝑦 ∨ 𝐴 ∈ ( 𝑋 ∖ 𝑦 ) ) )
17		ibar	⊢ ( 𝑦 ∈ 𝒫 𝑋 → ( 𝐴 ∈ 𝑦 ↔ ( 𝑦 ∈ 𝒫 𝑋 ∧ 𝐴 ∈ 𝑦 ) ) )
18	17	adantl	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝒫 𝑋 ) → ( 𝐴 ∈ 𝑦 ↔ ( 𝑦 ∈ 𝒫 𝑋 ∧ 𝐴 ∈ 𝑦 ) ) )
19		difss	⊢ ( 𝑋 ∖ 𝑦 ) ⊆ 𝑋
20		elpw2g	⊢ ( 𝑋 ∈ 𝑉 → ( ( 𝑋 ∖ 𝑦 ) ∈ 𝒫 𝑋 ↔ ( 𝑋 ∖ 𝑦 ) ⊆ 𝑋 ) )
21	19 20	mpbiri	⊢ ( 𝑋 ∈ 𝑉 → ( 𝑋 ∖ 𝑦 ) ∈ 𝒫 𝑋 )
22	21	ad2antrr	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝒫 𝑋 ) → ( 𝑋 ∖ 𝑦 ) ∈ 𝒫 𝑋 )
23	22	biantrurd	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝒫 𝑋 ) → ( 𝐴 ∈ ( 𝑋 ∖ 𝑦 ) ↔ ( ( 𝑋 ∖ 𝑦 ) ∈ 𝒫 𝑋 ∧ 𝐴 ∈ ( 𝑋 ∖ 𝑦 ) ) ) )
24	18 23	orbi12d	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝒫 𝑋 ) → ( ( 𝐴 ∈ 𝑦 ∨ 𝐴 ∈ ( 𝑋 ∖ 𝑦 ) ) ↔ ( ( 𝑦 ∈ 𝒫 𝑋 ∧ 𝐴 ∈ 𝑦 ) ∨ ( ( 𝑋 ∖ 𝑦 ) ∈ 𝒫 𝑋 ∧ 𝐴 ∈ ( 𝑋 ∖ 𝑦 ) ) ) ) )
25	16 24	mpbid	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝒫 𝑋 ) → ( ( 𝑦 ∈ 𝒫 𝑋 ∧ 𝐴 ∈ 𝑦 ) ∨ ( ( 𝑋 ∖ 𝑦 ) ∈ 𝒫 𝑋 ∧ 𝐴 ∈ ( 𝑋 ∖ 𝑦 ) ) ) )
26	25	ralrimiva	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ) → ∀ 𝑦 ∈ 𝒫 𝑋 ( ( 𝑦 ∈ 𝒫 𝑋 ∧ 𝐴 ∈ 𝑦 ) ∨ ( ( 𝑋 ∖ 𝑦 ) ∈ 𝒫 𝑋 ∧ 𝐴 ∈ ( 𝑋 ∖ 𝑦 ) ) ) )
27		eleq2	⊢ ( 𝑥 = 𝑦 → ( 𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑦 ) )
28	27	elrab	⊢ ( 𝑦 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } ↔ ( 𝑦 ∈ 𝒫 𝑋 ∧ 𝐴 ∈ 𝑦 ) )
29		eleq2	⊢ ( 𝑥 = ( 𝑋 ∖ 𝑦 ) → ( 𝐴 ∈ 𝑥 ↔ 𝐴 ∈ ( 𝑋 ∖ 𝑦 ) ) )
30	29	elrab	⊢ ( ( 𝑋 ∖ 𝑦 ) ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } ↔ ( ( 𝑋 ∖ 𝑦 ) ∈ 𝒫 𝑋 ∧ 𝐴 ∈ ( 𝑋 ∖ 𝑦 ) ) )
31	28 30	orbi12i	⊢ ( ( 𝑦 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } ∨ ( 𝑋 ∖ 𝑦 ) ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } ) ↔ ( ( 𝑦 ∈ 𝒫 𝑋 ∧ 𝐴 ∈ 𝑦 ) ∨ ( ( 𝑋 ∖ 𝑦 ) ∈ 𝒫 𝑋 ∧ 𝐴 ∈ ( 𝑋 ∖ 𝑦 ) ) ) )
32	31	ralbii	⊢ ( ∀ 𝑦 ∈ 𝒫 𝑋 ( 𝑦 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } ∨ ( 𝑋 ∖ 𝑦 ) ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } ) ↔ ∀ 𝑦 ∈ 𝒫 𝑋 ( ( 𝑦 ∈ 𝒫 𝑋 ∧ 𝐴 ∈ 𝑦 ) ∨ ( ( 𝑋 ∖ 𝑦 ) ∈ 𝒫 𝑋 ∧ 𝐴 ∈ ( 𝑋 ∖ 𝑦 ) ) ) )
33	26 32	sylibr	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ) → ∀ 𝑦 ∈ 𝒫 𝑋 ( 𝑦 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } ∨ ( 𝑋 ∖ 𝑦 ) ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } ) )
34		isufil	⊢ ( { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } ∈ ( UFil ‘ 𝑋 ) ↔ ( { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } ∈ ( Fil ‘ 𝑋 ) ∧ ∀ 𝑦 ∈ 𝒫 𝑋 ( 𝑦 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } ∨ ( 𝑋 ∖ 𝑦 ) ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } ) ) )
35	6 33 34	sylanbrc	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ) → { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } ∈ ( UFil ‘ 𝑋 ) )