Metamath Proof Explorer

Theorem ust0

Description: The unique uniform structure of the empty set is the empty set. Remark 3 of BourbakiTop1 p. II.2. (Contributed by Thierry Arnoux, 15-Nov-2017)

Ref Expression
Assertion ust0 ⊢UnifOn⁡∅=∅

Proof

Step Hyp Ref Expression
1 0ex ⊢∅∈V
2 isust ⊢∅∈V→u∈UnifOn⁡∅↔u⊆𝒫∅×∅∧∅×∅∈u∧∀v∈u∀w∈𝒫∅×∅v⊆w→w∈u∧∀w∈uv∩w∈u∧I↾∅⊆v∧v-1∈u∧∃w∈uw∘w⊆v
3 1 2 ax-mp ⊢u∈UnifOn⁡∅↔u⊆𝒫∅×∅∧∅×∅∈u∧∀v∈u∀w∈𝒫∅×∅v⊆w→w∈u∧∀w∈uv∩w∈u∧I↾∅⊆v∧v-1∈u∧∃w∈uw∘w⊆v
4 3 simp1bi ⊢u∈UnifOn⁡∅→u⊆𝒫∅×∅
5 0xp ⊢∅×∅=∅
6 5 pweqi ⊢𝒫∅×∅=𝒫∅
7 pw0 ⊢𝒫∅=∅
8 6 7 eqtri ⊢𝒫∅×∅=∅
9 4 8 sseqtrdi ⊢u∈UnifOn⁡∅→u⊆∅
10 ustbasel ⊢u∈UnifOn⁡∅→∅×∅∈u
11 5 10 eqeltrrid ⊢u∈UnifOn⁡∅→∅∈u
12 11 snssd ⊢u∈UnifOn⁡∅→∅⊆u
13 9 12 eqssd ⊢u∈UnifOn⁡∅→u=∅
14 velsn ⊢u∈∅↔u=∅
15 13 14 sylibr ⊢u∈UnifOn⁡∅→u∈∅
16 15 ssriv ⊢UnifOn⁡∅⊆∅
17 8 eqimss2i ⊢∅⊆𝒫∅×∅
18 1 snid ⊢∅∈∅
19 5 18 eqeltri ⊢∅×∅∈∅
20 18 a1i ⊢∅⊆∅→∅∈∅
21 8 raleqi ⊢∀w∈𝒫∅×∅∅⊆w→w∈∅↔∀w∈∅∅⊆w→w∈∅
22 sseq2 ⊢w=∅→∅⊆w↔∅⊆∅
23 eleq1 ⊢w=∅→w∈∅↔∅∈∅
24 22 23 imbi12d ⊢w=∅→∅⊆w→w∈∅↔∅⊆∅→∅∈∅
25 1 24 ralsn ⊢∀w∈∅∅⊆w→w∈∅↔∅⊆∅→∅∈∅
26 21 25 bitri ⊢∀w∈𝒫∅×∅∅⊆w→w∈∅↔∅⊆∅→∅∈∅
27 20 26 mpbir ⊢∀w∈𝒫∅×∅∅⊆w→w∈∅
28 inidm ⊢∅∩∅=∅
29 28 18 eqeltri ⊢∅∩∅∈∅
30 ineq2 ⊢w=∅→∅∩w=∅∩∅
31 30 eleq1d ⊢w=∅→∅∩w∈∅↔∅∩∅∈∅
32 1 31 ralsn ⊢∀w∈∅∅∩w∈∅↔∅∩∅∈∅
33 29 32 mpbir ⊢∀w∈∅∅∩w∈∅
34 res0 ⊢I↾∅=∅
35 34 eqimssi ⊢I↾∅⊆∅
36 cnv0 ⊢∅-1=∅
37 36 18 eqeltri ⊢∅-1∈∅
38 0trrel ⊢∅∘∅⊆∅
39 id ⊢w=∅→w=∅
40 39 39 coeq12d ⊢w=∅→w∘w=∅∘∅
41 40 sseq1d ⊢w=∅→w∘w⊆∅↔∅∘∅⊆∅
42 1 41 rexsn ⊢∃w∈∅w∘w⊆∅↔∅∘∅⊆∅
43 38 42 mpbir ⊢∃w∈∅w∘w⊆∅
44 35 37 43 3pm3.2i ⊢I↾∅⊆∅∧∅-1∈∅∧∃w∈∅w∘w⊆∅
45 sseq1 ⊢v=∅→v⊆w↔∅⊆w
46 45 imbi1d ⊢v=∅→v⊆w→w∈∅↔∅⊆w→w∈∅
47 46 ralbidv ⊢v=∅→∀w∈𝒫∅×∅v⊆w→w∈∅↔∀w∈𝒫∅×∅∅⊆w→w∈∅
48 ineq1 ⊢v=∅→v∩w=∅∩w
49 48 eleq1d ⊢v=∅→v∩w∈∅↔∅∩w∈∅
50 49 ralbidv ⊢v=∅→∀w∈∅v∩w∈∅↔∀w∈∅∅∩w∈∅
51 sseq2 ⊢v=∅→I↾∅⊆v↔I↾∅⊆∅
52 cnveq ⊢v=∅→v-1=∅-1
53 52 eleq1d ⊢v=∅→v-1∈∅↔∅-1∈∅
54 sseq2 ⊢v=∅→w∘w⊆v↔w∘w⊆∅
55 54 rexbidv ⊢v=∅→∃w∈∅w∘w⊆v↔∃w∈∅w∘w⊆∅
56 51 53 55 3anbi123d ⊢v=∅→I↾∅⊆v∧v-1∈∅∧∃w∈∅w∘w⊆v↔I↾∅⊆∅∧∅-1∈∅∧∃w∈∅w∘w⊆∅
57 47 50 56 3anbi123d ⊢v=∅→∀w∈𝒫∅×∅v⊆w→w∈∅∧∀w∈∅v∩w∈∅∧I↾∅⊆v∧v-1∈∅∧∃w∈∅w∘w⊆v↔∀w∈𝒫∅×∅∅⊆w→w∈∅∧∀w∈∅∅∩w∈∅∧I↾∅⊆∅∧∅-1∈∅∧∃w∈∅w∘w⊆∅
58 1 57 ralsn ⊢∀v∈∅∀w∈𝒫∅×∅v⊆w→w∈∅∧∀w∈∅v∩w∈∅∧I↾∅⊆v∧v-1∈∅∧∃w∈∅w∘w⊆v↔∀w∈𝒫∅×∅∅⊆w→w∈∅∧∀w∈∅∅∩w∈∅∧I↾∅⊆∅∧∅-1∈∅∧∃w∈∅w∘w⊆∅
59 27 33 44 58 mpbir3an ⊢∀v∈∅∀w∈𝒫∅×∅v⊆w→w∈∅∧∀w∈∅v∩w∈∅∧I↾∅⊆v∧v-1∈∅∧∃w∈∅w∘w⊆v
60 isust ⊢∅∈V→∅∈UnifOn⁡∅↔∅⊆𝒫∅×∅∧∅×∅∈∅∧∀v∈∅∀w∈𝒫∅×∅v⊆w→w∈∅∧∀w∈∅v∩w∈∅∧I↾∅⊆v∧v-1∈∅∧∃w∈∅w∘w⊆v
61 1 60 ax-mp ⊢∅∈UnifOn⁡∅↔∅⊆𝒫∅×∅∧∅×∅∈∅∧∀v∈∅∀w∈𝒫∅×∅v⊆w→w∈∅∧∀w∈∅v∩w∈∅∧I↾∅⊆v∧v-1∈∅∧∃w∈∅w∘w⊆v
62 17 19 59 61 mpbir3an ⊢∅∈UnifOn⁡∅
63 snssi ⊢∅∈UnifOn⁡∅→∅⊆UnifOn⁡∅
64 62 63 ax-mp ⊢∅⊆UnifOn⁡∅
65 16 64 eqssi ⊢UnifOn⁡∅=∅