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×Xv⊆w→w∈u∧∀w∈uv∩w∈u∧I↾X⊆v∧v-1∈u∧∃w∈uw∘w⊆v

Proof

Step Hyp Ref Expression
1 df-ust ⊢UnifOn=x∈V⟼u|u⊆𝒫x×x∧x×x∈u∧∀v∈u∀w∈𝒫x×xv⊆w→w∈u∧∀w∈uv∩w∈u∧I↾x⊆v∧v-1∈u∧∃w∈uw∘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×xv⊆w→w∈u↔∀w∈𝒫X×Xv⊆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∈uw∘w⊆v↔I↾X⊆v∧v-1∈u∧∃w∈uw∘w⊆v
11 7 10 3anbi13d ⊢x=X→∀w∈𝒫x×xv⊆w→w∈u∧∀w∈uv∩w∈u∧I↾x⊆v∧v-1∈u∧∃w∈uw∘w⊆v↔∀w∈𝒫X×Xv⊆w→w∈u∧∀w∈uv∩w∈u∧I↾X⊆v∧v-1∈u∧∃w∈uw∘w⊆v
12 11 ralbidv ⊢x=X→∀v∈u∀w∈𝒫x×xv⊆w→w∈u∧∀w∈uv∩w∈u∧I↾x⊆v∧v-1∈u∧∃w∈uw∘w⊆v↔∀v∈u∀w∈𝒫X×Xv⊆w→w∈u∧∀w∈uv∩w∈u∧I↾X⊆v∧v-1∈u∧∃w∈uw∘w⊆v
13 5 6 12 3anbi123d ⊢x=X→u⊆𝒫x×x∧x×x∈u∧∀v∈u∀w∈𝒫x×xv⊆w→w∈u∧∀w∈uv∩w∈u∧I↾x⊆v∧v-1∈u∧∃w∈uw∘w⊆v↔u⊆𝒫X×X∧X×X∈u∧∀v∈u∀w∈𝒫X×Xv⊆w→w∈u∧∀w∈uv∩w∈u∧I↾X⊆v∧v-1∈u∧∃w∈uw∘w⊆v
14 13 abbidv ⊢x=X→u|u⊆𝒫x×x∧x×x∈u∧∀v∈u∀w∈𝒫x×xv⊆w→w∈u∧∀w∈uv∩w∈u∧I↾x⊆v∧v-1∈u∧∃w∈uw∘w⊆v=u|u⊆𝒫X×X∧X×X∈u∧∀v∈u∀w∈𝒫X×Xv⊆w→w∈u∧∀w∈uv∩w∈u∧I↾X⊆v∧v-1∈u∧∃w∈uw∘w⊆v
15 elex ⊢X∈V→X∈V
16 simp1 ⊢u⊆𝒫X×X∧X×X∈u∧∀v∈u∀w∈𝒫X×Xv⊆w→w∈u∧∀w∈uv∩w∈u∧I↾X⊆v∧v-1∈u∧∃w∈uw∘w⊆v→u⊆𝒫X×X
17 16 ss2abi ⊢u|u⊆𝒫X×X∧X×X∈u∧∀v∈u∀w∈𝒫X×Xv⊆w→w∈u∧∀w∈uv∩w∈u∧I↾X⊆v∧v-1∈u∧∃w∈uw∘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×Xv⊆w→w∈u∧∀w∈uv∩w∈u∧I↾X⊆v∧v-1∈u∧∃w∈uw∘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×Xv⊆w→w∈u∧∀w∈uv∩w∈u∧I↾X⊆v∧v-1∈u∧∃w∈uw∘w⊆v⊆𝒫𝒫X×X∧𝒫𝒫X×X∈V→u|u⊆𝒫X×X∧X×X∈u∧∀v∈u∀w∈𝒫X×Xv⊆w→w∈u∧∀w∈uv∩w∈u∧I↾X⊆v∧v-1∈u∧∃w∈uw∘w⊆v∈V
25 19 23 24 sylancr ⊢X∈V→u|u⊆𝒫X×X∧X×X∈u∧∀v∈u∀w∈𝒫X×Xv⊆w→w∈u∧∀w∈uv∩w∈u∧I↾X⊆v∧v-1∈u∧∃w∈uw∘w⊆v∈V
26 1 14 15 25 fvmptd3 ⊢X∈V→UnifOn⁡X=u|u⊆𝒫X×X∧X×X∈u∧∀v∈u∀w∈𝒫X×Xv⊆w→w∈u∧∀w∈uv∩w∈u∧I↾X⊆v∧v-1∈u∧∃w∈uw∘w⊆v