Metamath Proof Explorer

Theorem fgmin

Description: Minimality property of a generated filter: every filter that contains B contains its generated filter. (Contributed by Jeff Hankins, 5-Sep-2009) (Revised by Mario Carneiro, 7-Aug-2015)

Ref Expression
Assertion fgmin ( ( 𝐵 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) → ( 𝐵 ⊆ 𝐹 ↔ ( 𝑋 filGen 𝐵 ) ⊆ 𝐹 ) )

Proof

Step Hyp Ref Expression
1 elfg ⊢ ( 𝐵 ∈ ( fBas ‘ 𝑋 ) → ( 𝑡 ∈ ( 𝑋 filGen 𝐵 ) ↔ ( 𝑡 ⊆ 𝑋 ∧ ∃ 𝑥 ∈ 𝐵 𝑥 ⊆ 𝑡 ) ) )
2 1 adantr ⊢ ( ( 𝐵 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) → ( 𝑡 ∈ ( 𝑋 filGen 𝐵 ) ↔ ( 𝑡 ⊆ 𝑋 ∧ ∃ 𝑥 ∈ 𝐵 𝑥 ⊆ 𝑡 ) ) )
3 2 adantr ⊢ ( ( ( 𝐵 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝐵 ⊆ 𝐹 ) → ( 𝑡 ∈ ( 𝑋 filGen 𝐵 ) ↔ ( 𝑡 ⊆ 𝑋 ∧ ∃ 𝑥 ∈ 𝐵 𝑥 ⊆ 𝑡 ) ) )
4 ssrexv ⊢ ( 𝐵 ⊆ 𝐹 → ( ∃ 𝑥 ∈ 𝐵 𝑥 ⊆ 𝑡 → ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 ) )
5 4 adantl ⊢ ( ( ( 𝐵 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝐵 ⊆ 𝐹 ) → ( ∃ 𝑥 ∈ 𝐵 𝑥 ⊆ 𝑡 → ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 ) )
6 filss ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑡 ⊆ 𝑋 ∧ 𝑥 ⊆ 𝑡 ) ) → 𝑡 ∈ 𝐹 )
7 6 3exp2 ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝑥 ∈ 𝐹 → ( 𝑡 ⊆ 𝑋 → ( 𝑥 ⊆ 𝑡 → 𝑡 ∈ 𝐹 ) ) ) )
8 7 com34 ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝑥 ∈ 𝐹 → ( 𝑥 ⊆ 𝑡 → ( 𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐹 ) ) ) )
9 8 rexlimdv ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 → ( 𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐹 ) ) )
10 9 ad2antlr ⊢ ( ( ( 𝐵 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝐵 ⊆ 𝐹 ) → ( ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 → ( 𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐹 ) ) )
11 5 10 syld ⊢ ( ( ( 𝐵 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝐵 ⊆ 𝐹 ) → ( ∃ 𝑥 ∈ 𝐵 𝑥 ⊆ 𝑡 → ( 𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐹 ) ) )
12 11 com23 ⊢ ( ( ( 𝐵 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝐵 ⊆ 𝐹 ) → ( 𝑡 ⊆ 𝑋 → ( ∃ 𝑥 ∈ 𝐵 𝑥 ⊆ 𝑡 → 𝑡 ∈ 𝐹 ) ) )
13 12 impd ⊢ ( ( ( 𝐵 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝐵 ⊆ 𝐹 ) → ( ( 𝑡 ⊆ 𝑋 ∧ ∃ 𝑥 ∈ 𝐵 𝑥 ⊆ 𝑡 ) → 𝑡 ∈ 𝐹 ) )
14 3 13 sylbid ⊢ ( ( ( 𝐵 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝐵 ⊆ 𝐹 ) → ( 𝑡 ∈ ( 𝑋 filGen 𝐵 ) → 𝑡 ∈ 𝐹 ) )
15 14 ssrdv ⊢ ( ( ( 𝐵 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝐵 ⊆ 𝐹 ) → ( 𝑋 filGen 𝐵 ) ⊆ 𝐹 )
16 15 ex ⊢ ( ( 𝐵 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) → ( 𝐵 ⊆ 𝐹 → ( 𝑋 filGen 𝐵 ) ⊆ 𝐹 ) )
17 ssfg ⊢ ( 𝐵 ∈ ( fBas ‘ 𝑋 ) → 𝐵 ⊆ ( 𝑋 filGen 𝐵 ) )
18 sstr2 ⊢ ( 𝐵 ⊆ ( 𝑋 filGen 𝐵 ) → ( ( 𝑋 filGen 𝐵 ) ⊆ 𝐹 → 𝐵 ⊆ 𝐹 ) )
19 17 18 syl ⊢ ( 𝐵 ∈ ( fBas ‘ 𝑋 ) → ( ( 𝑋 filGen 𝐵 ) ⊆ 𝐹 → 𝐵 ⊆ 𝐹 ) )
20 19 adantr ⊢ ( ( 𝐵 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) → ( ( 𝑋 filGen 𝐵 ) ⊆ 𝐹 → 𝐵 ⊆ 𝐹 ) )
21 16 20 impbid ⊢ ( ( 𝐵 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) → ( 𝐵 ⊆ 𝐹 ↔ ( 𝑋 filGen 𝐵 ) ⊆ 𝐹 ) )