Metamath Proof Explorer

Theorem ustn0

Description: The empty set is not an uniform structure. (Contributed by Thierry Arnoux, 3-Dec-2017)

Ref Expression
Assertion ustn0 ⊢¬∅∈⋃ran⁡UnifOn

Proof

Step Hyp Ref Expression
1 noel ⊢¬x×x∈∅
2 0ex ⊢∅∈V
3 eleq2 ⊢u=∅→x×x∈u↔x×x∈∅
4 2 3 elab ⊢∅∈u|x×x∈u↔x×x∈∅
5 1 4 mtbir ⊢¬∅∈u|x×x∈u
6 vex ⊢x∈V
7 velpw ⊢u∈𝒫𝒫x×x↔u⊆𝒫x×x
8 7 abbii ⊢u|u∈𝒫𝒫x×x=u|u⊆𝒫x×x
9 abid2 ⊢u|u∈𝒫𝒫x×x=𝒫𝒫x×x
10 6 6 xpex ⊢x×x∈V
11 10 pwex ⊢𝒫x×x∈V
12 11 pwex ⊢𝒫𝒫x×x∈V
13 9 12 eqeltri ⊢u|u∈𝒫𝒫x×x∈V
14 8 13 eqeltrri ⊢u|u⊆𝒫x×x∈V
15 simp1 ⊢u⊆𝒫x×x∧x×x∈u∧∀v∈u∀w∈𝒫x×xv⊆w→w∈u∧∀w∈uv∩w∈u∧I↾x⊆v∧v-1∈u∧∃w∈uw∘w⊆v→u⊆𝒫x×x
16 15 ss2abi ⊢u|u⊆𝒫x×x∧x×x∈u∧∀v∈u∀w∈𝒫x×xv⊆w→w∈u∧∀w∈uv∩w∈u∧I↾x⊆v∧v-1∈u∧∃w∈uw∘w⊆v⊆u|u⊆𝒫x×x
17 14 16 ssexi ⊢u|u⊆𝒫x×x∧x×x∈u∧∀v∈u∀w∈𝒫x×xv⊆w→w∈u∧∀w∈uv∩w∈u∧I↾x⊆v∧v-1∈u∧∃w∈uw∘w⊆v∈V
18 df-ust ⊢UnifOn=x∈V⟼u|u⊆𝒫x×x∧x×x∈u∧∀v∈u∀w∈𝒫x×xv⊆w→w∈u∧∀w∈uv∩w∈u∧I↾x⊆v∧v-1∈u∧∃w∈uw∘w⊆v
19 18 fvmpt2 ⊢x∈V∧u|u⊆𝒫x×x∧x×x∈u∧∀v∈u∀w∈𝒫x×xv⊆w→w∈u∧∀w∈uv∩w∈u∧I↾x⊆v∧v-1∈u∧∃w∈uw∘w⊆v∈V→UnifOn⁡x=u|u⊆𝒫x×x∧x×x∈u∧∀v∈u∀w∈𝒫x×xv⊆w→w∈u∧∀w∈uv∩w∈u∧I↾x⊆v∧v-1∈u∧∃w∈uw∘w⊆v
20 6 17 19 mp2an ⊢UnifOn⁡x=u|u⊆𝒫x×x∧x×x∈u∧∀v∈u∀w∈𝒫x×xv⊆w→w∈u∧∀w∈uv∩w∈u∧I↾x⊆v∧v-1∈u∧∃w∈uw∘w⊆v
21 simp2 ⊢u⊆𝒫x×x∧x×x∈u∧∀v∈u∀w∈𝒫x×xv⊆w→w∈u∧∀w∈uv∩w∈u∧I↾x⊆v∧v-1∈u∧∃w∈uw∘w⊆v→x×x∈u
22 21 ss2abi ⊢u|u⊆𝒫x×x∧x×x∈u∧∀v∈u∀w∈𝒫x×xv⊆w→w∈u∧∀w∈uv∩w∈u∧I↾x⊆v∧v-1∈u∧∃w∈uw∘w⊆v⊆u|x×x∈u
23 20 22 eqsstri ⊢UnifOn⁡x⊆u|x×x∈u
24 23 sseli ⊢∅∈UnifOn⁡x→∅∈u|x×x∈u
25 5 24 mto ⊢¬∅∈UnifOn⁡x
26 25 nex ⊢¬∃x∅∈UnifOn⁡x
27 18 funmpt2 ⊢Fun⁡UnifOn
28 elunirn ⊢Fun⁡UnifOn→∅∈⋃ran⁡UnifOn↔∃x∈dom⁡UnifOn∅∈UnifOn⁡x
29 27 28 ax-mp ⊢∅∈⋃ran⁡UnifOn↔∃x∈dom⁡UnifOn∅∈UnifOn⁡x
30 ustfn ⊢UnifOnFnV
31 fndm ⊢UnifOnFnV→dom⁡UnifOn=V
32 30 31 ax-mp ⊢dom⁡UnifOn=V
33 32 rexeqi ⊢∃x∈dom⁡UnifOn∅∈UnifOn⁡x↔∃x∈V∅∈UnifOn⁡x
34 rexv ⊢∃x∈V∅∈UnifOn⁡x↔∃x∅∈UnifOn⁡x
35 29 33 34 3bitri ⊢∅∈⋃ran⁡UnifOn↔∃x∅∈UnifOn⁡x
36 26 35 mtbir ⊢¬∅∈⋃ran⁡UnifOn