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

Metamath Proof Explorer

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 ‘ 𝑥 ) = 𝐽 ) )