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