This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝑥 ∈ Top ↔ 𝑥 ∈ ( TopOn ‘ ∪ 𝑥 ) )
2 fvex ⊢ ( TopOn ‘ ∪ 𝑥 ) ∈ V
3 eleq2 ⊢ ( 𝑦 = ( TopOn ‘ ∪ 𝑥 ) → ( 𝑥 ∈ 𝑦 ↔ 𝑥 ∈ ( TopOn ‘ ∪ 𝑥 ) ) )
4 eleq1 ⊢ ( 𝑦 = ( TopOn ‘ ∪ 𝑥 ) → ( 𝑦 ∈ ran TopOn ↔ ( TopOn ‘ ∪ 𝑥 ) ∈ ran TopOn ) )
5 3 4 anbi12d ⊢ ( 𝑦 = ( TopOn ‘ ∪ 𝑥 ) → ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ran TopOn ) ↔ ( 𝑥 ∈ ( TopOn ‘ ∪ 𝑥 ) ∧ ( TopOn ‘ ∪ 𝑥 ) ∈ ran TopOn ) ) )
6 simpl ⊢ ( ( 𝑥 ∈ ( TopOn ‘ ∪ 𝑥 ) ∧ ( TopOn ‘ ∪ 𝑥 ) ∈ ran TopOn ) → 𝑥 ∈ ( TopOn ‘ ∪ 𝑥 ) )
7 fntopon ⊢ TopOn Fn V
8 vuniex ⊢ ∪ 𝑥 ∈ V
9 fnfvelrn ⊢ ( ( TopOn Fn V ∧ ∪ 𝑥 ∈ V ) → ( TopOn ‘ ∪ 𝑥 ) ∈ ran TopOn )
10 7 8 9 mp2an ⊢ ( TopOn ‘ ∪ 𝑥 ) ∈ ran TopOn
11 10 jctr ⊢ ( 𝑥 ∈ ( TopOn ‘ ∪ 𝑥 ) → ( 𝑥 ∈ ( TopOn ‘ ∪ 𝑥 ) ∧ ( TopOn ‘ ∪ 𝑥 ) ∈ ran TopOn ) )
12 6 11 impbii ⊢ ( ( 𝑥 ∈ ( TopOn ‘ ∪ 𝑥 ) ∧ ( TopOn ‘ ∪ 𝑥 ) ∈ ran TopOn ) ↔ 𝑥 ∈ ( TopOn ‘ ∪ 𝑥 ) )
13 5 12 bitrdi ⊢ ( 𝑦 = ( TopOn ‘ ∪ 𝑥 ) → ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ran TopOn ) ↔ 𝑥 ∈ ( TopOn ‘ ∪ 𝑥 ) ) )
14 2 13 spcev ⊢ ( 𝑥 ∈ ( TopOn ‘ ∪ 𝑥 ) → ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ran TopOn ) )
15 1 14 sylbi ⊢ ( 𝑥 ∈ Top → ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ran TopOn ) )
16 funtopon ⊢ Fun TopOn
17 elrnrexdm ⊢ ( Fun TopOn → ( 𝑦 ∈ ran TopOn → ∃ 𝑧 ∈ dom TopOn 𝑦 = ( TopOn ‘ 𝑧 ) ) )
18 16 17 ax-mp ⊢ ( 𝑦 ∈ ran TopOn → ∃ 𝑧 ∈ dom TopOn 𝑦 = ( TopOn ‘ 𝑧 ) )
19 rexex ⊢ ( ∃ 𝑧 ∈ dom TopOn 𝑦 = ( TopOn ‘ 𝑧 ) → ∃ 𝑧 𝑦 = ( TopOn ‘ 𝑧 ) )
20 18 19 syl ⊢ ( 𝑦 ∈ ran TopOn → ∃ 𝑧 𝑦 = ( TopOn ‘ 𝑧 ) )
21 19.42v ⊢ ( ∃ 𝑧 ( 𝑥 ∈ 𝑦 ∧ 𝑦 = ( TopOn ‘ 𝑧 ) ) ↔ ( 𝑥 ∈ 𝑦 ∧ ∃ 𝑧 𝑦 = ( TopOn ‘ 𝑧 ) ) )
22 eqimss ⊢ ( 𝑦 = ( TopOn ‘ 𝑧 ) → 𝑦 ⊆ ( TopOn ‘ 𝑧 ) )
23 22 sseld ⊢ ( 𝑦 = ( TopOn ‘ 𝑧 ) → ( 𝑥 ∈ 𝑦 → 𝑥 ∈ ( TopOn ‘ 𝑧 ) ) )
24 23 impcom ⊢ ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 = ( TopOn ‘ 𝑧 ) ) → 𝑥 ∈ ( TopOn ‘ 𝑧 ) )
25 24 eximi ⊢ ( ∃ 𝑧 ( 𝑥 ∈ 𝑦 ∧ 𝑦 = ( TopOn ‘ 𝑧 ) ) → ∃ 𝑧 𝑥 ∈ ( TopOn ‘ 𝑧 ) )
26 21 25 sylbir ⊢ ( ( 𝑥 ∈ 𝑦 ∧ ∃ 𝑧 𝑦 = ( TopOn ‘ 𝑧 ) ) → ∃ 𝑧 𝑥 ∈ ( TopOn ‘ 𝑧 ) )
27 20 26 sylan2 ⊢ ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ran TopOn ) → ∃ 𝑧 𝑥 ∈ ( TopOn ‘ 𝑧 ) )
28 topontop ⊢ ( 𝑥 ∈ ( TopOn ‘ 𝑧 ) → 𝑥 ∈ Top )
29 28 exlimiv ⊢ ( ∃ 𝑧 𝑥 ∈ ( TopOn ‘ 𝑧 ) → 𝑥 ∈ Top )
30 27 29 syl ⊢ ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ran TopOn ) → 𝑥 ∈ Top )
31 30 exlimiv ⊢ ( ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ran TopOn ) → 𝑥 ∈ Top )
32 15 31 impbii ⊢ ( 𝑥 ∈ Top ↔ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ran TopOn ) )
33 eluni ⊢ ( 𝑥 ∈ ∪ ran TopOn ↔ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ran TopOn ) )
34 32 33 bitr4i ⊢ ( 𝑥 ∈ Top ↔ 𝑥 ∈ ∪ ran TopOn )
35 34 eqriv ⊢ Top = ∪ ran TopOn