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 ‘ ∅ ) = { { ∅ } }