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	|- ( ( F e. ( UFil ` X ) /\ A e. |^| F ) -> { A } e. F )

Proof

Step	Hyp	Ref	Expression
1		eleq2	|- ( x = { A } -> ( A e. x <-> A e. { A } ) )
2		ufilfil	|- ( F e. ( UFil ` X ) -> F e. ( Fil ` X ) )
3		filn0	|- ( F e. ( Fil ` X ) -> F =/= (/) )
4		intssuni	|- ( F =/= (/) -> |^| F C_ U. F )
5	2 3 4	3syl	|- ( F e. ( UFil ` X ) -> |^| F C_ U. F )
6		filunibas	|- ( F e. ( Fil ` X ) -> U. F = X )
7	2 6	syl	|- ( F e. ( UFil ` X ) -> U. F = X )
8	5 7	sseqtrd	|- ( F e. ( UFil ` X ) -> |^| F C_ X )
9	8	sselda	|- ( ( F e. ( UFil ` X ) /\ A e. |^| F ) -> A e. X )
10	9	snssd	|- ( ( F e. ( UFil ` X ) /\ A e. |^| F ) -> { A } C_ X )
11		snex	|- { A } e. _V
12	11	elpw	|- ( { A } e. ~P X <-> { A } C_ X )
13	10 12	sylibr	|- ( ( F e. ( UFil ` X ) /\ A e. |^| F ) -> { A } e. ~P X )
14		snidg	|- ( A e. |^| F -> A e. { A } )
15	14	adantl	|- ( ( F e. ( UFil ` X ) /\ A e. |^| F ) -> A e. { A } )
16	1 13 15	elrabd	|- ( ( F e. ( UFil ` X ) /\ A e. |^| F ) -> { A } e. { x e. ~P X | A e. x } )
17		uffixfr	|- ( F e. ( UFil ` X ) -> ( A e. |^| F <-> F = { x e. ~P X | A e. x } ) )
18	17	biimpa	|- ( ( F e. ( UFil ` X ) /\ A e. |^| F ) -> F = { x e. ~P X | A e. x } )
19	16 18	eleqtrrd	|- ( ( F e. ( UFil ` X ) /\ A e. |^| F ) -> { A } e. F )