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 ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝐺 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 ⊆ 𝐺 ) → 𝐹 = 𝐺 )

Proof

Step Hyp Ref Expression
1 simp3 ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝐺 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 ⊆ 𝐺 ) → 𝐹 ⊆ 𝐺 )
2 filelss ⊢ ( ( 𝐺 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ∈ 𝐺 ) → 𝑥 ⊆ 𝑋 )
3 2 ex ⊢ ( 𝐺 ∈ ( Fil ‘ 𝑋 ) → ( 𝑥 ∈ 𝐺 → 𝑥 ⊆ 𝑋 ) )
4 3 3ad2ant2 ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝐺 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 ⊆ 𝐺 ) → ( 𝑥 ∈ 𝐺 → 𝑥 ⊆ 𝑋 ) )
5 ufilb ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) → ( ¬ 𝑥 ∈ 𝐹 ↔ ( 𝑋 ∖ 𝑥 ) ∈ 𝐹 ) )
6 5 3ad2antl1 ⊢ ( ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝐺 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 ⊆ 𝐺 ) ∧ 𝑥 ⊆ 𝑋 ) → ( ¬ 𝑥 ∈ 𝐹 ↔ ( 𝑋 ∖ 𝑥 ) ∈ 𝐹 ) )
7 simpl3 ⊢ ( ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝐺 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 ⊆ 𝐺 ) ∧ 𝑥 ⊆ 𝑋 ) → 𝐹 ⊆ 𝐺 )
8 7 sseld ⊢ ( ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝐺 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 ⊆ 𝐺 ) ∧ 𝑥 ⊆ 𝑋 ) → ( ( 𝑋 ∖ 𝑥 ) ∈ 𝐹 → ( 𝑋 ∖ 𝑥 ) ∈ 𝐺 ) )
9 filfbas ⊢ ( 𝐺 ∈ ( Fil ‘ 𝑋 ) → 𝐺 ∈ ( fBas ‘ 𝑋 ) )
10 fbncp ⊢ ( ( 𝐺 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑥 ∈ 𝐺 ) → ¬ ( 𝑋 ∖ 𝑥 ) ∈ 𝐺 )
11 10 ex ⊢ ( 𝐺 ∈ ( fBas ‘ 𝑋 ) → ( 𝑥 ∈ 𝐺 → ¬ ( 𝑋 ∖ 𝑥 ) ∈ 𝐺 ) )
12 9 11 syl ⊢ ( 𝐺 ∈ ( Fil ‘ 𝑋 ) → ( 𝑥 ∈ 𝐺 → ¬ ( 𝑋 ∖ 𝑥 ) ∈ 𝐺 ) )
13 12 con2d ⊢ ( 𝐺 ∈ ( Fil ‘ 𝑋 ) → ( ( 𝑋 ∖ 𝑥 ) ∈ 𝐺 → ¬ 𝑥 ∈ 𝐺 ) )
14 13 3ad2ant2 ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝐺 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 ⊆ 𝐺 ) → ( ( 𝑋 ∖ 𝑥 ) ∈ 𝐺 → ¬ 𝑥 ∈ 𝐺 ) )
15 14 adantr ⊢ ( ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝐺 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 ⊆ 𝐺 ) ∧ 𝑥 ⊆ 𝑋 ) → ( ( 𝑋 ∖ 𝑥 ) ∈ 𝐺 → ¬ 𝑥 ∈ 𝐺 ) )
16 8 15 syld ⊢ ( ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝐺 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 ⊆ 𝐺 ) ∧ 𝑥 ⊆ 𝑋 ) → ( ( 𝑋 ∖ 𝑥 ) ∈ 𝐹 → ¬ 𝑥 ∈ 𝐺 ) )
17 6 16 sylbid ⊢ ( ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝐺 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 ⊆ 𝐺 ) ∧ 𝑥 ⊆ 𝑋 ) → ( ¬ 𝑥 ∈ 𝐹 → ¬ 𝑥 ∈ 𝐺 ) )
18 17 con4d ⊢ ( ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝐺 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 ⊆ 𝐺 ) ∧ 𝑥 ⊆ 𝑋 ) → ( 𝑥 ∈ 𝐺 → 𝑥 ∈ 𝐹 ) )
19 18 ex ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝐺 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 ⊆ 𝐺 ) → ( 𝑥 ⊆ 𝑋 → ( 𝑥 ∈ 𝐺 → 𝑥 ∈ 𝐹 ) ) )
20 19 com23 ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝐺 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 ⊆ 𝐺 ) → ( 𝑥 ∈ 𝐺 → ( 𝑥 ⊆ 𝑋 → 𝑥 ∈ 𝐹 ) ) )
21 4 20 mpdd ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝐺 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 ⊆ 𝐺 ) → ( 𝑥 ∈ 𝐺 → 𝑥 ∈ 𝐹 ) )
22 21 ssrdv ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝐺 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 ⊆ 𝐺 ) → 𝐺 ⊆ 𝐹 )
23 1 22 eqssd ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝐺 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 ⊆ 𝐺 ) → 𝐹 = 𝐺 )