Metamath Proof Explorer

Theorem ustval

Description: The class of all uniform structures for a base X . (Contributed by Thierry Arnoux, 15-Nov-2017) (Revised by AV, 17-Sep-2021)

Ref Expression
Assertion ustval ⊢ X ∈ 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

Proof

Step Hyp Ref Expression
1 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
2 id ⊢ x = X → x = X
3 2 sqxpeqd ⊢ x = X → x × x = X × X
4 3 pweqd ⊢ x = X → 𝒫 x × x = 𝒫 X × X
5 4 sseq2d ⊢ x = X → u ⊆ 𝒫 x × x ↔ u ⊆ 𝒫 X × X
6 3 eleq1d ⊢ x = X → x × x ∈ u ↔ X × X ∈ u
7 4 raleqdv ⊢ x = X → ∀ w ∈ 𝒫 x × x v ⊆ w → w ∈ u ↔ ∀ w ∈ 𝒫 X × X v ⊆ w → w ∈ u
8 reseq2 ⊢ x = X → I ↾ x = I ↾ X
9 8 sseq1d ⊢ x = X → I ↾ x ⊆ v ↔ I ↾ X ⊆ v
10 9 3anbi1d ⊢ x = X → I ↾ x ⊆ v ∧ v -1 ∈ u ∧ ∃ w ∈ u w ∘ w ⊆ v ↔ I ↾ X ⊆ v ∧ v -1 ∈ u ∧ ∃ w ∈ u w ∘ w ⊆ v
11 7 10 3anbi13d ⊢ x = X → ∀ w ∈ 𝒫 x × x v ⊆ w → w ∈ u ∧ ∀ w ∈ u v ∩ w ∈ u ∧ I ↾ x ⊆ v ∧ v -1 ∈ u ∧ ∃ w ∈ u w ∘ w ⊆ v ↔ ∀ w ∈ 𝒫 X × X v ⊆ w → w ∈ u ∧ ∀ w ∈ u v ∩ w ∈ u ∧ I ↾ X ⊆ v ∧ v -1 ∈ u ∧ ∃ w ∈ u w ∘ w ⊆ v
12 11 ralbidv ⊢ x = X → ∀ 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 ∈ u ∀ w ∈ 𝒫 X × X v ⊆ w → w ∈ u ∧ ∀ w ∈ u v ∩ w ∈ u ∧ I ↾ X ⊆ v ∧ v -1 ∈ u ∧ ∃ w ∈ u w ∘ w ⊆ v
13 5 6 12 3anbi123d ⊢ x = X → 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 ∧ 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 13 abbidv ⊢ x = 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 = 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
15 elex ⊢ X ∈ V → X ∈ V
16 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
17 16 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
18 df-pw ⊢ 𝒫 𝒫 X × X = u | u ⊆ 𝒫 X × X
19 17 18 sseqtrri ⊢ 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 ⊆ 𝒫 𝒫 X × X
20 sqxpexg ⊢ X ∈ V → X × X ∈ V
21 pwexg ⊢ X × X ∈ V → 𝒫 X × X ∈ V
22 pwexg ⊢ 𝒫 X × X ∈ V → 𝒫 𝒫 X × X ∈ V
23 20 21 22 3syl ⊢ X ∈ V → 𝒫 𝒫 X × X ∈ V
24 ssexg ⊢ 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 ⊆ 𝒫 𝒫 X × X ∧ 𝒫 𝒫 X × 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
25 19 23 24 sylancr ⊢ 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
26 1 14 15 25 fvmptd3 ⊢ X ∈ 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