Metamath Proof Explorer

Theorem ufilmax

Description: Any filter finer than an ultrafilter is actually equal to it. (Contributed by Jeff Hankins, 1-Dec-2009) (Revised by Mario Carneiro, 29-Jul-2015)

Ref Expression
Assertion ufilmax 
|- ( ( F e. ( UFil ` X ) /\ G e. ( Fil ` X ) /\ F C_ G ) -> F = G )

Proof

Step Hyp Ref Expression
1 simp3 
 |-  ( ( F e. ( UFil ` X ) /\ G e. ( Fil ` X ) /\ F C_ G ) -> F C_ G )
2 filelss 
 |-  ( ( G e. ( Fil ` X ) /\ x e. G ) -> x C_ X )
3 2 ex 
 |-  ( G e. ( Fil ` X ) -> ( x e. G -> x C_ X ) )
4 3 3ad2ant2 
 |-  ( ( F e. ( UFil ` X ) /\ G e. ( Fil ` X ) /\ F C_ G ) -> ( x e. G -> x C_ X ) )
5 ufilb 
 |-  ( ( F e. ( UFil ` X ) /\ x C_ X ) -> ( -. x e. F <-> ( X \ x ) e. F ) )
6 5 3ad2antl1 
 |-  ( ( ( F e. ( UFil ` X ) /\ G e. ( Fil ` X ) /\ F C_ G ) /\ x C_ X ) -> ( -. x e. F <-> ( X \ x ) e. F ) )
7 simpl3 
 |-  ( ( ( F e. ( UFil ` X ) /\ G e. ( Fil ` X ) /\ F C_ G ) /\ x C_ X ) -> F C_ G )
8 7 sseld 
 |-  ( ( ( F e. ( UFil ` X ) /\ G e. ( Fil ` X ) /\ F C_ G ) /\ x C_ X ) -> ( ( X \ x ) e. F -> ( X \ x ) e. G ) )
9 filfbas 
 |-  ( G e. ( Fil ` X ) -> G e. ( fBas ` X ) )
10 fbncp 
 |-  ( ( G e. ( fBas ` X ) /\ x e. G ) -> -. ( X \ x ) e. G )
11 10 ex 
 |-  ( G e. ( fBas ` X ) -> ( x e. G -> -. ( X \ x ) e. G ) )
12 9 11 syl 
 |-  ( G e. ( Fil ` X ) -> ( x e. G -> -. ( X \ x ) e. G ) )
13 12 con2d 
 |-  ( G e. ( Fil ` X ) -> ( ( X \ x ) e. G -> -. x e. G ) )
14 13 3ad2ant2 
 |-  ( ( F e. ( UFil ` X ) /\ G e. ( Fil ` X ) /\ F C_ G ) -> ( ( X \ x ) e. G -> -. x e. G ) )
15 14 adantr 
 |-  ( ( ( F e. ( UFil ` X ) /\ G e. ( Fil ` X ) /\ F C_ G ) /\ x C_ X ) -> ( ( X \ x ) e. G -> -. x e. G ) )
16 8 15 syld 
 |-  ( ( ( F e. ( UFil ` X ) /\ G e. ( Fil ` X ) /\ F C_ G ) /\ x C_ X ) -> ( ( X \ x ) e. F -> -. x e. G ) )
17 6 16 sylbid 
 |-  ( ( ( F e. ( UFil ` X ) /\ G e. ( Fil ` X ) /\ F C_ G ) /\ x C_ X ) -> ( -. x e. F -> -. x e. G ) )
18 17 con4d 
 |-  ( ( ( F e. ( UFil ` X ) /\ G e. ( Fil ` X ) /\ F C_ G ) /\ x C_ X ) -> ( x e. G -> x e. F ) )
19 18 ex 
 |-  ( ( F e. ( UFil ` X ) /\ G e. ( Fil ` X ) /\ F C_ G ) -> ( x C_ X -> ( x e. G -> x e. F ) ) )
20 19 com23 
 |-  ( ( F e. ( UFil ` X ) /\ G e. ( Fil ` X ) /\ F C_ G ) -> ( x e. G -> ( x C_ X -> x e. F ) ) )
21 4 20 mpdd 
 |-  ( ( F e. ( UFil ` X ) /\ G e. ( Fil ` X ) /\ F C_ G ) -> ( x e. G -> x e. F ) )
22 21 ssrdv 
 |-  ( ( F e. ( UFil ` X ) /\ G e. ( Fil ` X ) /\ F C_ G ) -> G C_ F )
23 1 22 eqssd 
 |-  ( ( F e. ( UFil ` X ) /\ G e. ( Fil ` X ) /\ F C_ G ) -> F = G )