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 × 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 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
2 1 eleq2d ⊢ X ∈ V → U ∈ UnifOn ⁡ X ↔ U ∈ 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
3 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
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 × X v ⊆ w → w ∈ U ∧ ∀ w ∈ U v ∩ w ∈ U ∧ I ↾ X ⊆ v ∧ v -1 ∈ U ∧ ∃ w ∈ U w ∘ 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 × X v ⊆ w → w ∈ u ↔ ∀ w ∈ 𝒫 X × X v ⊆ w → w ∈ U
16 eleq2 ⊢ u = U → v ∩ w ∈ u ↔ v ∩ w ∈ U
17 16 raleqbi1dv ⊢ u = U → ∀ w ∈ u v ∩ w ∈ u ↔ ∀ w ∈ U v ∩ w ∈ U
18 eleq2 ⊢ u = U → v -1 ∈ u ↔ v -1 ∈ U
19 rexeq ⊢ u = U → ∃ w ∈ u w ∘ w ⊆ v ↔ ∃ w ∈ U w ∘ w ⊆ v
20 18 19 3anbi23d ⊢ u = U → I ↾ X ⊆ v ∧ v -1 ∈ u ∧ ∃ w ∈ u w ∘ w ⊆ v ↔ I ↾ X ⊆ v ∧ v -1 ∈ U ∧ ∃ w ∈ U w ∘ w ⊆ v
21 15 17 20 3anbi123d ⊢ u = U → ∀ 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
22 21 raleqbi1dv ⊢ u = 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 ∈ U ∀ w ∈ 𝒫 X × X v ⊆ w → w ∈ U ∧ ∀ w ∈ U v ∩ w ∈ U ∧ I ↾ X ⊆ v ∧ v -1 ∈ U ∧ ∃ w ∈ U w ∘ w ⊆ v
23 11 12 22 3anbi123d ⊢ u = 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 ⊆ 𝒫 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
24 23 elab3g ⊢ 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 ∈ V → U ∈ 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 ⊆ 𝒫 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
25 10 24 syl ⊢ X ∈ V → U ∈ 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 ⊆ 𝒫 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
26 2 25 bitrd ⊢ X ∈ V → U ∈ UnifOn ⁡ 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