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

Metamath Proof Explorer

Theorem infil

Description: The intersection of two filters is a filter. Use fiint to extend this property to the intersection of a finite set of filters. Paragraph 3 of BourbakiTop1 p. I.36. (Contributed by FL, 17-Sep-2007) (Revised by Stefan O'Rear, 2-Aug-2015)

Ref Expression
Assertion infil ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐺 ∈ ( Fil ‘ 𝑋 ) ) → ( 𝐹 ∩ 𝐺 ) ∈ ( Fil ‘ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 inss1 ⊢ ( 𝐹 ∩ 𝐺 ) ⊆ 𝐹
2 filsspw ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝐹 ⊆ 𝒫 𝑋 )
3 2 adantr ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐺 ∈ ( Fil ‘ 𝑋 ) ) → 𝐹 ⊆ 𝒫 𝑋 )
4 1 3 sstrid ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐺 ∈ ( Fil ‘ 𝑋 ) ) → ( 𝐹 ∩ 𝐺 ) ⊆ 𝒫 𝑋 )
5 0nelfil ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ¬ ∅ ∈ 𝐹 )
6 5 adantr ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐺 ∈ ( Fil ‘ 𝑋 ) ) → ¬ ∅ ∈ 𝐹 )
7 elinel1 ⊢ ( ∅ ∈ ( 𝐹 ∩ 𝐺 ) → ∅ ∈ 𝐹 )
8 6 7 nsyl ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐺 ∈ ( Fil ‘ 𝑋 ) ) → ¬ ∅ ∈ ( 𝐹 ∩ 𝐺 ) )
9 filtop ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝑋 ∈ 𝐹 )
10 9 adantr ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐺 ∈ ( Fil ‘ 𝑋 ) ) → 𝑋 ∈ 𝐹 )
11 filtop ⊢ ( 𝐺 ∈ ( Fil ‘ 𝑋 ) → 𝑋 ∈ 𝐺 )
12 11 adantl ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐺 ∈ ( Fil ‘ 𝑋 ) ) → 𝑋 ∈ 𝐺 )
13 10 12 elind ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐺 ∈ ( Fil ‘ 𝑋 ) ) → 𝑋 ∈ ( 𝐹 ∩ 𝐺 ) )
14 4 8 13 3jca ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐺 ∈ ( Fil ‘ 𝑋 ) ) → ( ( 𝐹 ∩ 𝐺 ) ⊆ 𝒫 𝑋 ∧ ¬ ∅ ∈ ( 𝐹 ∩ 𝐺 ) ∧ 𝑋 ∈ ( 𝐹 ∩ 𝐺 ) ) )
15 simpll ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐺 ∈ ( Fil ‘ 𝑋 ) ) ∧ ( 𝑥 ∈ 𝒫 𝑋 ∧ 𝑦 ∈ ( 𝐹 ∩ 𝐺 ) ∧ 𝑦 ⊆ 𝑥 ) ) → 𝐹 ∈ ( Fil ‘ 𝑋 ) )
16 simpr2 ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐺 ∈ ( Fil ‘ 𝑋 ) ) ∧ ( 𝑥 ∈ 𝒫 𝑋 ∧ 𝑦 ∈ ( 𝐹 ∩ 𝐺 ) ∧ 𝑦 ⊆ 𝑥 ) ) → 𝑦 ∈ ( 𝐹 ∩ 𝐺 ) )
17 elinel1 ⊢ ( 𝑦 ∈ ( 𝐹 ∩ 𝐺 ) → 𝑦 ∈ 𝐹 )
18 16 17 syl ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐺 ∈ ( Fil ‘ 𝑋 ) ) ∧ ( 𝑥 ∈ 𝒫 𝑋 ∧ 𝑦 ∈ ( 𝐹 ∩ 𝐺 ) ∧ 𝑦 ⊆ 𝑥 ) ) → 𝑦 ∈ 𝐹 )
19 simpr1 ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐺 ∈ ( Fil ‘ 𝑋 ) ) ∧ ( 𝑥 ∈ 𝒫 𝑋 ∧ 𝑦 ∈ ( 𝐹 ∩ 𝐺 ) ∧ 𝑦 ⊆ 𝑥 ) ) → 𝑥 ∈ 𝒫 𝑋 )
20 19 elpwid ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐺 ∈ ( Fil ‘ 𝑋 ) ) ∧ ( 𝑥 ∈ 𝒫 𝑋 ∧ 𝑦 ∈ ( 𝐹 ∩ 𝐺 ) ∧ 𝑦 ⊆ 𝑥 ) ) → 𝑥 ⊆ 𝑋 )
21 simpr3 ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐺 ∈ ( Fil ‘ 𝑋 ) ) ∧ ( 𝑥 ∈ 𝒫 𝑋 ∧ 𝑦 ∈ ( 𝐹 ∩ 𝐺 ) ∧ 𝑦 ⊆ 𝑥 ) ) → 𝑦 ⊆ 𝑥 )
22 filss ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑦 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑥 ) ) → 𝑥 ∈ 𝐹 )
23 15 18 20 21 22 syl13anc ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐺 ∈ ( Fil ‘ 𝑋 ) ) ∧ ( 𝑥 ∈ 𝒫 𝑋 ∧ 𝑦 ∈ ( 𝐹 ∩ 𝐺 ) ∧ 𝑦 ⊆ 𝑥 ) ) → 𝑥 ∈ 𝐹 )
24 simplr ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐺 ∈ ( Fil ‘ 𝑋 ) ) ∧ ( 𝑥 ∈ 𝒫 𝑋 ∧ 𝑦 ∈ ( 𝐹 ∩ 𝐺 ) ∧ 𝑦 ⊆ 𝑥 ) ) → 𝐺 ∈ ( Fil ‘ 𝑋 ) )
25 elinel2 ⊢ ( 𝑦 ∈ ( 𝐹 ∩ 𝐺 ) → 𝑦 ∈ 𝐺 )
26 16 25 syl ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐺 ∈ ( Fil ‘ 𝑋 ) ) ∧ ( 𝑥 ∈ 𝒫 𝑋 ∧ 𝑦 ∈ ( 𝐹 ∩ 𝐺 ) ∧ 𝑦 ⊆ 𝑥 ) ) → 𝑦 ∈ 𝐺 )
27 filss ⊢ ( ( 𝐺 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑦 ∈ 𝐺 ∧ 𝑥 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑥 ) ) → 𝑥 ∈ 𝐺 )
28 24 26 20 21 27 syl13anc ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐺 ∈ ( Fil ‘ 𝑋 ) ) ∧ ( 𝑥 ∈ 𝒫 𝑋 ∧ 𝑦 ∈ ( 𝐹 ∩ 𝐺 ) ∧ 𝑦 ⊆ 𝑥 ) ) → 𝑥 ∈ 𝐺 )
29 23 28 elind ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐺 ∈ ( Fil ‘ 𝑋 ) ) ∧ ( 𝑥 ∈ 𝒫 𝑋 ∧ 𝑦 ∈ ( 𝐹 ∩ 𝐺 ) ∧ 𝑦 ⊆ 𝑥 ) ) → 𝑥 ∈ ( 𝐹 ∩ 𝐺 ) )
30 29 3exp2 ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐺 ∈ ( Fil ‘ 𝑋 ) ) → ( 𝑥 ∈ 𝒫 𝑋 → ( 𝑦 ∈ ( 𝐹 ∩ 𝐺 ) → ( 𝑦 ⊆ 𝑥 → 𝑥 ∈ ( 𝐹 ∩ 𝐺 ) ) ) ) )
31 30 imp ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐺 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑥 ∈ 𝒫 𝑋 ) → ( 𝑦 ∈ ( 𝐹 ∩ 𝐺 ) → ( 𝑦 ⊆ 𝑥 → 𝑥 ∈ ( 𝐹 ∩ 𝐺 ) ) ) )
32 31 rexlimdv ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐺 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑥 ∈ 𝒫 𝑋 ) → ( ∃ 𝑦 ∈ ( 𝐹 ∩ 𝐺 ) 𝑦 ⊆ 𝑥 → 𝑥 ∈ ( 𝐹 ∩ 𝐺 ) ) )
33 32 ralrimiva ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐺 ∈ ( Fil ‘ 𝑋 ) ) → ∀ 𝑥 ∈ 𝒫 𝑋 ( ∃ 𝑦 ∈ ( 𝐹 ∩ 𝐺 ) 𝑦 ⊆ 𝑥 → 𝑥 ∈ ( 𝐹 ∩ 𝐺 ) ) )
34 simpl ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐺 ∈ ( Fil ‘ 𝑋 ) ) → 𝐹 ∈ ( Fil ‘ 𝑋 ) )
35 elinel1 ⊢ ( 𝑥 ∈ ( 𝐹 ∩ 𝐺 ) → 𝑥 ∈ 𝐹 )
36 35 17 anim12i ⊢ ( ( 𝑥 ∈ ( 𝐹 ∩ 𝐺 ) ∧ 𝑦 ∈ ( 𝐹 ∩ 𝐺 ) ) → ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) )
37 filin ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) → ( 𝑥 ∩ 𝑦 ) ∈ 𝐹 )
38 37 3expb ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) ) → ( 𝑥 ∩ 𝑦 ) ∈ 𝐹 )
39 34 36 38 syl2an ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐺 ∈ ( Fil ‘ 𝑋 ) ) ∧ ( 𝑥 ∈ ( 𝐹 ∩ 𝐺 ) ∧ 𝑦 ∈ ( 𝐹 ∩ 𝐺 ) ) ) → ( 𝑥 ∩ 𝑦 ) ∈ 𝐹 )
40 simpr ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐺 ∈ ( Fil ‘ 𝑋 ) ) → 𝐺 ∈ ( Fil ‘ 𝑋 ) )
41 elinel2 ⊢ ( 𝑥 ∈ ( 𝐹 ∩ 𝐺 ) → 𝑥 ∈ 𝐺 )
42 41 25 anim12i ⊢ ( ( 𝑥 ∈ ( 𝐹 ∩ 𝐺 ) ∧ 𝑦 ∈ ( 𝐹 ∩ 𝐺 ) ) → ( 𝑥 ∈ 𝐺 ∧ 𝑦 ∈ 𝐺 ) )
43 filin ⊢ ( ( 𝐺 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ∈ 𝐺 ∧ 𝑦 ∈ 𝐺 ) → ( 𝑥 ∩ 𝑦 ) ∈ 𝐺 )
44 43 3expb ⊢ ( ( 𝐺 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑥 ∈ 𝐺 ∧ 𝑦 ∈ 𝐺 ) ) → ( 𝑥 ∩ 𝑦 ) ∈ 𝐺 )
45 40 42 44 syl2an ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐺 ∈ ( Fil ‘ 𝑋 ) ) ∧ ( 𝑥 ∈ ( 𝐹 ∩ 𝐺 ) ∧ 𝑦 ∈ ( 𝐹 ∩ 𝐺 ) ) ) → ( 𝑥 ∩ 𝑦 ) ∈ 𝐺 )
46 39 45 elind ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐺 ∈ ( Fil ‘ 𝑋 ) ) ∧ ( 𝑥 ∈ ( 𝐹 ∩ 𝐺 ) ∧ 𝑦 ∈ ( 𝐹 ∩ 𝐺 ) ) ) → ( 𝑥 ∩ 𝑦 ) ∈ ( 𝐹 ∩ 𝐺 ) )
47 46 ralrimivva ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐺 ∈ ( Fil ‘ 𝑋 ) ) → ∀ 𝑥 ∈ ( 𝐹 ∩ 𝐺 ) ∀ 𝑦 ∈ ( 𝐹 ∩ 𝐺 ) ( 𝑥 ∩ 𝑦 ) ∈ ( 𝐹 ∩ 𝐺 ) )
48 isfil2 ⊢ ( ( 𝐹 ∩ 𝐺 ) ∈ ( Fil ‘ 𝑋 ) ↔ ( ( ( 𝐹 ∩ 𝐺 ) ⊆ 𝒫 𝑋 ∧ ¬ ∅ ∈ ( 𝐹 ∩ 𝐺 ) ∧ 𝑋 ∈ ( 𝐹 ∩ 𝐺 ) ) ∧ ∀ 𝑥 ∈ 𝒫 𝑋 ( ∃ 𝑦 ∈ ( 𝐹 ∩ 𝐺 ) 𝑦 ⊆ 𝑥 → 𝑥 ∈ ( 𝐹 ∩ 𝐺 ) ) ∧ ∀ 𝑥 ∈ ( 𝐹 ∩ 𝐺 ) ∀ 𝑦 ∈ ( 𝐹 ∩ 𝐺 ) ( 𝑥 ∩ 𝑦 ) ∈ ( 𝐹 ∩ 𝐺 ) ) )
49 14 33 47 48 syl3anbrc ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐺 ∈ ( Fil ‘ 𝑋 ) ) → ( 𝐹 ∩ 𝐺 ) ∈ ( Fil ‘ 𝑋 ) )