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 × X v ⊆ w → w ∈ U ∧ ∀ w ∈ U v ∩ w ∈ U ∧ I ↾ X ⊆ v ∧ v -1 ∈ U ∧ ∃ w ∈ U w ∘ w ⊆ v
3 1 2 syl ⊢ U ∈ UnifOn ⁡ X → U ∈ UnifOn ⁡ X ↔ U ⊆ 𝒫 X × X ∧ X × X ∈ U ∧ ∀ v ∈ U ∀ w ∈ 𝒫 X × X v ⊆ w → w ∈ U ∧ ∀ w ∈ U v ∩ w ∈ U ∧ I ↾ X ⊆ v ∧ v -1 ∈ U ∧ ∃ w ∈ U w ∘ w ⊆ v
4 3 ibi ⊢ U ∈ UnifOn ⁡ X → U ⊆ 𝒫 X × X ∧ X × X ∈ U ∧ ∀ v ∈ U ∀ w ∈ 𝒫 X × X v ⊆ w → w ∈ U ∧ ∀ w ∈ U v ∩ w ∈ U ∧ I ↾ X ⊆ v ∧ v -1 ∈ U ∧ ∃ w ∈ U w ∘ w ⊆ v
5 4 simp3d ⊢ U ∈ UnifOn ⁡ X → ∀ v ∈ U ∀ w ∈ 𝒫 X × X v ⊆ w → w ∈ U ∧ ∀ w ∈ U v ∩ w ∈ U ∧ I ↾ X ⊆ v ∧ v -1 ∈ U ∧ ∃ w ∈ U w ∘ 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 × X v ⊆ w → w ∈ U ↔ ∀ w ∈ 𝒫 X × X V ⊆ 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 ∈ U v ∩ w ∈ U ↔ ∀ w ∈ U V ∩ 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 ∈ U w ∘ w ⊆ v ↔ ∃ w ∈ U w ∘ w ⊆ V
17 12 14 16 3anbi123d ⊢ v = V → I ↾ X ⊆ v ∧ v -1 ∈ U ∧ ∃ w ∈ U w ∘ w ⊆ v ↔ I ↾ X ⊆ V ∧ V -1 ∈ U ∧ ∃ w ∈ U w ∘ w ⊆ V
18 8 11 17 3anbi123d ⊢ v = V → ∀ w ∈ 𝒫 X × X v ⊆ w → w ∈ U ∧ ∀ w ∈ U v ∩ w ∈ U ∧ I ↾ X ⊆ v ∧ v -1 ∈ U ∧ ∃ w ∈ U w ∘ w ⊆ v ↔ ∀ w ∈ 𝒫 X × X V ⊆ w → w ∈ U ∧ ∀ w ∈ U V ∩ w ∈ U ∧ I ↾ X ⊆ V ∧ V -1 ∈ U ∧ ∃ w ∈ U w ∘ w ⊆ V
19 18 rspcv ⊢ V ∈ U → ∀ v ∈ U ∀ w ∈ 𝒫 X × X v ⊆ w → w ∈ U ∧ ∀ w ∈ U v ∩ w ∈ U ∧ I ↾ X ⊆ v ∧ v -1 ∈ U ∧ ∃ w ∈ U w ∘ w ⊆ v → ∀ w ∈ 𝒫 X × X V ⊆ w → w ∈ U ∧ ∀ w ∈ U V ∩ w ∈ U ∧ I ↾ X ⊆ V ∧ V -1 ∈ U ∧ ∃ w ∈ U w ∘ w ⊆ V
20 5 19 mpan9 ⊢ U ∈ UnifOn ⁡ X ∧ V ∈ U → ∀ w ∈ 𝒫 X × X V ⊆ w → w ∈ U ∧ ∀ w ∈ U V ∩ w ∈ U ∧ I ↾ X ⊆ V ∧ V -1 ∈ U ∧ ∃ w ∈ U w ∘ w ⊆ V
21 20 simp2d ⊢ U ∈ UnifOn ⁡ X ∧ V ∈ U → ∀ w ∈ U V ∩ 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 ∈ U V ∩ 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