Theorem istopon

Description: Property of being a topology with a given base set. (Contributed by Stefan O'Rear, 31-Jan-2015) (Revised by Mario Carneiro, 13-Aug-2015)

	Ref	Expression
Assertion	istopon	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝐵 ) ↔ ( 𝐽 ∈ Top ∧ 𝐵 = ∪ 𝐽 ) )

Proof

Step	Hyp	Ref	Expression
1		elfvex	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝐵 ) → 𝐵 ∈ V )
2		uniexg	⊢ ( 𝐽 ∈ Top → ∪ 𝐽 ∈ V )
3		eleq1	⊢ ( 𝐵 = ∪ 𝐽 → ( 𝐵 ∈ V ↔ ∪ 𝐽 ∈ V ) )
4	2 3	syl5ibrcom	⊢ ( 𝐽 ∈ Top → ( 𝐵 = ∪ 𝐽 → 𝐵 ∈ V ) )
5	4	imp	⊢ ( ( 𝐽 ∈ Top ∧ 𝐵 = ∪ 𝐽 ) → 𝐵 ∈ V )
6		eqeq1	⊢ ( 𝑏 = 𝐵 → ( 𝑏 = ∪ 𝑗 ↔ 𝐵 = ∪ 𝑗 ) )
7	6	rabbidv	⊢ ( 𝑏 = 𝐵 → { 𝑗 ∈ Top ∣ 𝑏 = ∪ 𝑗 } = { 𝑗 ∈ Top ∣ 𝐵 = ∪ 𝑗 } )
8		df-topon	⊢ TopOn = ( 𝑏 ∈ V ↦ { 𝑗 ∈ Top ∣ 𝑏 = ∪ 𝑗 } )
9		vpwex	⊢ 𝒫 𝑏 ∈ V
10	9	pwex	⊢ 𝒫 𝒫 𝑏 ∈ V
11		rabss	⊢ ( { 𝑗 ∈ Top ∣ 𝑏 = ∪ 𝑗 } ⊆ 𝒫 𝒫 𝑏 ↔ ∀ 𝑗 ∈ Top ( 𝑏 = ∪ 𝑗 → 𝑗 ∈ 𝒫 𝒫 𝑏 ) )
12		pwuni	⊢ 𝑗 ⊆ 𝒫 ∪ 𝑗
13		pweq	⊢ ( 𝑏 = ∪ 𝑗 → 𝒫 𝑏 = 𝒫 ∪ 𝑗 )
14	12 13	sseqtrrid	⊢ ( 𝑏 = ∪ 𝑗 → 𝑗 ⊆ 𝒫 𝑏 )
15		velpw	⊢ ( 𝑗 ∈ 𝒫 𝒫 𝑏 ↔ 𝑗 ⊆ 𝒫 𝑏 )
16	14 15	sylibr	⊢ ( 𝑏 = ∪ 𝑗 → 𝑗 ∈ 𝒫 𝒫 𝑏 )
17	16	a1i	⊢ ( 𝑗 ∈ Top → ( 𝑏 = ∪ 𝑗 → 𝑗 ∈ 𝒫 𝒫 𝑏 ) )
18	11 17	mprgbir	⊢ { 𝑗 ∈ Top ∣ 𝑏 = ∪ 𝑗 } ⊆ 𝒫 𝒫 𝑏
19	10 18	ssexi	⊢ { 𝑗 ∈ Top ∣ 𝑏 = ∪ 𝑗 } ∈ V
20	7 8 19	fvmpt3i	⊢ ( 𝐵 ∈ V → ( TopOn ‘ 𝐵 ) = { 𝑗 ∈ Top ∣ 𝐵 = ∪ 𝑗 } )
21	20	eleq2d	⊢ ( 𝐵 ∈ V → ( 𝐽 ∈ ( TopOn ‘ 𝐵 ) ↔ 𝐽 ∈ { 𝑗 ∈ Top ∣ 𝐵 = ∪ 𝑗 } ) )
22		unieq	⊢ ( 𝑗 = 𝐽 → ∪ 𝑗 = ∪ 𝐽 )
23	22	eqeq2d	⊢ ( 𝑗 = 𝐽 → ( 𝐵 = ∪ 𝑗 ↔ 𝐵 = ∪ 𝐽 ) )
24	23	elrab	⊢ ( 𝐽 ∈ { 𝑗 ∈ Top ∣ 𝐵 = ∪ 𝑗 } ↔ ( 𝐽 ∈ Top ∧ 𝐵 = ∪ 𝐽 ) )
25	21 24	bitrdi	⊢ ( 𝐵 ∈ V → ( 𝐽 ∈ ( TopOn ‘ 𝐵 ) ↔ ( 𝐽 ∈ Top ∧ 𝐵 = ∪ 𝐽 ) ) )
26	1 5 25	pm5.21nii	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝐵 ) ↔ ( 𝐽 ∈ Top ∧ 𝐵 = ∪ 𝐽 ) )