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