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 ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐹 ) → ( 𝐴 ∩ 𝐵 ) ∈ 𝐹 )