This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem filin

Description: A filter is closed under taking intersections. (Contributed by FL, 20-Jul-2007) (Revised by Stefan O'Rear, 28-Jul-2015)

Ref Expression
Assertion filin ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐹 ) → ( 𝐴 ∩ 𝐵 ) ∈ 𝐹 )

Proof

Step Hyp Ref Expression
1 filfbas ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝐹 ∈ ( fBas ‘ 𝑋 ) )
2 fbasssin ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐹 ) → ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ ( 𝐴 ∩ 𝐵 ) )
3 1 2 syl3an1 ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐹 ) → ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ ( 𝐴 ∩ 𝐵 ) )
4 inss1 ⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴
5 filelss ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ) → 𝐴 ⊆ 𝑋 )
6 4 5 sstrid ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ) → ( 𝐴 ∩ 𝐵 ) ⊆ 𝑋 )
7 filss ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑥 ∈ 𝐹 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝑋 ∧ 𝑥 ⊆ ( 𝐴 ∩ 𝐵 ) ) ) → ( 𝐴 ∩ 𝐵 ) ∈ 𝐹 )
8 7 3exp2 ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝑥 ∈ 𝐹 → ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝑋 → ( 𝑥 ⊆ ( 𝐴 ∩ 𝐵 ) → ( 𝐴 ∩ 𝐵 ) ∈ 𝐹 ) ) ) )
9 8 com23 ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝑋 → ( 𝑥 ∈ 𝐹 → ( 𝑥 ⊆ ( 𝐴 ∩ 𝐵 ) → ( 𝐴 ∩ 𝐵 ) ∈ 𝐹 ) ) ) )
10 9 imp ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝑋 ) → ( 𝑥 ∈ 𝐹 → ( 𝑥 ⊆ ( 𝐴 ∩ 𝐵 ) → ( 𝐴 ∩ 𝐵 ) ∈ 𝐹 ) ) )
11 10 rexlimdv ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝑋 ) → ( ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ ( 𝐴 ∩ 𝐵 ) → ( 𝐴 ∩ 𝐵 ) ∈ 𝐹 ) )
12 6 11 syldan ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ) → ( ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ ( 𝐴 ∩ 𝐵 ) → ( 𝐴 ∩ 𝐵 ) ∈ 𝐹 ) )
13 12 3adant3 ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐹 ) → ( ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ ( 𝐴 ∩ 𝐵 ) → ( 𝐴 ∩ 𝐵 ) ∈ 𝐹 ) )
14 3 13 mpd ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐹 ) → ( 𝐴 ∩ 𝐵 ) ∈ 𝐹 )