Metamath Proof Explorer

Theorem ustincl

Description: A uniform structure is closed under finite intersection. Condition F_II of BourbakiTop1 p. I.36. (Contributed by Thierry Arnoux, 30-Nov-2017)

Ref Expression
Assertion ustincl ⊢U∈UnifOn⁡X∧V∈U∧W∈U→V∩W∈U

Proof

Step Hyp Ref Expression
1 elfvex ⊢U∈UnifOn⁡X→X∈V
2 isust ⊢X∈V→U∈UnifOn⁡X↔U⊆𝒫X×X∧X×X∈U∧∀v∈U∀w∈𝒫X×Xv⊆w→w∈U∧∀w∈Uv∩w∈U∧I↾X⊆v∧v-1∈U∧∃w∈Uw∘w⊆v
3 1 2 syl ⊢U∈UnifOn⁡X→U∈UnifOn⁡X↔U⊆𝒫X×X∧X×X∈U∧∀v∈U∀w∈𝒫X×Xv⊆w→w∈U∧∀w∈Uv∩w∈U∧I↾X⊆v∧v-1∈U∧∃w∈Uw∘w⊆v
4 3 ibi ⊢U∈UnifOn⁡X→U⊆𝒫X×X∧X×X∈U∧∀v∈U∀w∈𝒫X×Xv⊆w→w∈U∧∀w∈Uv∩w∈U∧I↾X⊆v∧v-1∈U∧∃w∈Uw∘w⊆v
5 4 simp3d ⊢U∈UnifOn⁡X→∀v∈U∀w∈𝒫X×Xv⊆w→w∈U∧∀w∈Uv∩w∈U∧I↾X⊆v∧v-1∈U∧∃w∈Uw∘w⊆v
6 sseq1 ⊢v=V→v⊆w↔V⊆w
7 6 imbi1d ⊢v=V→v⊆w→w∈U↔V⊆w→w∈U
8 7 ralbidv ⊢v=V→∀w∈𝒫X×Xv⊆w→w∈U↔∀w∈𝒫X×XV⊆w→w∈U
9 ineq1 ⊢v=V→v∩w=V∩w
10 9 eleq1d ⊢v=V→v∩w∈U↔V∩w∈U
11 10 ralbidv ⊢v=V→∀w∈Uv∩w∈U↔∀w∈UV∩w∈U
12 sseq2 ⊢v=V→I↾X⊆v↔I↾X⊆V
13 cnveq ⊢v=V→v-1=V-1
14 13 eleq1d ⊢v=V→v-1∈U↔V-1∈U
15 sseq2 ⊢v=V→w∘w⊆v↔w∘w⊆V
16 15 rexbidv ⊢v=V→∃w∈Uw∘w⊆v↔∃w∈Uw∘w⊆V
17 12 14 16 3anbi123d ⊢v=V→I↾X⊆v∧v-1∈U∧∃w∈Uw∘w⊆v↔I↾X⊆V∧V-1∈U∧∃w∈Uw∘w⊆V
18 8 11 17 3anbi123d ⊢v=V→∀w∈𝒫X×Xv⊆w→w∈U∧∀w∈Uv∩w∈U∧I↾X⊆v∧v-1∈U∧∃w∈Uw∘w⊆v↔∀w∈𝒫X×XV⊆w→w∈U∧∀w∈UV∩w∈U∧I↾X⊆V∧V-1∈U∧∃w∈Uw∘w⊆V
19 18 rspcv ⊢V∈U→∀v∈U∀w∈𝒫X×Xv⊆w→w∈U∧∀w∈Uv∩w∈U∧I↾X⊆v∧v-1∈U∧∃w∈Uw∘w⊆v→∀w∈𝒫X×XV⊆w→w∈U∧∀w∈UV∩w∈U∧I↾X⊆V∧V-1∈U∧∃w∈Uw∘w⊆V
20 5 19 mpan9 ⊢U∈UnifOn⁡X∧V∈U→∀w∈𝒫X×XV⊆w→w∈U∧∀w∈UV∩w∈U∧I↾X⊆V∧V-1∈U∧∃w∈Uw∘w⊆V
21 20 simp2d ⊢U∈UnifOn⁡X∧V∈U→∀w∈UV∩w∈U
22 ineq2 ⊢w=W→V∩w=V∩W
23 22 eleq1d ⊢w=W→V∩w∈U↔V∩W∈U
24 23 rspcv ⊢W∈U→∀w∈UV∩w∈U→V∩W∈U
25 21 24 mpan9 ⊢U∈UnifOn⁡X∧V∈U∧W∈U→V∩W∈U
26 25 3impa ⊢U∈UnifOn⁡X∧V∈U∧W∈U→V∩W∈U