Metamath Proof Explorer

Theorem ustbas2

Description: Second direction for ustbas . (Contributed by Thierry Arnoux, 16-Nov-2017)

Ref Expression
Assertion ustbas2 ⊢ U ∈ UnifOn ⁡ X → X = dom ⁡ ⋃ U

Proof

Step Hyp Ref Expression
1 dmxpid ⊢ dom ⁡ X × X = X
2 ustbasel ⊢ U ∈ UnifOn ⁡ X → X × X ∈ U
3 elssuni ⊢ X × X ∈ U → X × X ⊆ ⋃ U
4 2 3 syl ⊢ U ∈ UnifOn ⁡ X → X × X ⊆ ⋃ U
5 elfvex ⊢ U ∈ UnifOn ⁡ X → X ∈ V
6 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
7 5 6 syl ⊢ U ∈ UnifOn ⁡ X → 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
8 7 ibi ⊢ 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
9 8 simp1d ⊢ U ∈ UnifOn ⁡ X → U ⊆ 𝒫 X × X
10 9 unissd ⊢ U ∈ UnifOn ⁡ X → ⋃ U ⊆ ⋃ 𝒫 X × X
11 unipw ⊢ ⋃ 𝒫 X × X = X × X
12 10 11 sseqtrdi ⊢ U ∈ UnifOn ⁡ X → ⋃ U ⊆ X × X
13 4 12 eqssd ⊢ U ∈ UnifOn ⁡ X → X × X = ⋃ U
14 13 dmeqd ⊢ U ∈ UnifOn ⁡ X → dom ⁡ X × X = dom ⁡ ⋃ U
15 1 14 eqtr3id ⊢ U ∈ UnifOn ⁡ X → X = dom ⁡ ⋃ U