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∈UFil⁡X∧A⊆X∧B⊆X→A∈F∨B∈F↔A∪B∈F

Proof

Step Hyp Ref Expression
1 ufilfil ⊢F∈UFil⁡X→F∈Fil⁡X
2 1 3ad2ant1 ⊢F∈UFil⁡X∧A⊆X∧B⊆X→F∈Fil⁡X
3 2 adantr ⊢F∈UFil⁡X∧A⊆X∧B⊆X∧A∈F→F∈Fil⁡X
4 simpr ⊢F∈UFil⁡X∧A⊆X∧B⊆X∧A∈F→A∈F
5 unss ⊢A⊆X∧B⊆X↔A∪B⊆X
6 5 biimpi ⊢A⊆X∧B⊆X→A∪B⊆X
7 6 3adant1 ⊢F∈UFil⁡X∧A⊆X∧B⊆X→A∪B⊆X
8 7 adantr ⊢F∈UFil⁡X∧A⊆X∧B⊆X∧A∈F→A∪B⊆X
9 ssun1 ⊢A⊆A∪B
10 9 a1i ⊢F∈UFil⁡X∧A⊆X∧B⊆X∧A∈F→A⊆A∪B
11 filss ⊢F∈Fil⁡X∧A∈F∧A∪B⊆X∧A⊆A∪B→A∪B∈F
12 3 4 8 10 11 syl13anc ⊢F∈UFil⁡X∧A⊆X∧B⊆X∧A∈F→A∪B∈F
13 12 ex ⊢F∈UFil⁡X∧A⊆X∧B⊆X→A∈F→A∪B∈F
14 2 adantr ⊢F∈UFil⁡X∧A⊆X∧B⊆X∧B∈F→F∈Fil⁡X
15 simpr ⊢F∈UFil⁡X∧A⊆X∧B⊆X∧B∈F→B∈F
16 7 adantr ⊢F∈UFil⁡X∧A⊆X∧B⊆X∧B∈F→A∪B⊆X
17 ssun2 ⊢B⊆A∪B
18 17 a1i ⊢F∈UFil⁡X∧A⊆X∧B⊆X∧B∈F→B⊆A∪B
19 filss ⊢F∈Fil⁡X∧B∈F∧A∪B⊆X∧B⊆A∪B→A∪B∈F
20 14 15 16 18 19 syl13anc ⊢F∈UFil⁡X∧A⊆X∧B⊆X∧B∈F→A∪B∈F
21 20 ex ⊢F∈UFil⁡X∧A⊆X∧B⊆X→B∈F→A∪B∈F
22 13 21 jaod ⊢F∈UFil⁡X∧A⊆X∧B⊆X→A∈F∨B∈F→A∪B∈F
23 ufilb ⊢F∈UFil⁡X∧A⊆X→¬A∈F↔X∖A∈F
24 23 3adant3 ⊢F∈UFil⁡X∧A⊆X∧B⊆X→¬A∈F↔X∖A∈F
25 24 adantr ⊢F∈UFil⁡X∧A⊆X∧B⊆X∧A∪B∈F→¬A∈F↔X∖A∈F
26 2 3ad2ant1 ⊢F∈UFil⁡X∧A⊆X∧B⊆X∧A∪B∈F∧X∖A∈F→F∈Fil⁡X
27 difun2 ⊢B∪A∖A=B∖A
28 uncom ⊢B∪A=A∪B
29 28 difeq1i ⊢B∪A∖A=A∪B∖A
30 27 29 eqtr3i ⊢B∖A=A∪B∖A
31 30 ineq2i ⊢X∩B∖A=X∩A∪B∖A
32 indifcom ⊢B∩X∖A=X∩B∖A
33 indifcom ⊢A∪B∩X∖A=X∩A∪B∖A
34 31 32 33 3eqtr4i ⊢B∩X∖A=A∪B∩X∖A
35 filin ⊢F∈Fil⁡X∧A∪B∈F∧X∖A∈F→A∪B∩X∖A∈F
36 2 35 syl3an1 ⊢F∈UFil⁡X∧A⊆X∧B⊆X∧A∪B∈F∧X∖A∈F→A∪B∩X∖A∈F
37 34 36 eqeltrid ⊢F∈UFil⁡X∧A⊆X∧B⊆X∧A∪B∈F∧X∖A∈F→B∩X∖A∈F
38 simp13 ⊢F∈UFil⁡X∧A⊆X∧B⊆X∧A∪B∈F∧X∖A∈F→B⊆X
39 inss1 ⊢B∩X∖A⊆B
40 39 a1i ⊢F∈UFil⁡X∧A⊆X∧B⊆X∧A∪B∈F∧X∖A∈F→B∩X∖A⊆B
41 filss ⊢F∈Fil⁡X∧B∩X∖A∈F∧B⊆X∧B∩X∖A⊆B→B∈F
42 26 37 38 40 41 syl13anc ⊢F∈UFil⁡X∧A⊆X∧B⊆X∧A∪B∈F∧X∖A∈F→B∈F
43 42 3expia ⊢F∈UFil⁡X∧A⊆X∧B⊆X∧A∪B∈F→X∖A∈F→B∈F
44 25 43 sylbid ⊢F∈UFil⁡X∧A⊆X∧B⊆X∧A∪B∈F→¬A∈F→B∈F
45 44 orrd ⊢F∈UFil⁡X∧A⊆X∧B⊆X∧A∪B∈F→A∈F∨B∈F
46 45 ex ⊢F∈UFil⁡X∧A⊆X∧B⊆X→A∪B∈F→A∈F∨B∈F
47 22 46 impbid ⊢F∈UFil⁡X∧A⊆X∧B⊆X→A∈F∨B∈F↔A∪B∈F