This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 eqtr4di ⊢ ( 𝑈 ∈ ( 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 elfvunirn ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑈 ∈ ∪ ran UnifOn )
14 12 13 impbii ⊢ ( 𝑈 ∈ ∪ ran UnifOn ↔ 𝑈 ∈ ( UnifOn ‘ 𝑋 ) )