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