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 ‘ 𝑋 ) )