Metamath Proof Explorer


Theorem elmopn

Description: The defining property of an open set of a metric space. (Contributed by NM, 1-Sep-2006) (Revised by Mario Carneiro, 12-Nov-2013)

Ref Expression
Hypothesis mopnval.1 ⊒ 𝐽 = ( MetOpen β€˜ 𝐷 )
Assertion elmopn ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) β†’ ( 𝐴 ∈ 𝐽 ↔ ( 𝐴 βŠ† 𝑋 ∧ βˆ€ π‘₯ ∈ 𝐴 βˆƒ 𝑦 ∈ ran ( ball β€˜ 𝐷 ) ( π‘₯ ∈ 𝑦 ∧ 𝑦 βŠ† 𝐴 ) ) ) )

Proof

Step Hyp Ref Expression
1 mopnval.1 ⊒ 𝐽 = ( MetOpen β€˜ 𝐷 )
2 1 mopnval ⊒ ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) β†’ 𝐽 = ( topGen β€˜ ran ( ball β€˜ 𝐷 ) ) )
3 2 eleq2d ⊒ ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) β†’ ( 𝐴 ∈ 𝐽 ↔ 𝐴 ∈ ( topGen β€˜ ran ( ball β€˜ 𝐷 ) ) ) )
4 blbas ⊒ ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) β†’ ran ( ball β€˜ 𝐷 ) ∈ TopBases )
5 eltg2 ⊒ ( ran ( ball β€˜ 𝐷 ) ∈ TopBases β†’ ( 𝐴 ∈ ( topGen β€˜ ran ( ball β€˜ 𝐷 ) ) ↔ ( 𝐴 βŠ† βˆͺ ran ( ball β€˜ 𝐷 ) ∧ βˆ€ π‘₯ ∈ 𝐴 βˆƒ 𝑦 ∈ ran ( ball β€˜ 𝐷 ) ( π‘₯ ∈ 𝑦 ∧ 𝑦 βŠ† 𝐴 ) ) ) )
6 4 5 syl ⊒ ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) β†’ ( 𝐴 ∈ ( topGen β€˜ ran ( ball β€˜ 𝐷 ) ) ↔ ( 𝐴 βŠ† βˆͺ ran ( ball β€˜ 𝐷 ) ∧ βˆ€ π‘₯ ∈ 𝐴 βˆƒ 𝑦 ∈ ran ( ball β€˜ 𝐷 ) ( π‘₯ ∈ 𝑦 ∧ 𝑦 βŠ† 𝐴 ) ) ) )
7 unirnbl ⊒ ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) β†’ βˆͺ ran ( ball β€˜ 𝐷 ) = 𝑋 )
8 7 sseq2d ⊒ ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) β†’ ( 𝐴 βŠ† βˆͺ ran ( ball β€˜ 𝐷 ) ↔ 𝐴 βŠ† 𝑋 ) )
9 8 anbi1d ⊒ ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) β†’ ( ( 𝐴 βŠ† βˆͺ ran ( ball β€˜ 𝐷 ) ∧ βˆ€ π‘₯ ∈ 𝐴 βˆƒ 𝑦 ∈ ran ( ball β€˜ 𝐷 ) ( π‘₯ ∈ 𝑦 ∧ 𝑦 βŠ† 𝐴 ) ) ↔ ( 𝐴 βŠ† 𝑋 ∧ βˆ€ π‘₯ ∈ 𝐴 βˆƒ 𝑦 ∈ ran ( ball β€˜ 𝐷 ) ( π‘₯ ∈ 𝑦 ∧ 𝑦 βŠ† 𝐴 ) ) ) )
10 3 6 9 3bitrd ⊒ ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) β†’ ( 𝐴 ∈ 𝐽 ↔ ( 𝐴 βŠ† 𝑋 ∧ βˆ€ π‘₯ ∈ 𝐴 βˆƒ 𝑦 ∈ ran ( ball β€˜ 𝐷 ) ( π‘₯ ∈ 𝑦 ∧ 𝑦 βŠ† 𝐴 ) ) ) )