Metamath Proof Explorer


Theorem uffinfix

Description: An ultrafilter containing a finite element is fixed. (Contributed by Jeff Hankins, 5-Dec-2009) (Revised by Stefan O'Rear, 2-Aug-2015)

Ref Expression
Assertion uffinfix FUFilXSFSFinxXF=y𝒫X|xy

Proof

Step Hyp Ref Expression
1 ufilfil FUFilXFFilX
2 filfinnfr FFilXSFSFinF
3 1 2 syl3an1 FUFilXSFSFinF
4 uffix2 FUFilXFxXF=y𝒫X|xy
5 4 3ad2ant1 FUFilXSFSFinFxXF=y𝒫X|xy
6 3 5 mpbid FUFilXSFSFinxXF=y𝒫X|xy