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 ⊢ u ∈ 𝒫 𝒫 x × x ↔ u ⊆ 𝒫 x × x
2 1 abbii ⊢ u | u ∈ 𝒫 𝒫 x × x = u | u ⊆ 𝒫 x × x
3 abid2 ⊢ u | u ∈ 𝒫 𝒫 x × x = 𝒫 𝒫 x × x
4 vex ⊢ x ∈ V
5 4 4 xpex ⊢ x × x ∈ V
6 5 pwex ⊢ 𝒫 x × x ∈ V
7 6 pwex ⊢ 𝒫 𝒫 x × x ∈ V
8 3 7 eqeltri ⊢ u | u ∈ 𝒫 𝒫 x × x ∈ V
9 2 8 eqeltrri ⊢ u | u ⊆ 𝒫 x × x ∈ V
10 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
11 10 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
12 9 11 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
13 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
14 12 13 fnmpti ⊢ UnifOn Fn V