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

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 ⊢ ¬ ( 𝑥 × 𝑥 ) ∈ ∅
2 0ex ⊢ ∅ ∈ V
3 eleq2 ⊢ ( 𝑢 = ∅ → ( ( 𝑥 × 𝑥 ) ∈ 𝑢 ↔ ( 𝑥 × 𝑥 ) ∈ ∅ ) )
4 2 3 elab ⊢ ( ∅ ∈ { 𝑢 ∣ ( 𝑥 × 𝑥 ) ∈ 𝑢 } ↔ ( 𝑥 × 𝑥 ) ∈ ∅ )
5 1 4 mtbir ⊢ ¬ ∅ ∈ { 𝑢 ∣ ( 𝑥 × 𝑥 ) ∈ 𝑢 }
6 vex ⊢ 𝑥 ∈ V
7 velpw ⊢ ( 𝑢 ∈ 𝒫 𝒫 ( 𝑥 × 𝑥 ) ↔ 𝑢 ⊆ 𝒫 ( 𝑥 × 𝑥 ) )
8 7 abbii ⊢ { 𝑢 ∣ 𝑢 ∈ 𝒫 𝒫 ( 𝑥 × 𝑥 ) } = { 𝑢 ∣ 𝑢 ⊆ 𝒫 ( 𝑥 × 𝑥 ) }
9 abid2 ⊢ { 𝑢 ∣ 𝑢 ∈ 𝒫 𝒫 ( 𝑥 × 𝑥 ) } = 𝒫 𝒫 ( 𝑥 × 𝑥 )
10 6 6 xpex ⊢ ( 𝑥 × 𝑥 ) ∈ V
11 10 pwex ⊢ 𝒫 ( 𝑥 × 𝑥 ) ∈ V
12 11 pwex ⊢ 𝒫 𝒫 ( 𝑥 × 𝑥 ) ∈ V
13 9 12 eqeltri ⊢ { 𝑢 ∣ 𝑢 ∈ 𝒫 𝒫 ( 𝑥 × 𝑥 ) } ∈ V
14 8 13 eqeltrri ⊢ { 𝑢 ∣ 𝑢 ⊆ 𝒫 ( 𝑥 × 𝑥 ) } ∈ V
15 simp1 ⊢ ( ( 𝑢 ⊆ 𝒫 ( 𝑥 × 𝑥 ) ∧ ( 𝑥 × 𝑥 ) ∈ 𝑢 ∧ ∀ 𝑣 ∈ 𝑢 ( ∀ 𝑤 ∈ 𝒫 ( 𝑥 × 𝑥 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢 ) ∧ ∀ 𝑤 ∈ 𝑢 ( 𝑣 ∩ 𝑤 ) ∈ 𝑢 ∧ ( ( I ↾ 𝑥 ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ 𝑢 ∧ ∃ 𝑤 ∈ 𝑢 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) ) ) → 𝑢 ⊆ 𝒫 ( 𝑥 × 𝑥 ) )
16 15 ss2abi ⊢ { 𝑢 ∣ ( 𝑢 ⊆ 𝒫 ( 𝑥 × 𝑥 ) ∧ ( 𝑥 × 𝑥 ) ∈ 𝑢 ∧ ∀ 𝑣 ∈ 𝑢 ( ∀ 𝑤 ∈ 𝒫 ( 𝑥 × 𝑥 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢 ) ∧ ∀ 𝑤 ∈ 𝑢 ( 𝑣 ∩ 𝑤 ) ∈ 𝑢 ∧ ( ( I ↾ 𝑥 ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ 𝑢 ∧ ∃ 𝑤 ∈ 𝑢 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) ) ) } ⊆ { 𝑢 ∣ 𝑢 ⊆ 𝒫 ( 𝑥 × 𝑥 ) }
17 14 16 ssexi ⊢ { 𝑢 ∣ ( 𝑢 ⊆ 𝒫 ( 𝑥 × 𝑥 ) ∧ ( 𝑥 × 𝑥 ) ∈ 𝑢 ∧ ∀ 𝑣 ∈ 𝑢 ( ∀ 𝑤 ∈ 𝒫 ( 𝑥 × 𝑥 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢 ) ∧ ∀ 𝑤 ∈ 𝑢 ( 𝑣 ∩ 𝑤 ) ∈ 𝑢 ∧ ( ( I ↾ 𝑥 ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ 𝑢 ∧ ∃ 𝑤 ∈ 𝑢 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) ) ) } ∈ V
18 df-ust ⊢ UnifOn = ( 𝑥 ∈ V ↦ { 𝑢 ∣ ( 𝑢 ⊆ 𝒫 ( 𝑥 × 𝑥 ) ∧ ( 𝑥 × 𝑥 ) ∈ 𝑢 ∧ ∀ 𝑣 ∈ 𝑢 ( ∀ 𝑤 ∈ 𝒫 ( 𝑥 × 𝑥 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢 ) ∧ ∀ 𝑤 ∈ 𝑢 ( 𝑣 ∩ 𝑤 ) ∈ 𝑢 ∧ ( ( I ↾ 𝑥 ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ 𝑢 ∧ ∃ 𝑤 ∈ 𝑢 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) ) ) } )
19 18 fvmpt2 ⊢ ( ( 𝑥 ∈ V ∧ { 𝑢 ∣ ( 𝑢 ⊆ 𝒫 ( 𝑥 × 𝑥 ) ∧ ( 𝑥 × 𝑥 ) ∈ 𝑢 ∧ ∀ 𝑣 ∈ 𝑢 ( ∀ 𝑤 ∈ 𝒫 ( 𝑥 × 𝑥 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢 ) ∧ ∀ 𝑤 ∈ 𝑢 ( 𝑣 ∩ 𝑤 ) ∈ 𝑢 ∧ ( ( I ↾ 𝑥 ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ 𝑢 ∧ ∃ 𝑤 ∈ 𝑢 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) ) ) } ∈ V ) → ( UnifOn ‘ 𝑥 ) = { 𝑢 ∣ ( 𝑢 ⊆ 𝒫 ( 𝑥 × 𝑥 ) ∧ ( 𝑥 × 𝑥 ) ∈ 𝑢 ∧ ∀ 𝑣 ∈ 𝑢 ( ∀ 𝑤 ∈ 𝒫 ( 𝑥 × 𝑥 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢 ) ∧ ∀ 𝑤 ∈ 𝑢 ( 𝑣 ∩ 𝑤 ) ∈ 𝑢 ∧ ( ( I ↾ 𝑥 ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ 𝑢 ∧ ∃ 𝑤 ∈ 𝑢 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) ) ) } )
20 6 17 19 mp2an ⊢ ( UnifOn ‘ 𝑥 ) = { 𝑢 ∣ ( 𝑢 ⊆ 𝒫 ( 𝑥 × 𝑥 ) ∧ ( 𝑥 × 𝑥 ) ∈ 𝑢 ∧ ∀ 𝑣 ∈ 𝑢 ( ∀ 𝑤 ∈ 𝒫 ( 𝑥 × 𝑥 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢 ) ∧ ∀ 𝑤 ∈ 𝑢 ( 𝑣 ∩ 𝑤 ) ∈ 𝑢 ∧ ( ( I ↾ 𝑥 ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ 𝑢 ∧ ∃ 𝑤 ∈ 𝑢 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) ) ) }
21 simp2 ⊢ ( ( 𝑢 ⊆ 𝒫 ( 𝑥 × 𝑥 ) ∧ ( 𝑥 × 𝑥 ) ∈ 𝑢 ∧ ∀ 𝑣 ∈ 𝑢 ( ∀ 𝑤 ∈ 𝒫 ( 𝑥 × 𝑥 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢 ) ∧ ∀ 𝑤 ∈ 𝑢 ( 𝑣 ∩ 𝑤 ) ∈ 𝑢 ∧ ( ( I ↾ 𝑥 ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ 𝑢 ∧ ∃ 𝑤 ∈ 𝑢 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) ) ) → ( 𝑥 × 𝑥 ) ∈ 𝑢 )
22 21 ss2abi ⊢ { 𝑢 ∣ ( 𝑢 ⊆ 𝒫 ( 𝑥 × 𝑥 ) ∧ ( 𝑥 × 𝑥 ) ∈ 𝑢 ∧ ∀ 𝑣 ∈ 𝑢 ( ∀ 𝑤 ∈ 𝒫 ( 𝑥 × 𝑥 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢 ) ∧ ∀ 𝑤 ∈ 𝑢 ( 𝑣 ∩ 𝑤 ) ∈ 𝑢 ∧ ( ( I ↾ 𝑥 ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ 𝑢 ∧ ∃ 𝑤 ∈ 𝑢 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) ) ) } ⊆ { 𝑢 ∣ ( 𝑥 × 𝑥 ) ∈ 𝑢 }
23 20 22 eqsstri ⊢ ( UnifOn ‘ 𝑥 ) ⊆ { 𝑢 ∣ ( 𝑥 × 𝑥 ) ∈ 𝑢 }
24 23 sseli ⊢ ( ∅ ∈ ( UnifOn ‘ 𝑥 ) → ∅ ∈ { 𝑢 ∣ ( 𝑥 × 𝑥 ) ∈ 𝑢 } )
25 5 24 mto ⊢ ¬ ∅ ∈ ( UnifOn ‘ 𝑥 )
26 25 nex ⊢ ¬ ∃ 𝑥 ∅ ∈ ( UnifOn ‘ 𝑥 )
27 18 funmpt2 ⊢ Fun UnifOn
28 elunirn ⊢ ( Fun UnifOn → ( ∅ ∈ ∪ ran UnifOn ↔ ∃ 𝑥 ∈ dom UnifOn ∅ ∈ ( UnifOn ‘ 𝑥 ) ) )
29 27 28 ax-mp ⊢ ( ∅ ∈ ∪ ran UnifOn ↔ ∃ 𝑥 ∈ dom UnifOn ∅ ∈ ( UnifOn ‘ 𝑥 ) )
30 ustfn ⊢ UnifOn Fn V
31 fndm ⊢ ( UnifOn Fn V → dom UnifOn = V )
32 30 31 ax-mp ⊢ dom UnifOn = V
33 32 rexeqi ⊢ ( ∃ 𝑥 ∈ dom UnifOn ∅ ∈ ( UnifOn ‘ 𝑥 ) ↔ ∃ 𝑥 ∈ V ∅ ∈ ( UnifOn ‘ 𝑥 ) )
34 rexv ⊢ ( ∃ 𝑥 ∈ V ∅ ∈ ( UnifOn ‘ 𝑥 ) ↔ ∃ 𝑥 ∅ ∈ ( UnifOn ‘ 𝑥 ) )
35 29 33 34 3bitri ⊢ ( ∅ ∈ ∪ ran UnifOn ↔ ∃ 𝑥 ∅ ∈ ( UnifOn ‘ 𝑥 ) )
36 26 35 mtbir ⊢ ¬ ∅ ∈ ∪ ran UnifOn