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 ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋 ) → ( ( 𝐴 ∈ 𝐹 ∨ 𝐵 ∈ 𝐹 ) ↔ ( 𝐴 ∪ 𝐵 ) ∈ 𝐹 ) )

Proof

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