Metamath Proof Explorer

Theorem toprntopon

Description: A topology is the same thing as a topology on a set (variable-free version). (Contributed by BJ, 27-Apr-2021)

Ref Expression
Assertion toprntopon ⊢Top=⋃ran⁡TopOn

Proof

Step Hyp Ref Expression
1 toptopon2 ⊢x∈Top↔x∈TopOn⁡⋃x
2 fvex ⊢TopOn⁡⋃x∈V
3 eleq2 ⊢y=TopOn⁡⋃x→x∈y↔x∈TopOn⁡⋃x
4 eleq1 ⊢y=TopOn⁡⋃x→y∈ran⁡TopOn↔TopOn⁡⋃x∈ran⁡TopOn
5 3 4 anbi12d ⊢y=TopOn⁡⋃x→x∈y∧y∈ran⁡TopOn↔x∈TopOn⁡⋃x∧TopOn⁡⋃x∈ran⁡TopOn
6 simpl ⊢x∈TopOn⁡⋃x∧TopOn⁡⋃x∈ran⁡TopOn→x∈TopOn⁡⋃x
7 fntopon ⊢TopOnFnV
8 vuniex ⊢⋃x∈V
9 fnfvelrn ⊢TopOnFnV∧⋃x∈V→TopOn⁡⋃x∈ran⁡TopOn
10 7 8 9 mp2an ⊢TopOn⁡⋃x∈ran⁡TopOn
11 10 jctr ⊢x∈TopOn⁡⋃x→x∈TopOn⁡⋃x∧TopOn⁡⋃x∈ran⁡TopOn
12 6 11 impbii ⊢x∈TopOn⁡⋃x∧TopOn⁡⋃x∈ran⁡TopOn↔x∈TopOn⁡⋃x
13 5 12 bitrdi ⊢y=TopOn⁡⋃x→x∈y∧y∈ran⁡TopOn↔x∈TopOn⁡⋃x
14 2 13 spcev ⊢x∈TopOn⁡⋃x→∃yx∈y∧y∈ran⁡TopOn
15 1 14 sylbi ⊢x∈Top→∃yx∈y∧y∈ran⁡TopOn
16 funtopon ⊢Fun⁡TopOn
17 elrnrexdm ⊢Fun⁡TopOn→y∈ran⁡TopOn→∃z∈dom⁡TopOny=TopOn⁡z
18 16 17 ax-mp ⊢y∈ran⁡TopOn→∃z∈dom⁡TopOny=TopOn⁡z
19 rexex ⊢∃z∈dom⁡TopOny=TopOn⁡z→∃zy=TopOn⁡z
20 18 19 syl ⊢y∈ran⁡TopOn→∃zy=TopOn⁡z
21 19.42v ⊢∃zx∈y∧y=TopOn⁡z↔x∈y∧∃zy=TopOn⁡z
22 eqimss ⊢y=TopOn⁡z→y⊆TopOn⁡z
23 22 sseld ⊢y=TopOn⁡z→x∈y→x∈TopOn⁡z
24 23 impcom ⊢x∈y∧y=TopOn⁡z→x∈TopOn⁡z
25 24 eximi ⊢∃zx∈y∧y=TopOn⁡z→∃zx∈TopOn⁡z
26 21 25 sylbir ⊢x∈y∧∃zy=TopOn⁡z→∃zx∈TopOn⁡z
27 20 26 sylan2 ⊢x∈y∧y∈ran⁡TopOn→∃zx∈TopOn⁡z
28 topontop ⊢x∈TopOn⁡z→x∈Top
29 28 exlimiv ⊢∃zx∈TopOn⁡z→x∈Top
30 27 29 syl ⊢x∈y∧y∈ran⁡TopOn→x∈Top
31 30 exlimiv ⊢∃yx∈y∧y∈ran⁡TopOn→x∈Top
32 15 31 impbii ⊢x∈Top↔∃yx∈y∧y∈ran⁡TopOn
33 eluni ⊢x∈⋃ran⁡TopOn↔∃yx∈y∧y∈ran⁡TopOn
34 32 33 bitr4i ⊢x∈Top↔x∈⋃ran⁡TopOn
35 34 eqriv ⊢Top=⋃ran⁡TopOn