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 ⊢ TopOn Fn V
8 vuniex ⊢ ⋃ x ∈ V
9 fnfvelrn ⊢ TopOn Fn V ∧ ⋃ 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 → ∃ y x ∈ y ∧ y ∈ ran ⁡ TopOn
15 1 14 sylbi ⊢ x ∈ Top → ∃ y x ∈ y ∧ y ∈ ran ⁡ TopOn
16 funtopon ⊢ Fun ⁡ TopOn
17 elrnrexdm ⊢ Fun ⁡ TopOn → y ∈ ran ⁡ TopOn → ∃ z ∈ dom ⁡ TopOn y = TopOn ⁡ z
18 16 17 ax-mp ⊢ y ∈ ran ⁡ TopOn → ∃ z ∈ dom ⁡ TopOn y = TopOn ⁡ z
19 rexex ⊢ ∃ z ∈ dom ⁡ TopOn y = TopOn ⁡ z → ∃ z y = TopOn ⁡ z
20 18 19 syl ⊢ y ∈ ran ⁡ TopOn → ∃ z y = TopOn ⁡ z
21 19.42v ⊢ ∃ z x ∈ y ∧ y = TopOn ⁡ z ↔ x ∈ y ∧ ∃ z y = 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 ⊢ ∃ z x ∈ y ∧ y = TopOn ⁡ z → ∃ z x ∈ TopOn ⁡ z
26 21 25 sylbir ⊢ x ∈ y ∧ ∃ z y = TopOn ⁡ z → ∃ z x ∈ TopOn ⁡ z
27 20 26 sylan2 ⊢ x ∈ y ∧ y ∈ ran ⁡ TopOn → ∃ z x ∈ TopOn ⁡ z
28 topontop ⊢ x ∈ TopOn ⁡ z → x ∈ Top
29 28 exlimiv ⊢ ∃ z x ∈ TopOn ⁡ z → x ∈ Top
30 27 29 syl ⊢ x ∈ y ∧ y ∈ ran ⁡ TopOn → x ∈ Top
31 30 exlimiv ⊢ ∃ y x ∈ y ∧ y ∈ ran ⁡ TopOn → x ∈ Top
32 15 31 impbii ⊢ x ∈ Top ↔ ∃ y x ∈ y ∧ y ∈ ran ⁡ TopOn
33 eluni ⊢ x ∈ ⋃ ran ⁡ TopOn ↔ ∃ y x ∈ y ∧ y ∈ ran ⁡ TopOn
34 32 33 bitr4i ⊢ x ∈ Top ↔ x ∈ ⋃ ran ⁡ TopOn
35 34 eqriv ⊢ Top = ⋃ ran ⁡ TopOn