Metamath Proof Explorer

Theorem ufprim

Description: An ultrafilter is a prime filter. (Contributed by Jeff Hankins, 1-Jan-2010) (Revised by Mario Carneiro, 2-Aug-2015)

Ref Expression
Assertion ufprim 
|- ( ( F e. ( UFil ` X ) /\ A C_ X /\ B C_ X ) -> ( ( A e. F \/ B e. F ) <-> ( A u. B ) e. F ) )

Proof

Step Hyp Ref Expression
1 ufilfil 
 |-  ( F e. ( UFil ` X ) -> F e. ( Fil ` X ) )
2 1 3ad2ant1 
 |-  ( ( F e. ( UFil ` X ) /\ A C_ X /\ B C_ X ) -> F e. ( Fil ` X ) )
3 2 adantr 
 |-  ( ( ( F e. ( UFil ` X ) /\ A C_ X /\ B C_ X ) /\ A e. F ) -> F e. ( Fil ` X ) )
4 simpr 
 |-  ( ( ( F e. ( UFil ` X ) /\ A C_ X /\ B C_ X ) /\ A e. F ) -> A e. F )
5 unss 
 |-  ( ( A C_ X /\ B C_ X ) <-> ( A u. B ) C_ X )
6 5 biimpi 
 |-  ( ( A C_ X /\ B C_ X ) -> ( A u. B ) C_ X )
7 6 3adant1 
 |-  ( ( F e. ( UFil ` X ) /\ A C_ X /\ B C_ X ) -> ( A u. B ) C_ X )
8 7 adantr 
 |-  ( ( ( F e. ( UFil ` X ) /\ A C_ X /\ B C_ X ) /\ A e. F ) -> ( A u. B ) C_ X )
9 ssun1 
 |-  A C_ ( A u. B )
10 9 a1i 
 |-  ( ( ( F e. ( UFil ` X ) /\ A C_ X /\ B C_ X ) /\ A e. F ) -> A C_ ( A u. B ) )
11 filss 
 |-  ( ( F e. ( Fil ` X ) /\ ( A e. F /\ ( A u. B ) C_ X /\ A C_ ( A u. B ) ) ) -> ( A u. B ) e. F )
12 3 4 8 10 11 syl13anc 
 |-  ( ( ( F e. ( UFil ` X ) /\ A C_ X /\ B C_ X ) /\ A e. F ) -> ( A u. B ) e. F )
13 12 ex 
 |-  ( ( F e. ( UFil ` X ) /\ A C_ X /\ B C_ X ) -> ( A e. F -> ( A u. B ) e. F ) )
14 2 adantr 
 |-  ( ( ( F e. ( UFil ` X ) /\ A C_ X /\ B C_ X ) /\ B e. F ) -> F e. ( Fil ` X ) )
15 simpr 
 |-  ( ( ( F e. ( UFil ` X ) /\ A C_ X /\ B C_ X ) /\ B e. F ) -> B e. F )
16 7 adantr 
 |-  ( ( ( F e. ( UFil ` X ) /\ A C_ X /\ B C_ X ) /\ B e. F ) -> ( A u. B ) C_ X )
17 ssun2 
 |-  B C_ ( A u. B )
18 17 a1i 
 |-  ( ( ( F e. ( UFil ` X ) /\ A C_ X /\ B C_ X ) /\ B e. F ) -> B C_ ( A u. B ) )
19 filss 
 |-  ( ( F e. ( Fil ` X ) /\ ( B e. F /\ ( A u. B ) C_ X /\ B C_ ( A u. B ) ) ) -> ( A u. B ) e. F )
20 14 15 16 18 19 syl13anc 
 |-  ( ( ( F e. ( UFil ` X ) /\ A C_ X /\ B C_ X ) /\ B e. F ) -> ( A u. B ) e. F )
21 20 ex 
 |-  ( ( F e. ( UFil ` X ) /\ A C_ X /\ B C_ X ) -> ( B e. F -> ( A u. B ) e. F ) )
22 13 21 jaod 
 |-  ( ( F e. ( UFil ` X ) /\ A C_ X /\ B C_ X ) -> ( ( A e. F \/ B e. F ) -> ( A u. B ) e. F ) )
23 ufilb 
 |-  ( ( F e. ( UFil ` X ) /\ A C_ X ) -> ( -. A e. F <-> ( X \ A ) e. F ) )
24 23 3adant3 
 |-  ( ( F e. ( UFil ` X ) /\ A C_ X /\ B C_ X ) -> ( -. A e. F <-> ( X \ A ) e. F ) )
25 24 adantr 
 |-  ( ( ( F e. ( UFil ` X ) /\ A C_ X /\ B C_ X ) /\ ( A u. B ) e. F ) -> ( -. A e. F <-> ( X \ A ) e. F ) )
26 2 3ad2ant1 
 |-  ( ( ( F e. ( UFil ` X ) /\ A C_ X /\ B C_ X ) /\ ( A u. B ) e. F /\ ( X \ A ) e. F ) -> F e. ( Fil ` X ) )
27 difun2 
 |-  ( ( B u. A ) \ A ) = ( B \ A )
28 uncom 
 |-  ( B u. A ) = ( A u. B )
29 28 difeq1i 
 |-  ( ( B u. A ) \ A ) = ( ( A u. B ) \ A )
30 27 29 eqtr3i 
 |-  ( B \ A ) = ( ( A u. B ) \ A )
31 30 ineq2i 
 |-  ( X i^i ( B \ A ) ) = ( X i^i ( ( A u. B ) \ A ) )
32 indifcom 
 |-  ( B i^i ( X \ A ) ) = ( X i^i ( B \ A ) )
33 indifcom 
 |-  ( ( A u. B ) i^i ( X \ A ) ) = ( X i^i ( ( A u. B ) \ A ) )
34 31 32 33 3eqtr4i 
 |-  ( B i^i ( X \ A ) ) = ( ( A u. B ) i^i ( X \ A ) )
35 filin 
 |-  ( ( F e. ( Fil ` X ) /\ ( A u. B ) e. F /\ ( X \ A ) e. F ) -> ( ( A u. B ) i^i ( X \ A ) ) e. F )
36 2 35 syl3an1 
 |-  ( ( ( F e. ( UFil ` X ) /\ A C_ X /\ B C_ X ) /\ ( A u. B ) e. F /\ ( X \ A ) e. F ) -> ( ( A u. B ) i^i ( X \ A ) ) e. F )
37 34 36 eqeltrid 
 |-  ( ( ( F e. ( UFil ` X ) /\ A C_ X /\ B C_ X ) /\ ( A u. B ) e. F /\ ( X \ A ) e. F ) -> ( B i^i ( X \ A ) ) e. F )
38 simp13 
 |-  ( ( ( F e. ( UFil ` X ) /\ A C_ X /\ B C_ X ) /\ ( A u. B ) e. F /\ ( X \ A ) e. F ) -> B C_ X )
39 inss1 
 |-  ( B i^i ( X \ A ) ) C_ B
40 39 a1i 
 |-  ( ( ( F e. ( UFil ` X ) /\ A C_ X /\ B C_ X ) /\ ( A u. B ) e. F /\ ( X \ A ) e. F ) -> ( B i^i ( X \ A ) ) C_ B )
41 filss 
 |-  ( ( F e. ( Fil ` X ) /\ ( ( B i^i ( X \ A ) ) e. F /\ B C_ X /\ ( B i^i ( X \ A ) ) C_ B ) ) -> B e. F )
42 26 37 38 40 41 syl13anc 
 |-  ( ( ( F e. ( UFil ` X ) /\ A C_ X /\ B C_ X ) /\ ( A u. B ) e. F /\ ( X \ A ) e. F ) -> B e. F )
43 42 3expia 
 |-  ( ( ( F e. ( UFil ` X ) /\ A C_ X /\ B C_ X ) /\ ( A u. B ) e. F ) -> ( ( X \ A ) e. F -> B e. F ) )
44 25 43 sylbid 
 |-  ( ( ( F e. ( UFil ` X ) /\ A C_ X /\ B C_ X ) /\ ( A u. B ) e. F ) -> ( -. A e. F -> B e. F ) )
45 44 orrd 
 |-  ( ( ( F e. ( UFil ` X ) /\ A C_ X /\ B C_ X ) /\ ( A u. B ) e. F ) -> ( A e. F \/ B e. F ) )
46 45 ex 
 |-  ( ( F e. ( UFil ` X ) /\ A C_ X /\ B C_ X ) -> ( ( A u. B ) e. F -> ( A e. F \/ B e. F ) ) )
47 22 46 impbid 
 |-  ( ( F e. ( UFil ` X ) /\ A C_ X /\ B C_ X ) -> ( ( A e. F \/ B e. F ) <-> ( A u. B ) e. F ) )