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 ∈ u v ∩ w ∈ u ∧ I ↾ ∅ ⊆ v ∧ v -1 ∈ u ∧ ∃ w ∈ u w ∘ w ⊆ v
3 1 2 ax-mp ⊢ u ∈ UnifOn ⁡ ∅ ↔ u ⊆ 𝒫 ∅ × ∅ ∧ ∅ × ∅ ∈ u ∧ ∀ v ∈ u ∀ w ∈ 𝒫 ∅ × ∅ v ⊆ w → w ∈ u ∧ ∀ w ∈ u v ∩ w ∈ u ∧ I ↾ ∅ ⊆ v ∧ v -1 ∈ u ∧ ∃ w ∈ u w ∘ 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 ⁡ ∅ = ∅