Theorem is2ndc

Description: The property of being second-countable. (Contributed by Jeff Hankins, 17-Jan-2010) (Revised by Mario Carneiro, 21-Mar-2015)

	Ref	Expression
Assertion	is2ndc	⊢ ( 𝐽 ∈ 2ndω ↔ ∃ 𝑥 ∈ TopBases ( 𝑥 ≼ ω ∧ ( topGen ‘ 𝑥 ) = 𝐽 ) )

Proof

Step	Hyp	Ref	Expression
1		df-2ndc	⊢ 2ndω = { 𝑗 ∣ ∃ 𝑥 ∈ TopBases ( 𝑥 ≼ ω ∧ ( topGen ‘ 𝑥 ) = 𝑗 ) }
2	1	eleq2i	⊢ ( 𝐽 ∈ 2ndω ↔ 𝐽 ∈ { 𝑗 ∣ ∃ 𝑥 ∈ TopBases ( 𝑥 ≼ ω ∧ ( topGen ‘ 𝑥 ) = 𝑗 ) } )
3		simpr	⊢ ( ( 𝑥 ≼ ω ∧ ( topGen ‘ 𝑥 ) = 𝐽 ) → ( topGen ‘ 𝑥 ) = 𝐽 )
4		fvex	⊢ ( topGen ‘ 𝑥 ) ∈ V
5	3 4	eqeltrrdi	⊢ ( ( 𝑥 ≼ ω ∧ ( topGen ‘ 𝑥 ) = 𝐽 ) → 𝐽 ∈ V )
6	5	rexlimivw	⊢ ( ∃ 𝑥 ∈ TopBases ( 𝑥 ≼ ω ∧ ( topGen ‘ 𝑥 ) = 𝐽 ) → 𝐽 ∈ V )
7		eqeq2	⊢ ( 𝑗 = 𝐽 → ( ( topGen ‘ 𝑥 ) = 𝑗 ↔ ( topGen ‘ 𝑥 ) = 𝐽 ) )
8	7	anbi2d	⊢ ( 𝑗 = 𝐽 → ( ( 𝑥 ≼ ω ∧ ( topGen ‘ 𝑥 ) = 𝑗 ) ↔ ( 𝑥 ≼ ω ∧ ( topGen ‘ 𝑥 ) = 𝐽 ) ) )
9	8	rexbidv	⊢ ( 𝑗 = 𝐽 → ( ∃ 𝑥 ∈ TopBases ( 𝑥 ≼ ω ∧ ( topGen ‘ 𝑥 ) = 𝑗 ) ↔ ∃ 𝑥 ∈ TopBases ( 𝑥 ≼ ω ∧ ( topGen ‘ 𝑥 ) = 𝐽 ) ) )
10	6 9	elab3	⊢ ( 𝐽 ∈ { 𝑗 ∣ ∃ 𝑥 ∈ TopBases ( 𝑥 ≼ ω ∧ ( topGen ‘ 𝑥 ) = 𝑗 ) } ↔ ∃ 𝑥 ∈ TopBases ( 𝑥 ≼ ω ∧ ( topGen ‘ 𝑥 ) = 𝐽 ) )
11	2 10	bitri	⊢ ( 𝐽 ∈ 2ndω ↔ ∃ 𝑥 ∈ TopBases ( 𝑥 ≼ ω ∧ ( topGen ‘ 𝑥 ) = 𝐽 ) )