This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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