Metamath Proof Explorer

Theorem ustbas

Description: Recover the base of an uniform structure U . U. ran UnifOn is to UnifOn what Top is to TopOn . (Contributed by Thierry Arnoux, 16-Nov-2017)

Ref Expression
Hypothesis ustbas.1 ⊢ X = dom ⁡ ⋃ U
Assertion ustbas ⊢ U ∈ ⋃ ran ⁡ UnifOn ↔ U ∈ UnifOn ⁡ X

Proof

Step Hyp Ref Expression
1 ustbas.1 ⊢ X = dom ⁡ ⋃ U
2 ustfn ⊢ UnifOn Fn V
3 fnfun ⊢ UnifOn Fn V → Fun ⁡ UnifOn
4 elunirn ⊢ Fun ⁡ UnifOn → U ∈ ⋃ ran ⁡ UnifOn ↔ ∃ x ∈ dom ⁡ UnifOn U ∈ UnifOn ⁡ x
5 2 3 4 mp2b ⊢ U ∈ ⋃ ran ⁡ UnifOn ↔ ∃ x ∈ dom ⁡ UnifOn U ∈ UnifOn ⁡ x
6 ustbas2 ⊢ U ∈ UnifOn ⁡ x → x = dom ⁡ ⋃ U
7 6 1 eqtr4di ⊢ U ∈ UnifOn ⁡ x → x = X
8 7 fveq2d ⊢ U ∈ UnifOn ⁡ x → UnifOn ⁡ x = UnifOn ⁡ X
9 8 eleq2d ⊢ U ∈ UnifOn ⁡ x → U ∈ UnifOn ⁡ x ↔ U ∈ UnifOn ⁡ X
10 9 ibi ⊢ U ∈ UnifOn ⁡ x → U ∈ UnifOn ⁡ X
11 10 rexlimivw ⊢ ∃ x ∈ dom ⁡ UnifOn U ∈ UnifOn ⁡ x → U ∈ UnifOn ⁡ X
12 5 11 sylbi ⊢ U ∈ ⋃ ran ⁡ UnifOn → U ∈ UnifOn ⁡ X
13 elrnust ⊢ U ∈ UnifOn ⁡ X → U ∈ ⋃ ran ⁡ UnifOn
14 12 13 impbii ⊢ U ∈ ⋃ ran ⁡ UnifOn ↔ U ∈ UnifOn ⁡ X