Theorem uffixsn

Description: The singleton of the generator of a fixed ultrafilter is in the filter. (Contributed by Mario Carneiro, 24-May-2015) (Revised by Stefan O'Rear, 2-Aug-2015)

	Ref	Expression
Assertion	uffixsn	⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝐴 ∈ ∩ 𝐹 ) → { 𝐴 } ∈ 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		eleq2	⊢ ( 𝑥 = { 𝐴 } → ( 𝐴 ∈ 𝑥 ↔ 𝐴 ∈ { 𝐴 } ) )
2		ufilfil	⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → 𝐹 ∈ ( Fil ‘ 𝑋 ) )
3		filn0	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝐹 ≠ ∅ )
4		intssuni	⊢ ( 𝐹 ≠ ∅ → ∩ 𝐹 ⊆ ∪ 𝐹 )
5	2 3 4	3syl	⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ∩ 𝐹 ⊆ ∪ 𝐹 )
6		filunibas	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ∪ 𝐹 = 𝑋 )
7	2 6	syl	⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ∪ 𝐹 = 𝑋 )
8	5 7	sseqtrd	⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ∩ 𝐹 ⊆ 𝑋 )
9	8	sselda	⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝐴 ∈ ∩ 𝐹 ) → 𝐴 ∈ 𝑋 )
10	9	snssd	⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝐴 ∈ ∩ 𝐹 ) → { 𝐴 } ⊆ 𝑋 )
11		snex	⊢ { 𝐴 } ∈ V
12	11	elpw	⊢ ( { 𝐴 } ∈ 𝒫 𝑋 ↔ { 𝐴 } ⊆ 𝑋 )
13	10 12	sylibr	⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝐴 ∈ ∩ 𝐹 ) → { 𝐴 } ∈ 𝒫 𝑋 )
14		snidg	⊢ ( 𝐴 ∈ ∩ 𝐹 → 𝐴 ∈ { 𝐴 } )
15	14	adantl	⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝐴 ∈ ∩ 𝐹 ) → 𝐴 ∈ { 𝐴 } )
16	1 13 15	elrabd	⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝐴 ∈ ∩ 𝐹 ) → { 𝐴 } ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } )
17		uffixfr	⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ( 𝐴 ∈ ∩ 𝐹 ↔ 𝐹 = { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } ) )
18	17	biimpa	⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝐴 ∈ ∩ 𝐹 ) → 𝐹 = { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } )
19	16 18	eleqtrrd	⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝐴 ∈ ∩ 𝐹 ) → { 𝐴 } ∈ 𝐹 )