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 × x v ⊆ w → w ∈ u ∧ ∀ w ∈ u v ∩ w ∈ u ∧ I ↾ x ⊆ v ∧ v -1 ∈ u ∧ ∃ w ∈ u w ∘ w ⊆ v → u ⊆ 𝒫 x × x
16 15 ss2abi ⊢ u | u ⊆ 𝒫 x × x ∧ x × x ∈ u ∧ ∀ v ∈ u ∀ w ∈ 𝒫 x × x v ⊆ w → w ∈ u ∧ ∀ w ∈ u v ∩ w ∈ u ∧ I ↾ x ⊆ v ∧ v -1 ∈ u ∧ ∃ w ∈ u w ∘ w ⊆ v ⊆ u | u ⊆ 𝒫 x × x
17 14 16 ssexi ⊢ u | u ⊆ 𝒫 x × x ∧ x × x ∈ u ∧ ∀ v ∈ u ∀ w ∈ 𝒫 x × x v ⊆ w → w ∈ u ∧ ∀ w ∈ u v ∩ w ∈ u ∧ I ↾ x ⊆ v ∧ v -1 ∈ u ∧ ∃ w ∈ u w ∘ w ⊆ v ∈ V
18 df-ust ⊢ UnifOn = x ∈ V ⟼ u | u ⊆ 𝒫 x × x ∧ x × x ∈ u ∧ ∀ v ∈ u ∀ w ∈ 𝒫 x × x v ⊆ w → w ∈ u ∧ ∀ w ∈ u v ∩ w ∈ u ∧ I ↾ x ⊆ v ∧ v -1 ∈ u ∧ ∃ w ∈ u w ∘ w ⊆ v
19 18 fvmpt2 ⊢ x ∈ V ∧ u | u ⊆ 𝒫 x × x ∧ x × x ∈ u ∧ ∀ v ∈ u ∀ w ∈ 𝒫 x × x v ⊆ w → w ∈ u ∧ ∀ w ∈ u v ∩ w ∈ u ∧ I ↾ x ⊆ v ∧ v -1 ∈ u ∧ ∃ w ∈ u w ∘ w ⊆ v ∈ V → UnifOn ⁡ x = u | u ⊆ 𝒫 x × x ∧ x × x ∈ u ∧ ∀ v ∈ u ∀ w ∈ 𝒫 x × x v ⊆ w → w ∈ u ∧ ∀ w ∈ u v ∩ w ∈ u ∧ I ↾ x ⊆ v ∧ v -1 ∈ u ∧ ∃ w ∈ u w ∘ w ⊆ v
20 6 17 19 mp2an ⊢ UnifOn ⁡ x = u | u ⊆ 𝒫 x × x ∧ x × x ∈ u ∧ ∀ v ∈ u ∀ w ∈ 𝒫 x × x v ⊆ w → w ∈ u ∧ ∀ w ∈ u v ∩ w ∈ u ∧ I ↾ x ⊆ v ∧ v -1 ∈ u ∧ ∃ w ∈ u w ∘ w ⊆ v
21 simp2 ⊢ u ⊆ 𝒫 x × x ∧ x × x ∈ u ∧ ∀ v ∈ u ∀ w ∈ 𝒫 x × x v ⊆ w → w ∈ u ∧ ∀ w ∈ u v ∩ w ∈ u ∧ I ↾ x ⊆ v ∧ v -1 ∈ u ∧ ∃ w ∈ u w ∘ w ⊆ v → x × x ∈ u
22 21 ss2abi ⊢ u | u ⊆ 𝒫 x × x ∧ x × x ∈ u ∧ ∀ v ∈ u ∀ w ∈ 𝒫 x × x v ⊆ w → w ∈ u ∧ ∀ w ∈ u v ∩ w ∈ u ∧ I ↾ x ⊆ v ∧ v -1 ∈ u ∧ ∃ w ∈ u w ∘ 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 ⊢ UnifOn Fn V
31 fndm ⊢ UnifOn Fn V → 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