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 syl6eqr 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