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 B V x A C B x A C topGen B

Proof

Step Hyp Ref Expression
1 dfiun3g x A C B x A C = ran x A C
2 1 adantl B V x A C B x A C = ran x A C
3 eqid x A C = x A C
4 3 rnmptss x A C B ran x A C B
5 eltg3i B V ran x A C B ran x A C topGen B
6 4 5 sylan2 B V x A C B ran x A C topGen B
7 2 6 eqeltrd B V x A C B x A C topGen B