Metamath Proof Explorer

Theorem isust

Description: The predicate " U is a uniform structure with base X ". (Contributed by Thierry Arnoux, 15-Nov-2017) (Revised by AV, 17-Sep-2021)

Ref Expression
Assertion isust ⊢X∈V→U∈UnifOn⁡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

Proof

Step Hyp Ref Expression
1 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
2 1 eleq2d ⊢X∈V→U∈UnifOn⁡X↔U∈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
3 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
4 sqxpexg ⊢X∈V→X×X∈V
5 4 pwexd ⊢X∈V→𝒫X×X∈V
6 5 adantr ⊢X∈V∧U⊆𝒫X×X→𝒫X×X∈V
7 simpr ⊢X∈V∧U⊆𝒫X×X→U⊆𝒫X×X
8 6 7 ssexd ⊢X∈V∧U⊆𝒫X×X→U∈V
9 8 ex ⊢X∈V→U⊆𝒫X×X→U∈V
10 3 9 syl5 ⊢X∈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→U∈V
11 sseq1 ⊢u=U→u⊆𝒫X×X↔U⊆𝒫X×X
12 eleq2 ⊢u=U→X×X∈u↔X×X∈U
13 eleq2 ⊢u=U→w∈u↔w∈U
14 13 imbi2d ⊢u=U→v⊆w→w∈u↔v⊆w→w∈U
15 14 ralbidv ⊢u=U→∀w∈𝒫X×Xv⊆w→w∈u↔∀w∈𝒫X×Xv⊆w→w∈U
16 eleq2 ⊢u=U→v∩w∈u↔v∩w∈U
17 16 raleqbi1dv ⊢u=U→∀w∈uv∩w∈u↔∀w∈Uv∩w∈U
18 eleq2 ⊢u=U→v-1∈u↔v-1∈U
19 rexeq ⊢u=U→∃w∈uw∘w⊆v↔∃w∈Uw∘w⊆v
20 18 19 3anbi23d ⊢u=U→I↾X⊆v∧v-1∈u∧∃w∈uw∘w⊆v↔I↾X⊆v∧v-1∈U∧∃w∈Uw∘w⊆v
21 15 17 20 3anbi123d ⊢u=U→∀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
22 21 raleqbi1dv ⊢u=U→∀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
23 11 12 22 3anbi123d ⊢u=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⊆𝒫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
24 23 elab3g ⊢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∈V→U∈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⊆𝒫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
25 10 24 syl ⊢X∈V→U∈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⊆𝒫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
26 2 25 bitrd ⊢X∈V→U∈UnifOn⁡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