On April 22, 2024 11:20:58 PM PDT, "'B. Wilson' via Metamath"
wrote:
>It looks suspiciously close to A e. _V which reas as "A is a set", but in this
>case the V is just floating. What are the semantics here?
>
It functions much like A e. _V would. A proof using this theorem can always
plug
The A e. V antecedent is confusing me. Might I ask for a quick pointer?
85195 indistopon $p |- ( A e. V -> { (/) , A } e. ( TopOn ` A ) ) $= ... $.
It looks suspiciously close to A e. _V which reas as "A is a set", but in this
case the V is just floating. What are the semantics here?
--
