Description: Closure of the base set in a uniform limit. (Contributed by Mario Carneiro, 26-Feb-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | ulmscl | ⊢ ( 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 → 𝑆 ∈ V ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-br | ⊢ ( 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ↔ 〈 𝐹 , 𝐺 〉 ∈ ( ⇝𝑢 ‘ 𝑆 ) ) | |
2 | elfvex | ⊢ ( 〈 𝐹 , 𝐺 〉 ∈ ( ⇝𝑢 ‘ 𝑆 ) → 𝑆 ∈ V ) | |
3 | 1 2 | sylbi | ⊢ ( 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 → 𝑆 ∈ V ) |