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