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 𝑋 = dom 𝑈
Assertion ustbas ( 𝑈 ran UnifOn ↔ 𝑈 ∈ ( UnifOn ‘ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 ustbas.1 𝑋 = dom 𝑈
2 ustfn UnifOn Fn V
3 fnfun ( UnifOn Fn V → Fun UnifOn )
4 elunirn ( Fun UnifOn → ( 𝑈 ran UnifOn ↔ ∃ 𝑥 ∈ dom UnifOn 𝑈 ∈ ( UnifOn ‘ 𝑥 ) ) )
5 2 3 4 mp2b ( 𝑈 ran UnifOn ↔ ∃ 𝑥 ∈ dom UnifOn 𝑈 ∈ ( UnifOn ‘ 𝑥 ) )
6 ustbas2 ( 𝑈 ∈ ( UnifOn ‘ 𝑥 ) → 𝑥 = dom 𝑈 )
7 6 1 syl6eqr ( 𝑈 ∈ ( UnifOn ‘ 𝑥 ) → 𝑥 = 𝑋 )
8 7 fveq2d ( 𝑈 ∈ ( UnifOn ‘ 𝑥 ) → ( UnifOn ‘ 𝑥 ) = ( UnifOn ‘ 𝑋 ) )
9 8 eleq2d ( 𝑈 ∈ ( UnifOn ‘ 𝑥 ) → ( 𝑈 ∈ ( UnifOn ‘ 𝑥 ) ↔ 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ) )
10 9 ibi ( 𝑈 ∈ ( UnifOn ‘ 𝑥 ) → 𝑈 ∈ ( UnifOn ‘ 𝑋 ) )
11 10 rexlimivw ( ∃ 𝑥 ∈ dom UnifOn 𝑈 ∈ ( UnifOn ‘ 𝑥 ) → 𝑈 ∈ ( UnifOn ‘ 𝑋 ) )
12 5 11 sylbi ( 𝑈 ran UnifOn → 𝑈 ∈ ( UnifOn ‘ 𝑋 ) )
13 elrnust ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑈 ran UnifOn )
14 12 13 impbii ( 𝑈 ran UnifOn ↔ 𝑈 ∈ ( UnifOn ‘ 𝑋 ) )