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

Metamath Proof Explorer

Theorem ustfn

Description: The defined uniform structure as a function. (Contributed by Thierry Arnoux, 15-Nov-2017)

Ref Expression
Assertion ustfn UnifOn Fn V

Proof

Step Hyp Ref Expression
1 velpw ⊢ ( 𝑢 ∈ 𝒫 𝒫 ( 𝑥 × 𝑥 ) ↔ 𝑢 ⊆ 𝒫 ( 𝑥 × 𝑥 ) )
2 1 abbii ⊢ { 𝑢 ∣ 𝑢 ∈ 𝒫 𝒫 ( 𝑥 × 𝑥 ) } = { 𝑢 ∣ 𝑢 ⊆ 𝒫 ( 𝑥 × 𝑥 ) }
3 abid2 ⊢ { 𝑢 ∣ 𝑢 ∈ 𝒫 𝒫 ( 𝑥 × 𝑥 ) } = 𝒫 𝒫 ( 𝑥 × 𝑥 )
4 vex ⊢ 𝑥 ∈ V
5 4 4 xpex ⊢ ( 𝑥 × 𝑥 ) ∈ V
6 5 pwex ⊢ 𝒫 ( 𝑥 × 𝑥 ) ∈ V
7 6 pwex ⊢ 𝒫 𝒫 ( 𝑥 × 𝑥 ) ∈ V
8 3 7 eqeltri ⊢ { 𝑢 ∣ 𝑢 ∈ 𝒫 𝒫 ( 𝑥 × 𝑥 ) } ∈ V
9 2 8 eqeltrri ⊢ { 𝑢 ∣ 𝑢 ⊆ 𝒫 ( 𝑥 × 𝑥 ) } ∈ V
10 simp1 ⊢ ( ( 𝑢 ⊆ 𝒫 ( 𝑥 × 𝑥 ) ∧ ( 𝑥 × 𝑥 ) ∈ 𝑢 ∧ ∀ 𝑣 ∈ 𝑢 ( ∀ 𝑤 ∈ 𝒫 ( 𝑥 × 𝑥 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢 ) ∧ ∀ 𝑤 ∈ 𝑢 ( 𝑣 ∩ 𝑤 ) ∈ 𝑢 ∧ ( ( I ↾ 𝑥 ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ 𝑢 ∧ ∃ 𝑤 ∈ 𝑢 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) ) ) → 𝑢 ⊆ 𝒫 ( 𝑥 × 𝑥 ) )
11 10 ss2abi ⊢ { 𝑢 ∣ ( 𝑢 ⊆ 𝒫 ( 𝑥 × 𝑥 ) ∧ ( 𝑥 × 𝑥 ) ∈ 𝑢 ∧ ∀ 𝑣 ∈ 𝑢 ( ∀ 𝑤 ∈ 𝒫 ( 𝑥 × 𝑥 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢 ) ∧ ∀ 𝑤 ∈ 𝑢 ( 𝑣 ∩ 𝑤 ) ∈ 𝑢 ∧ ( ( I ↾ 𝑥 ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ 𝑢 ∧ ∃ 𝑤 ∈ 𝑢 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) ) ) } ⊆ { 𝑢 ∣ 𝑢 ⊆ 𝒫 ( 𝑥 × 𝑥 ) }
12 9 11 ssexi ⊢ { 𝑢 ∣ ( 𝑢 ⊆ 𝒫 ( 𝑥 × 𝑥 ) ∧ ( 𝑥 × 𝑥 ) ∈ 𝑢 ∧ ∀ 𝑣 ∈ 𝑢 ( ∀ 𝑤 ∈ 𝒫 ( 𝑥 × 𝑥 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢 ) ∧ ∀ 𝑤 ∈ 𝑢 ( 𝑣 ∩ 𝑤 ) ∈ 𝑢 ∧ ( ( I ↾ 𝑥 ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ 𝑢 ∧ ∃ 𝑤 ∈ 𝑢 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) ) ) } ∈ V
13 df-ust ⊢ UnifOn = ( 𝑥 ∈ V ↦ { 𝑢 ∣ ( 𝑢 ⊆ 𝒫 ( 𝑥 × 𝑥 ) ∧ ( 𝑥 × 𝑥 ) ∈ 𝑢 ∧ ∀ 𝑣 ∈ 𝑢 ( ∀ 𝑤 ∈ 𝒫 ( 𝑥 × 𝑥 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢 ) ∧ ∀ 𝑤 ∈ 𝑢 ( 𝑣 ∩ 𝑤 ) ∈ 𝑢 ∧ ( ( I ↾ 𝑥 ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ 𝑢 ∧ ∃ 𝑤 ∈ 𝑢 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) ) ) } )
14 12 13 fnmpti ⊢ UnifOn Fn V