Metamath Proof Explorer


Theorem tgiun

Description: The indexed union of a set of basic open sets is in the generated topology. (Contributed by Mario Carneiro, 2-Sep-2015)

Ref Expression
Assertion tgiun BVxACBxACtopGenB

Proof

Step Hyp Ref Expression
1 dfiun3g xACBxAC=ranxAC
2 1 adantl BVxACBxAC=ranxAC
3 eqid xAC=xAC
4 3 rnmptss xACBranxACB
5 eltg3i BVranxACBranxACtopGenB
6 4 5 sylan2 BVxACBranxACtopGenB
7 2 6 eqeltrd BVxACBxACtopGenB