Metamath Proof Explorer

Theorem metrest

Description: Two alternate formulations of a subspace topology of a metric space topology. (Contributed by Jeff Hankins, 19-Aug-2009) (Proof shortened by Mario Carneiro, 5-Jan-2014)

Ref Expression
Hypotheses metrest.1 ⊒ 𝐷 = ( 𝐢 β†Ύ ( π‘Œ Γ— π‘Œ ) )
metrest.3 ⊒ 𝐽 = ( MetOpen β€˜ 𝐢 )
metrest.4 ⊒ 𝐾 = ( MetOpen β€˜ 𝐷 )
Assertion metrest ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ π‘Œ βŠ† 𝑋 ) β†’ ( 𝐽 β†Ύt π‘Œ ) = 𝐾 )

Proof

Step Hyp Ref Expression
1 metrest.1 ⊒ 𝐷 = ( 𝐢 β†Ύ ( π‘Œ Γ— π‘Œ ) )
2 metrest.3 ⊒ 𝐽 = ( MetOpen β€˜ 𝐢 )
3 metrest.4 ⊒ 𝐾 = ( MetOpen β€˜ 𝐷 )
4 inss1 ⊒ ( 𝑒 ∩ π‘Œ ) βŠ† 𝑒
5 2 elmopn2 ⊒ ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) β†’ ( 𝑒 ∈ 𝐽 ↔ ( 𝑒 βŠ† 𝑋 ∧ βˆ€ 𝑦 ∈ 𝑒 βˆƒ π‘Ÿ ∈ ℝ+ ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) βŠ† 𝑒 ) ) )
6 5 simplbda ⊒ ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑒 ∈ 𝐽 ) β†’ βˆ€ 𝑦 ∈ 𝑒 βˆƒ π‘Ÿ ∈ ℝ+ ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) βŠ† 𝑒 )
7 6 adantlr ⊒ ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ π‘Œ βŠ† 𝑋 ) ∧ 𝑒 ∈ 𝐽 ) β†’ βˆ€ 𝑦 ∈ 𝑒 βˆƒ π‘Ÿ ∈ ℝ+ ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) βŠ† 𝑒 )
8 ssralv ⊒ ( ( 𝑒 ∩ π‘Œ ) βŠ† 𝑒 β†’ ( βˆ€ 𝑦 ∈ 𝑒 βˆƒ π‘Ÿ ∈ ℝ+ ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) βŠ† 𝑒 β†’ βˆ€ 𝑦 ∈ ( 𝑒 ∩ π‘Œ ) βˆƒ π‘Ÿ ∈ ℝ+ ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) βŠ† 𝑒 ) )
9 4 7 8 mpsyl ⊒ ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ π‘Œ βŠ† 𝑋 ) ∧ 𝑒 ∈ 𝐽 ) β†’ βˆ€ 𝑦 ∈ ( 𝑒 ∩ π‘Œ ) βˆƒ π‘Ÿ ∈ ℝ+ ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) βŠ† 𝑒 )
10 ssrin ⊒ ( ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) βŠ† 𝑒 β†’ ( ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† ( 𝑒 ∩ π‘Œ ) )
11 10 reximi ⊒ ( βˆƒ π‘Ÿ ∈ ℝ+ ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) βŠ† 𝑒 β†’ βˆƒ π‘Ÿ ∈ ℝ+ ( ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† ( 𝑒 ∩ π‘Œ ) )
12 11 ralimi ⊒ ( βˆ€ 𝑦 ∈ ( 𝑒 ∩ π‘Œ ) βˆƒ π‘Ÿ ∈ ℝ+ ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) βŠ† 𝑒 β†’ βˆ€ 𝑦 ∈ ( 𝑒 ∩ π‘Œ ) βˆƒ π‘Ÿ ∈ ℝ+ ( ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† ( 𝑒 ∩ π‘Œ ) )
13 9 12 syl ⊒ ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ π‘Œ βŠ† 𝑋 ) ∧ 𝑒 ∈ 𝐽 ) β†’ βˆ€ 𝑦 ∈ ( 𝑒 ∩ π‘Œ ) βˆƒ π‘Ÿ ∈ ℝ+ ( ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† ( 𝑒 ∩ π‘Œ ) )
14 inss2 ⊒ ( 𝑒 ∩ π‘Œ ) βŠ† π‘Œ
15 13 14 jctil ⊒ ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ π‘Œ βŠ† 𝑋 ) ∧ 𝑒 ∈ 𝐽 ) β†’ ( ( 𝑒 ∩ π‘Œ ) βŠ† π‘Œ ∧ βˆ€ 𝑦 ∈ ( 𝑒 ∩ π‘Œ ) βˆƒ π‘Ÿ ∈ ℝ+ ( ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† ( 𝑒 ∩ π‘Œ ) ) )
16 sseq1 ⊒ ( π‘₯ = ( 𝑒 ∩ π‘Œ ) β†’ ( π‘₯ βŠ† π‘Œ ↔ ( 𝑒 ∩ π‘Œ ) βŠ† π‘Œ ) )
17 sseq2 ⊒ ( π‘₯ = ( 𝑒 ∩ π‘Œ ) β†’ ( ( ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ ↔ ( ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† ( 𝑒 ∩ π‘Œ ) ) )
18 17 rexbidv ⊒ ( π‘₯ = ( 𝑒 ∩ π‘Œ ) β†’ ( βˆƒ π‘Ÿ ∈ ℝ+ ( ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ ↔ βˆƒ π‘Ÿ ∈ ℝ+ ( ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† ( 𝑒 ∩ π‘Œ ) ) )
19 18 raleqbi1dv ⊒ ( π‘₯ = ( 𝑒 ∩ π‘Œ ) β†’ ( βˆ€ 𝑦 ∈ π‘₯ βˆƒ π‘Ÿ ∈ ℝ+ ( ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ ↔ βˆ€ 𝑦 ∈ ( 𝑒 ∩ π‘Œ ) βˆƒ π‘Ÿ ∈ ℝ+ ( ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† ( 𝑒 ∩ π‘Œ ) ) )
20 16 19 anbi12d ⊒ ( π‘₯ = ( 𝑒 ∩ π‘Œ ) β†’ ( ( π‘₯ βŠ† π‘Œ ∧ βˆ€ 𝑦 ∈ π‘₯ βˆƒ π‘Ÿ ∈ ℝ+ ( ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ ) ↔ ( ( 𝑒 ∩ π‘Œ ) βŠ† π‘Œ ∧ βˆ€ 𝑦 ∈ ( 𝑒 ∩ π‘Œ ) βˆƒ π‘Ÿ ∈ ℝ+ ( ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† ( 𝑒 ∩ π‘Œ ) ) ) )
21 15 20 syl5ibrcom ⊒ ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ π‘Œ βŠ† 𝑋 ) ∧ 𝑒 ∈ 𝐽 ) β†’ ( π‘₯ = ( 𝑒 ∩ π‘Œ ) β†’ ( π‘₯ βŠ† π‘Œ ∧ βˆ€ 𝑦 ∈ π‘₯ βˆƒ π‘Ÿ ∈ ℝ+ ( ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ ) ) )
22 21 rexlimdva ⊒ ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ π‘Œ βŠ† 𝑋 ) β†’ ( βˆƒ 𝑒 ∈ 𝐽 π‘₯ = ( 𝑒 ∩ π‘Œ ) β†’ ( π‘₯ βŠ† π‘Œ ∧ βˆ€ 𝑦 ∈ π‘₯ βˆƒ π‘Ÿ ∈ ℝ+ ( ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ ) ) )
23 2 mopntop ⊒ ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) β†’ 𝐽 ∈ Top )
24 23 ad2antrr ⊒ ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ π‘Œ βŠ† 𝑋 ) ∧ ( π‘₯ βŠ† π‘Œ ∧ βˆ€ 𝑦 ∈ π‘₯ βˆƒ π‘Ÿ ∈ ℝ+ ( ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ ) ) β†’ 𝐽 ∈ Top )
25 ssel2 ⊒ ( ( π‘₯ βŠ† π‘Œ ∧ 𝑦 ∈ π‘₯ ) β†’ 𝑦 ∈ π‘Œ )
26 ssel2 ⊒ ( ( π‘Œ βŠ† 𝑋 ∧ 𝑦 ∈ π‘Œ ) β†’ 𝑦 ∈ 𝑋 )
27 rpxr ⊒ ( π‘Ÿ ∈ ℝ+ β†’ π‘Ÿ ∈ ℝ* )
28 2 blopn ⊒ ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ π‘Ÿ ∈ ℝ* ) β†’ ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∈ 𝐽 )
29 eleq1a ⊒ ( ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∈ 𝐽 β†’ ( 𝑧 = ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) β†’ 𝑧 ∈ 𝐽 ) )
30 28 29 syl ⊒ ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ π‘Ÿ ∈ ℝ* ) β†’ ( 𝑧 = ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) β†’ 𝑧 ∈ 𝐽 ) )
31 30 3expa ⊒ ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ π‘Ÿ ∈ ℝ* ) β†’ ( 𝑧 = ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) β†’ 𝑧 ∈ 𝐽 ) )
32 27 31 sylan2 ⊒ ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( 𝑧 = ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) β†’ 𝑧 ∈ 𝐽 ) )
33 32 rexlimdva ⊒ ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) β†’ ( βˆƒ π‘Ÿ ∈ ℝ+ 𝑧 = ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) β†’ 𝑧 ∈ 𝐽 ) )
34 26 33 sylan2 ⊒ ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( π‘Œ βŠ† 𝑋 ∧ 𝑦 ∈ π‘Œ ) ) β†’ ( βˆƒ π‘Ÿ ∈ ℝ+ 𝑧 = ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) β†’ 𝑧 ∈ 𝐽 ) )
35 34 anassrs ⊒ ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ π‘Œ βŠ† 𝑋 ) ∧ 𝑦 ∈ π‘Œ ) β†’ ( βˆƒ π‘Ÿ ∈ ℝ+ 𝑧 = ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) β†’ 𝑧 ∈ 𝐽 ) )
36 25 35 sylan2 ⊒ ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ π‘Œ βŠ† 𝑋 ) ∧ ( π‘₯ βŠ† π‘Œ ∧ 𝑦 ∈ π‘₯ ) ) β†’ ( βˆƒ π‘Ÿ ∈ ℝ+ 𝑧 = ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) β†’ 𝑧 ∈ 𝐽 ) )
37 36 anassrs ⊒ ( ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ π‘Œ βŠ† 𝑋 ) ∧ π‘₯ βŠ† π‘Œ ) ∧ 𝑦 ∈ π‘₯ ) β†’ ( βˆƒ π‘Ÿ ∈ ℝ+ 𝑧 = ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) β†’ 𝑧 ∈ 𝐽 ) )
38 37 rexlimdva ⊒ ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ π‘Œ βŠ† 𝑋 ) ∧ π‘₯ βŠ† π‘Œ ) β†’ ( βˆƒ 𝑦 ∈ π‘₯ βˆƒ π‘Ÿ ∈ ℝ+ 𝑧 = ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) β†’ 𝑧 ∈ 𝐽 ) )
39 38 adantrd ⊒ ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ π‘Œ βŠ† 𝑋 ) ∧ π‘₯ βŠ† π‘Œ ) β†’ ( ( βˆƒ 𝑦 ∈ π‘₯ βˆƒ π‘Ÿ ∈ ℝ+ 𝑧 = ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∧ ( 𝑧 ∩ π‘Œ ) βŠ† π‘₯ ) β†’ 𝑧 ∈ 𝐽 ) )
40 39 adantrr ⊒ ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ π‘Œ βŠ† 𝑋 ) ∧ ( π‘₯ βŠ† π‘Œ ∧ βˆ€ 𝑦 ∈ π‘₯ βˆƒ π‘Ÿ ∈ ℝ+ ( ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ ) ) β†’ ( ( βˆƒ 𝑦 ∈ π‘₯ βˆƒ π‘Ÿ ∈ ℝ+ 𝑧 = ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∧ ( 𝑧 ∩ π‘Œ ) βŠ† π‘₯ ) β†’ 𝑧 ∈ 𝐽 ) )
41 40 abssdv ⊒ ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ π‘Œ βŠ† 𝑋 ) ∧ ( π‘₯ βŠ† π‘Œ ∧ βˆ€ 𝑦 ∈ π‘₯ βˆƒ π‘Ÿ ∈ ℝ+ ( ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ ) ) β†’ { 𝑧 ∣ ( βˆƒ 𝑦 ∈ π‘₯ βˆƒ π‘Ÿ ∈ ℝ+ 𝑧 = ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∧ ( 𝑧 ∩ π‘Œ ) βŠ† π‘₯ ) } βŠ† 𝐽 )
42 uniopn ⊒ ( ( 𝐽 ∈ Top ∧ { 𝑧 ∣ ( βˆƒ 𝑦 ∈ π‘₯ βˆƒ π‘Ÿ ∈ ℝ+ 𝑧 = ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∧ ( 𝑧 ∩ π‘Œ ) βŠ† π‘₯ ) } βŠ† 𝐽 ) β†’ βˆͺ { 𝑧 ∣ ( βˆƒ 𝑦 ∈ π‘₯ βˆƒ π‘Ÿ ∈ ℝ+ 𝑧 = ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∧ ( 𝑧 ∩ π‘Œ ) βŠ† π‘₯ ) } ∈ 𝐽 )
43 24 41 42 syl2anc ⊒ ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ π‘Œ βŠ† 𝑋 ) ∧ ( π‘₯ βŠ† π‘Œ ∧ βˆ€ 𝑦 ∈ π‘₯ βˆƒ π‘Ÿ ∈ ℝ+ ( ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ ) ) β†’ βˆͺ { 𝑧 ∣ ( βˆƒ 𝑦 ∈ π‘₯ βˆƒ π‘Ÿ ∈ ℝ+ 𝑧 = ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∧ ( 𝑧 ∩ π‘Œ ) βŠ† π‘₯ ) } ∈ 𝐽 )
44 oveq1 ⊒ ( 𝑦 = 𝑒 β†’ ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) = ( 𝑒 ( ball β€˜ 𝐢 ) π‘Ÿ ) )
45 44 ineq1d ⊒ ( 𝑦 = 𝑒 β†’ ( ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) = ( ( 𝑒 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) )
46 45 sseq1d ⊒ ( 𝑦 = 𝑒 β†’ ( ( ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ ↔ ( ( 𝑒 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ ) )
47 46 rexbidv ⊒ ( 𝑦 = 𝑒 β†’ ( βˆƒ π‘Ÿ ∈ ℝ+ ( ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ ↔ βˆƒ π‘Ÿ ∈ ℝ+ ( ( 𝑒 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ ) )
48 47 rspccv ⊒ ( βˆ€ 𝑦 ∈ π‘₯ βˆƒ π‘Ÿ ∈ ℝ+ ( ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ β†’ ( 𝑒 ∈ π‘₯ β†’ βˆƒ π‘Ÿ ∈ ℝ+ ( ( 𝑒 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ ) )
49 48 ad2antll ⊒ ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ π‘Œ βŠ† 𝑋 ) ∧ ( π‘₯ βŠ† π‘Œ ∧ βˆ€ 𝑦 ∈ π‘₯ βˆƒ π‘Ÿ ∈ ℝ+ ( ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ ) ) β†’ ( 𝑒 ∈ π‘₯ β†’ βˆƒ π‘Ÿ ∈ ℝ+ ( ( 𝑒 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ ) )
50 ssel ⊒ ( π‘₯ βŠ† π‘Œ β†’ ( 𝑒 ∈ π‘₯ β†’ 𝑒 ∈ π‘Œ ) )
51 ssel ⊒ ( π‘Œ βŠ† 𝑋 β†’ ( 𝑒 ∈ π‘Œ β†’ 𝑒 ∈ 𝑋 ) )
52 blcntr ⊒ ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑒 ∈ 𝑋 ∧ π‘Ÿ ∈ ℝ+ ) β†’ 𝑒 ∈ ( 𝑒 ( ball β€˜ 𝐢 ) π‘Ÿ ) )
53 52 a1d ⊒ ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑒 ∈ 𝑋 ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( ( ( 𝑒 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ β†’ 𝑒 ∈ ( 𝑒 ( ball β€˜ 𝐢 ) π‘Ÿ ) ) )
54 53 ancld ⊒ ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑒 ∈ 𝑋 ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( ( ( 𝑒 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ β†’ ( ( ( 𝑒 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ ∧ 𝑒 ∈ ( 𝑒 ( ball β€˜ 𝐢 ) π‘Ÿ ) ) ) )
55 54 3expa ⊒ ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑒 ∈ 𝑋 ) ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( ( ( 𝑒 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ β†’ ( ( ( 𝑒 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ ∧ 𝑒 ∈ ( 𝑒 ( ball β€˜ 𝐢 ) π‘Ÿ ) ) ) )
56 55 reximdva ⊒ ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑒 ∈ 𝑋 ) β†’ ( βˆƒ π‘Ÿ ∈ ℝ+ ( ( 𝑒 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ β†’ βˆƒ π‘Ÿ ∈ ℝ+ ( ( ( 𝑒 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ ∧ 𝑒 ∈ ( 𝑒 ( ball β€˜ 𝐢 ) π‘Ÿ ) ) ) )
57 56 ex ⊒ ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) β†’ ( 𝑒 ∈ 𝑋 β†’ ( βˆƒ π‘Ÿ ∈ ℝ+ ( ( 𝑒 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ β†’ βˆƒ π‘Ÿ ∈ ℝ+ ( ( ( 𝑒 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ ∧ 𝑒 ∈ ( 𝑒 ( ball β€˜ 𝐢 ) π‘Ÿ ) ) ) ) )
58 51 57 sylan9r ⊒ ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ π‘Œ βŠ† 𝑋 ) β†’ ( 𝑒 ∈ π‘Œ β†’ ( βˆƒ π‘Ÿ ∈ ℝ+ ( ( 𝑒 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ β†’ βˆƒ π‘Ÿ ∈ ℝ+ ( ( ( 𝑒 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ ∧ 𝑒 ∈ ( 𝑒 ( ball β€˜ 𝐢 ) π‘Ÿ ) ) ) ) )
59 50 58 sylan9r ⊒ ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ π‘Œ βŠ† 𝑋 ) ∧ π‘₯ βŠ† π‘Œ ) β†’ ( 𝑒 ∈ π‘₯ β†’ ( βˆƒ π‘Ÿ ∈ ℝ+ ( ( 𝑒 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ β†’ βˆƒ π‘Ÿ ∈ ℝ+ ( ( ( 𝑒 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ ∧ 𝑒 ∈ ( 𝑒 ( ball β€˜ 𝐢 ) π‘Ÿ ) ) ) ) )
60 59 adantrr ⊒ ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ π‘Œ βŠ† 𝑋 ) ∧ ( π‘₯ βŠ† π‘Œ ∧ βˆ€ 𝑦 ∈ π‘₯ βˆƒ π‘Ÿ ∈ ℝ+ ( ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ ) ) β†’ ( 𝑒 ∈ π‘₯ β†’ ( βˆƒ π‘Ÿ ∈ ℝ+ ( ( 𝑒 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ β†’ βˆƒ π‘Ÿ ∈ ℝ+ ( ( ( 𝑒 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ ∧ 𝑒 ∈ ( 𝑒 ( ball β€˜ 𝐢 ) π‘Ÿ ) ) ) ) )
61 49 60 mpdd ⊒ ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ π‘Œ βŠ† 𝑋 ) ∧ ( π‘₯ βŠ† π‘Œ ∧ βˆ€ 𝑦 ∈ π‘₯ βˆƒ π‘Ÿ ∈ ℝ+ ( ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ ) ) β†’ ( 𝑒 ∈ π‘₯ β†’ βˆƒ π‘Ÿ ∈ ℝ+ ( ( ( 𝑒 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ ∧ 𝑒 ∈ ( 𝑒 ( ball β€˜ 𝐢 ) π‘Ÿ ) ) ) )
62 44 eleq2d ⊒ ( 𝑦 = 𝑒 β†’ ( 𝑒 ∈ ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ↔ 𝑒 ∈ ( 𝑒 ( ball β€˜ 𝐢 ) π‘Ÿ ) ) )
63 46 62 anbi12d ⊒ ( 𝑦 = 𝑒 β†’ ( ( ( ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ ∧ 𝑒 ∈ ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ) ↔ ( ( ( 𝑒 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ ∧ 𝑒 ∈ ( 𝑒 ( ball β€˜ 𝐢 ) π‘Ÿ ) ) ) )
64 63 rexbidv ⊒ ( 𝑦 = 𝑒 β†’ ( βˆƒ π‘Ÿ ∈ ℝ+ ( ( ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ ∧ 𝑒 ∈ ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ) ↔ βˆƒ π‘Ÿ ∈ ℝ+ ( ( ( 𝑒 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ ∧ 𝑒 ∈ ( 𝑒 ( ball β€˜ 𝐢 ) π‘Ÿ ) ) ) )
65 64 rspcev ⊒ ( ( 𝑒 ∈ π‘₯ ∧ βˆƒ π‘Ÿ ∈ ℝ+ ( ( ( 𝑒 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ ∧ 𝑒 ∈ ( 𝑒 ( ball β€˜ 𝐢 ) π‘Ÿ ) ) ) β†’ βˆƒ 𝑦 ∈ π‘₯ βˆƒ π‘Ÿ ∈ ℝ+ ( ( ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ ∧ 𝑒 ∈ ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ) )
66 65 ex ⊒ ( 𝑒 ∈ π‘₯ β†’ ( βˆƒ π‘Ÿ ∈ ℝ+ ( ( ( 𝑒 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ ∧ 𝑒 ∈ ( 𝑒 ( ball β€˜ 𝐢 ) π‘Ÿ ) ) β†’ βˆƒ 𝑦 ∈ π‘₯ βˆƒ π‘Ÿ ∈ ℝ+ ( ( ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ ∧ 𝑒 ∈ ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ) ) )
67 61 66 sylcom ⊒ ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ π‘Œ βŠ† 𝑋 ) ∧ ( π‘₯ βŠ† π‘Œ ∧ βˆ€ 𝑦 ∈ π‘₯ βˆƒ π‘Ÿ ∈ ℝ+ ( ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ ) ) β†’ ( 𝑒 ∈ π‘₯ β†’ βˆƒ 𝑦 ∈ π‘₯ βˆƒ π‘Ÿ ∈ ℝ+ ( ( ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ ∧ 𝑒 ∈ ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ) ) )
68 simprl ⊒ ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ π‘Œ βŠ† 𝑋 ) ∧ ( π‘₯ βŠ† π‘Œ ∧ βˆ€ 𝑦 ∈ π‘₯ βˆƒ π‘Ÿ ∈ ℝ+ ( ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ ) ) β†’ π‘₯ βŠ† π‘Œ )
69 68 sseld ⊒ ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ π‘Œ βŠ† 𝑋 ) ∧ ( π‘₯ βŠ† π‘Œ ∧ βˆ€ 𝑦 ∈ π‘₯ βˆƒ π‘Ÿ ∈ ℝ+ ( ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ ) ) β†’ ( 𝑒 ∈ π‘₯ β†’ 𝑒 ∈ π‘Œ ) )
70 67 69 jcad ⊒ ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ π‘Œ βŠ† 𝑋 ) ∧ ( π‘₯ βŠ† π‘Œ ∧ βˆ€ 𝑦 ∈ π‘₯ βˆƒ π‘Ÿ ∈ ℝ+ ( ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ ) ) β†’ ( 𝑒 ∈ π‘₯ β†’ ( βˆƒ 𝑦 ∈ π‘₯ βˆƒ π‘Ÿ ∈ ℝ+ ( ( ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ ∧ 𝑒 ∈ ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ) ∧ 𝑒 ∈ π‘Œ ) ) )
71 elin ⊒ ( 𝑒 ∈ ( ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) ↔ ( 𝑒 ∈ ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∧ 𝑒 ∈ π‘Œ ) )
72 ssel2 ⊒ ( ( ( ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ ∧ 𝑒 ∈ ( ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) ) β†’ 𝑒 ∈ π‘₯ )
73 71 72 sylan2br ⊒ ( ( ( ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ ∧ ( 𝑒 ∈ ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∧ 𝑒 ∈ π‘Œ ) ) β†’ 𝑒 ∈ π‘₯ )
74 73 expr ⊒ ( ( ( ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ ∧ 𝑒 ∈ ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ) β†’ ( 𝑒 ∈ π‘Œ β†’ 𝑒 ∈ π‘₯ ) )
75 74 rexlimivw ⊒ ( βˆƒ π‘Ÿ ∈ ℝ+ ( ( ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ ∧ 𝑒 ∈ ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ) β†’ ( 𝑒 ∈ π‘Œ β†’ 𝑒 ∈ π‘₯ ) )
76 75 rexlimivw ⊒ ( βˆƒ 𝑦 ∈ π‘₯ βˆƒ π‘Ÿ ∈ ℝ+ ( ( ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ ∧ 𝑒 ∈ ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ) β†’ ( 𝑒 ∈ π‘Œ β†’ 𝑒 ∈ π‘₯ ) )
77 76 imp ⊒ ( ( βˆƒ 𝑦 ∈ π‘₯ βˆƒ π‘Ÿ ∈ ℝ+ ( ( ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ ∧ 𝑒 ∈ ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ) ∧ 𝑒 ∈ π‘Œ ) β†’ 𝑒 ∈ π‘₯ )
78 70 77 impbid1 ⊒ ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ π‘Œ βŠ† 𝑋 ) ∧ ( π‘₯ βŠ† π‘Œ ∧ βˆ€ 𝑦 ∈ π‘₯ βˆƒ π‘Ÿ ∈ ℝ+ ( ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ ) ) β†’ ( 𝑒 ∈ π‘₯ ↔ ( βˆƒ 𝑦 ∈ π‘₯ βˆƒ π‘Ÿ ∈ ℝ+ ( ( ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ ∧ 𝑒 ∈ ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ) ∧ 𝑒 ∈ π‘Œ ) ) )
79 elin ⊒ ( 𝑒 ∈ ( βˆͺ { 𝑧 ∣ ( βˆƒ 𝑦 ∈ π‘₯ βˆƒ π‘Ÿ ∈ ℝ+ 𝑧 = ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∧ ( 𝑧 ∩ π‘Œ ) βŠ† π‘₯ ) } ∩ π‘Œ ) ↔ ( 𝑒 ∈ βˆͺ { 𝑧 ∣ ( βˆƒ 𝑦 ∈ π‘₯ βˆƒ π‘Ÿ ∈ ℝ+ 𝑧 = ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∧ ( 𝑧 ∩ π‘Œ ) βŠ† π‘₯ ) } ∧ 𝑒 ∈ π‘Œ ) )
80 eluniab ⊒ ( 𝑒 ∈ βˆͺ { 𝑧 ∣ ( βˆƒ 𝑦 ∈ π‘₯ βˆƒ π‘Ÿ ∈ ℝ+ 𝑧 = ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∧ ( 𝑧 ∩ π‘Œ ) βŠ† π‘₯ ) } ↔ βˆƒ 𝑧 ( 𝑒 ∈ 𝑧 ∧ ( βˆƒ 𝑦 ∈ π‘₯ βˆƒ π‘Ÿ ∈ ℝ+ 𝑧 = ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∧ ( 𝑧 ∩ π‘Œ ) βŠ† π‘₯ ) ) )
81 ancom ⊒ ( ( 𝑒 ∈ 𝑧 ∧ ( βˆƒ 𝑦 ∈ π‘₯ βˆƒ π‘Ÿ ∈ ℝ+ 𝑧 = ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∧ ( 𝑧 ∩ π‘Œ ) βŠ† π‘₯ ) ) ↔ ( ( βˆƒ 𝑦 ∈ π‘₯ βˆƒ π‘Ÿ ∈ ℝ+ 𝑧 = ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∧ ( 𝑧 ∩ π‘Œ ) βŠ† π‘₯ ) ∧ 𝑒 ∈ 𝑧 ) )
82 anass ⊒ ( ( ( βˆƒ 𝑦 ∈ π‘₯ βˆƒ π‘Ÿ ∈ ℝ+ 𝑧 = ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∧ ( 𝑧 ∩ π‘Œ ) βŠ† π‘₯ ) ∧ 𝑒 ∈ 𝑧 ) ↔ ( βˆƒ 𝑦 ∈ π‘₯ βˆƒ π‘Ÿ ∈ ℝ+ 𝑧 = ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∧ ( ( 𝑧 ∩ π‘Œ ) βŠ† π‘₯ ∧ 𝑒 ∈ 𝑧 ) ) )
83 r19.41v ⊒ ( βˆƒ π‘Ÿ ∈ ℝ+ ( 𝑧 = ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∧ ( ( 𝑧 ∩ π‘Œ ) βŠ† π‘₯ ∧ 𝑒 ∈ 𝑧 ) ) ↔ ( βˆƒ π‘Ÿ ∈ ℝ+ 𝑧 = ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∧ ( ( 𝑧 ∩ π‘Œ ) βŠ† π‘₯ ∧ 𝑒 ∈ 𝑧 ) ) )
84 83 rexbii ⊒ ( βˆƒ 𝑦 ∈ π‘₯ βˆƒ π‘Ÿ ∈ ℝ+ ( 𝑧 = ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∧ ( ( 𝑧 ∩ π‘Œ ) βŠ† π‘₯ ∧ 𝑒 ∈ 𝑧 ) ) ↔ βˆƒ 𝑦 ∈ π‘₯ ( βˆƒ π‘Ÿ ∈ ℝ+ 𝑧 = ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∧ ( ( 𝑧 ∩ π‘Œ ) βŠ† π‘₯ ∧ 𝑒 ∈ 𝑧 ) ) )
85 r19.41v ⊒ ( βˆƒ 𝑦 ∈ π‘₯ ( βˆƒ π‘Ÿ ∈ ℝ+ 𝑧 = ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∧ ( ( 𝑧 ∩ π‘Œ ) βŠ† π‘₯ ∧ 𝑒 ∈ 𝑧 ) ) ↔ ( βˆƒ 𝑦 ∈ π‘₯ βˆƒ π‘Ÿ ∈ ℝ+ 𝑧 = ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∧ ( ( 𝑧 ∩ π‘Œ ) βŠ† π‘₯ ∧ 𝑒 ∈ 𝑧 ) ) )
86 84 85 bitr2i ⊒ ( ( βˆƒ 𝑦 ∈ π‘₯ βˆƒ π‘Ÿ ∈ ℝ+ 𝑧 = ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∧ ( ( 𝑧 ∩ π‘Œ ) βŠ† π‘₯ ∧ 𝑒 ∈ 𝑧 ) ) ↔ βˆƒ 𝑦 ∈ π‘₯ βˆƒ π‘Ÿ ∈ ℝ+ ( 𝑧 = ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∧ ( ( 𝑧 ∩ π‘Œ ) βŠ† π‘₯ ∧ 𝑒 ∈ 𝑧 ) ) )
87 81 82 86 3bitri ⊒ ( ( 𝑒 ∈ 𝑧 ∧ ( βˆƒ 𝑦 ∈ π‘₯ βˆƒ π‘Ÿ ∈ ℝ+ 𝑧 = ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∧ ( 𝑧 ∩ π‘Œ ) βŠ† π‘₯ ) ) ↔ βˆƒ 𝑦 ∈ π‘₯ βˆƒ π‘Ÿ ∈ ℝ+ ( 𝑧 = ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∧ ( ( 𝑧 ∩ π‘Œ ) βŠ† π‘₯ ∧ 𝑒 ∈ 𝑧 ) ) )
88 87 exbii ⊒ ( βˆƒ 𝑧 ( 𝑒 ∈ 𝑧 ∧ ( βˆƒ 𝑦 ∈ π‘₯ βˆƒ π‘Ÿ ∈ ℝ+ 𝑧 = ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∧ ( 𝑧 ∩ π‘Œ ) βŠ† π‘₯ ) ) ↔ βˆƒ 𝑧 βˆƒ 𝑦 ∈ π‘₯ βˆƒ π‘Ÿ ∈ ℝ+ ( 𝑧 = ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∧ ( ( 𝑧 ∩ π‘Œ ) βŠ† π‘₯ ∧ 𝑒 ∈ 𝑧 ) ) )
89 ovex ⊒ ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∈ V
90 ineq1 ⊒ ( 𝑧 = ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) β†’ ( 𝑧 ∩ π‘Œ ) = ( ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) )
91 90 sseq1d ⊒ ( 𝑧 = ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) β†’ ( ( 𝑧 ∩ π‘Œ ) βŠ† π‘₯ ↔ ( ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ ) )
92 eleq2 ⊒ ( 𝑧 = ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) β†’ ( 𝑒 ∈ 𝑧 ↔ 𝑒 ∈ ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ) )
93 91 92 anbi12d ⊒ ( 𝑧 = ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) β†’ ( ( ( 𝑧 ∩ π‘Œ ) βŠ† π‘₯ ∧ 𝑒 ∈ 𝑧 ) ↔ ( ( ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ ∧ 𝑒 ∈ ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ) ) )
94 89 93 ceqsexv ⊒ ( βˆƒ 𝑧 ( 𝑧 = ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∧ ( ( 𝑧 ∩ π‘Œ ) βŠ† π‘₯ ∧ 𝑒 ∈ 𝑧 ) ) ↔ ( ( ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ ∧ 𝑒 ∈ ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ) )
95 94 rexbii ⊒ ( βˆƒ π‘Ÿ ∈ ℝ+ βˆƒ 𝑧 ( 𝑧 = ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∧ ( ( 𝑧 ∩ π‘Œ ) βŠ† π‘₯ ∧ 𝑒 ∈ 𝑧 ) ) ↔ βˆƒ π‘Ÿ ∈ ℝ+ ( ( ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ ∧ 𝑒 ∈ ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ) )
96 rexcom4 ⊒ ( βˆƒ π‘Ÿ ∈ ℝ+ βˆƒ 𝑧 ( 𝑧 = ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∧ ( ( 𝑧 ∩ π‘Œ ) βŠ† π‘₯ ∧ 𝑒 ∈ 𝑧 ) ) ↔ βˆƒ 𝑧 βˆƒ π‘Ÿ ∈ ℝ+ ( 𝑧 = ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∧ ( ( 𝑧 ∩ π‘Œ ) βŠ† π‘₯ ∧ 𝑒 ∈ 𝑧 ) ) )
97 95 96 bitr3i ⊒ ( βˆƒ π‘Ÿ ∈ ℝ+ ( ( ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ ∧ 𝑒 ∈ ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ) ↔ βˆƒ 𝑧 βˆƒ π‘Ÿ ∈ ℝ+ ( 𝑧 = ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∧ ( ( 𝑧 ∩ π‘Œ ) βŠ† π‘₯ ∧ 𝑒 ∈ 𝑧 ) ) )
98 97 rexbii ⊒ ( βˆƒ 𝑦 ∈ π‘₯ βˆƒ π‘Ÿ ∈ ℝ+ ( ( ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ ∧ 𝑒 ∈ ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ) ↔ βˆƒ 𝑦 ∈ π‘₯ βˆƒ 𝑧 βˆƒ π‘Ÿ ∈ ℝ+ ( 𝑧 = ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∧ ( ( 𝑧 ∩ π‘Œ ) βŠ† π‘₯ ∧ 𝑒 ∈ 𝑧 ) ) )
99 rexcom4 ⊒ ( βˆƒ 𝑦 ∈ π‘₯ βˆƒ 𝑧 βˆƒ π‘Ÿ ∈ ℝ+ ( 𝑧 = ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∧ ( ( 𝑧 ∩ π‘Œ ) βŠ† π‘₯ ∧ 𝑒 ∈ 𝑧 ) ) ↔ βˆƒ 𝑧 βˆƒ 𝑦 ∈ π‘₯ βˆƒ π‘Ÿ ∈ ℝ+ ( 𝑧 = ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∧ ( ( 𝑧 ∩ π‘Œ ) βŠ† π‘₯ ∧ 𝑒 ∈ 𝑧 ) ) )
100 98 99 bitr2i ⊒ ( βˆƒ 𝑧 βˆƒ 𝑦 ∈ π‘₯ βˆƒ π‘Ÿ ∈ ℝ+ ( 𝑧 = ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∧ ( ( 𝑧 ∩ π‘Œ ) βŠ† π‘₯ ∧ 𝑒 ∈ 𝑧 ) ) ↔ βˆƒ 𝑦 ∈ π‘₯ βˆƒ π‘Ÿ ∈ ℝ+ ( ( ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ ∧ 𝑒 ∈ ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ) )
101 80 88 100 3bitri ⊒ ( 𝑒 ∈ βˆͺ { 𝑧 ∣ ( βˆƒ 𝑦 ∈ π‘₯ βˆƒ π‘Ÿ ∈ ℝ+ 𝑧 = ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∧ ( 𝑧 ∩ π‘Œ ) βŠ† π‘₯ ) } ↔ βˆƒ 𝑦 ∈ π‘₯ βˆƒ π‘Ÿ ∈ ℝ+ ( ( ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ ∧ 𝑒 ∈ ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ) )
102 101 anbi1i ⊒ ( ( 𝑒 ∈ βˆͺ { 𝑧 ∣ ( βˆƒ 𝑦 ∈ π‘₯ βˆƒ π‘Ÿ ∈ ℝ+ 𝑧 = ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∧ ( 𝑧 ∩ π‘Œ ) βŠ† π‘₯ ) } ∧ 𝑒 ∈ π‘Œ ) ↔ ( βˆƒ 𝑦 ∈ π‘₯ βˆƒ π‘Ÿ ∈ ℝ+ ( ( ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ ∧ 𝑒 ∈ ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ) ∧ 𝑒 ∈ π‘Œ ) )
103 79 102 bitr2i ⊒ ( ( βˆƒ 𝑦 ∈ π‘₯ βˆƒ π‘Ÿ ∈ ℝ+ ( ( ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ ∧ 𝑒 ∈ ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ) ∧ 𝑒 ∈ π‘Œ ) ↔ 𝑒 ∈ ( βˆͺ { 𝑧 ∣ ( βˆƒ 𝑦 ∈ π‘₯ βˆƒ π‘Ÿ ∈ ℝ+ 𝑧 = ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∧ ( 𝑧 ∩ π‘Œ ) βŠ† π‘₯ ) } ∩ π‘Œ ) )
104 78 103 bitrdi ⊒ ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ π‘Œ βŠ† 𝑋 ) ∧ ( π‘₯ βŠ† π‘Œ ∧ βˆ€ 𝑦 ∈ π‘₯ βˆƒ π‘Ÿ ∈ ℝ+ ( ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ ) ) β†’ ( 𝑒 ∈ π‘₯ ↔ 𝑒 ∈ ( βˆͺ { 𝑧 ∣ ( βˆƒ 𝑦 ∈ π‘₯ βˆƒ π‘Ÿ ∈ ℝ+ 𝑧 = ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∧ ( 𝑧 ∩ π‘Œ ) βŠ† π‘₯ ) } ∩ π‘Œ ) ) )
105 104 eqrdv ⊒ ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ π‘Œ βŠ† 𝑋 ) ∧ ( π‘₯ βŠ† π‘Œ ∧ βˆ€ 𝑦 ∈ π‘₯ βˆƒ π‘Ÿ ∈ ℝ+ ( ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ ) ) β†’ π‘₯ = ( βˆͺ { 𝑧 ∣ ( βˆƒ 𝑦 ∈ π‘₯ βˆƒ π‘Ÿ ∈ ℝ+ 𝑧 = ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∧ ( 𝑧 ∩ π‘Œ ) βŠ† π‘₯ ) } ∩ π‘Œ ) )
106 ineq1 ⊒ ( 𝑒 = βˆͺ { 𝑧 ∣ ( βˆƒ 𝑦 ∈ π‘₯ βˆƒ π‘Ÿ ∈ ℝ+ 𝑧 = ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∧ ( 𝑧 ∩ π‘Œ ) βŠ† π‘₯ ) } β†’ ( 𝑒 ∩ π‘Œ ) = ( βˆͺ { 𝑧 ∣ ( βˆƒ 𝑦 ∈ π‘₯ βˆƒ π‘Ÿ ∈ ℝ+ 𝑧 = ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∧ ( 𝑧 ∩ π‘Œ ) βŠ† π‘₯ ) } ∩ π‘Œ ) )
107 106 rspceeqv ⊒ ( ( βˆͺ { 𝑧 ∣ ( βˆƒ 𝑦 ∈ π‘₯ βˆƒ π‘Ÿ ∈ ℝ+ 𝑧 = ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∧ ( 𝑧 ∩ π‘Œ ) βŠ† π‘₯ ) } ∈ 𝐽 ∧ π‘₯ = ( βˆͺ { 𝑧 ∣ ( βˆƒ 𝑦 ∈ π‘₯ βˆƒ π‘Ÿ ∈ ℝ+ 𝑧 = ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∧ ( 𝑧 ∩ π‘Œ ) βŠ† π‘₯ ) } ∩ π‘Œ ) ) β†’ βˆƒ 𝑒 ∈ 𝐽 π‘₯ = ( 𝑒 ∩ π‘Œ ) )
108 43 105 107 syl2anc ⊒ ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ π‘Œ βŠ† 𝑋 ) ∧ ( π‘₯ βŠ† π‘Œ ∧ βˆ€ 𝑦 ∈ π‘₯ βˆƒ π‘Ÿ ∈ ℝ+ ( ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ ) ) β†’ βˆƒ 𝑒 ∈ 𝐽 π‘₯ = ( 𝑒 ∩ π‘Œ ) )
109 108 ex ⊒ ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ π‘Œ βŠ† 𝑋 ) β†’ ( ( π‘₯ βŠ† π‘Œ ∧ βˆ€ 𝑦 ∈ π‘₯ βˆƒ π‘Ÿ ∈ ℝ+ ( ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ ) β†’ βˆƒ 𝑒 ∈ 𝐽 π‘₯ = ( 𝑒 ∩ π‘Œ ) ) )
110 22 109 impbid ⊒ ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ π‘Œ βŠ† 𝑋 ) β†’ ( βˆƒ 𝑒 ∈ 𝐽 π‘₯ = ( 𝑒 ∩ π‘Œ ) ↔ ( π‘₯ βŠ† π‘Œ ∧ βˆ€ 𝑦 ∈ π‘₯ βˆƒ π‘Ÿ ∈ ℝ+ ( ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ ) ) )
111 simpr ⊒ ( ( π‘Œ βŠ† 𝑋 ∧ 𝑦 ∈ π‘Œ ) β†’ 𝑦 ∈ π‘Œ )
112 26 111 elind ⊒ ( ( π‘Œ βŠ† 𝑋 ∧ 𝑦 ∈ π‘Œ ) β†’ 𝑦 ∈ ( 𝑋 ∩ π‘Œ ) )
113 1 blres ⊒ ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑦 ∈ ( 𝑋 ∩ π‘Œ ) ∧ π‘Ÿ ∈ ℝ* ) β†’ ( 𝑦 ( ball β€˜ 𝐷 ) π‘Ÿ ) = ( ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) )
114 113 sseq1d ⊒ ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑦 ∈ ( 𝑋 ∩ π‘Œ ) ∧ π‘Ÿ ∈ ℝ* ) β†’ ( ( 𝑦 ( ball β€˜ 𝐷 ) π‘Ÿ ) βŠ† π‘₯ ↔ ( ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ ) )
115 114 3expa ⊒ ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑦 ∈ ( 𝑋 ∩ π‘Œ ) ) ∧ π‘Ÿ ∈ ℝ* ) β†’ ( ( 𝑦 ( ball β€˜ 𝐷 ) π‘Ÿ ) βŠ† π‘₯ ↔ ( ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ ) )
116 27 115 sylan2 ⊒ ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑦 ∈ ( 𝑋 ∩ π‘Œ ) ) ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( ( 𝑦 ( ball β€˜ 𝐷 ) π‘Ÿ ) βŠ† π‘₯ ↔ ( ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ ) )
117 116 rexbidva ⊒ ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑦 ∈ ( 𝑋 ∩ π‘Œ ) ) β†’ ( βˆƒ π‘Ÿ ∈ ℝ+ ( 𝑦 ( ball β€˜ 𝐷 ) π‘Ÿ ) βŠ† π‘₯ ↔ βˆƒ π‘Ÿ ∈ ℝ+ ( ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ ) )
118 112 117 sylan2 ⊒ ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( π‘Œ βŠ† 𝑋 ∧ 𝑦 ∈ π‘Œ ) ) β†’ ( βˆƒ π‘Ÿ ∈ ℝ+ ( 𝑦 ( ball β€˜ 𝐷 ) π‘Ÿ ) βŠ† π‘₯ ↔ βˆƒ π‘Ÿ ∈ ℝ+ ( ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ ) )
119 118 anassrs ⊒ ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ π‘Œ βŠ† 𝑋 ) ∧ 𝑦 ∈ π‘Œ ) β†’ ( βˆƒ π‘Ÿ ∈ ℝ+ ( 𝑦 ( ball β€˜ 𝐷 ) π‘Ÿ ) βŠ† π‘₯ ↔ βˆƒ π‘Ÿ ∈ ℝ+ ( ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ ) )
120 25 119 sylan2 ⊒ ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ π‘Œ βŠ† 𝑋 ) ∧ ( π‘₯ βŠ† π‘Œ ∧ 𝑦 ∈ π‘₯ ) ) β†’ ( βˆƒ π‘Ÿ ∈ ℝ+ ( 𝑦 ( ball β€˜ 𝐷 ) π‘Ÿ ) βŠ† π‘₯ ↔ βˆƒ π‘Ÿ ∈ ℝ+ ( ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ ) )
121 120 anassrs ⊒ ( ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ π‘Œ βŠ† 𝑋 ) ∧ π‘₯ βŠ† π‘Œ ) ∧ 𝑦 ∈ π‘₯ ) β†’ ( βˆƒ π‘Ÿ ∈ ℝ+ ( 𝑦 ( ball β€˜ 𝐷 ) π‘Ÿ ) βŠ† π‘₯ ↔ βˆƒ π‘Ÿ ∈ ℝ+ ( ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ ) )
122 121 ralbidva ⊒ ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ π‘Œ βŠ† 𝑋 ) ∧ π‘₯ βŠ† π‘Œ ) β†’ ( βˆ€ 𝑦 ∈ π‘₯ βˆƒ π‘Ÿ ∈ ℝ+ ( 𝑦 ( ball β€˜ 𝐷 ) π‘Ÿ ) βŠ† π‘₯ ↔ βˆ€ 𝑦 ∈ π‘₯ βˆƒ π‘Ÿ ∈ ℝ+ ( ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ ) )
123 122 pm5.32da ⊒ ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ π‘Œ βŠ† 𝑋 ) β†’ ( ( π‘₯ βŠ† π‘Œ ∧ βˆ€ 𝑦 ∈ π‘₯ βˆƒ π‘Ÿ ∈ ℝ+ ( 𝑦 ( ball β€˜ 𝐷 ) π‘Ÿ ) βŠ† π‘₯ ) ↔ ( π‘₯ βŠ† π‘Œ ∧ βˆ€ 𝑦 ∈ π‘₯ βˆƒ π‘Ÿ ∈ ℝ+ ( ( 𝑦 ( ball β€˜ 𝐢 ) π‘Ÿ ) ∩ π‘Œ ) βŠ† π‘₯ ) ) )
124 110 123 bitr4d ⊒ ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ π‘Œ βŠ† 𝑋 ) β†’ ( βˆƒ 𝑒 ∈ 𝐽 π‘₯ = ( 𝑒 ∩ π‘Œ ) ↔ ( π‘₯ βŠ† π‘Œ ∧ βˆ€ 𝑦 ∈ π‘₯ βˆƒ π‘Ÿ ∈ ℝ+ ( 𝑦 ( ball β€˜ 𝐷 ) π‘Ÿ ) βŠ† π‘₯ ) ) )
125 id ⊒ ( π‘Œ βŠ† 𝑋 β†’ π‘Œ βŠ† 𝑋 )
126 2 mopnm ⊒ ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) β†’ 𝑋 ∈ 𝐽 )
127 ssexg ⊒ ( ( π‘Œ βŠ† 𝑋 ∧ 𝑋 ∈ 𝐽 ) β†’ π‘Œ ∈ V )
128 125 126 127 syl2anr ⊒ ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ π‘Œ βŠ† 𝑋 ) β†’ π‘Œ ∈ V )
129 elrest ⊒ ( ( 𝐽 ∈ Top ∧ π‘Œ ∈ V ) β†’ ( π‘₯ ∈ ( 𝐽 β†Ύt π‘Œ ) ↔ βˆƒ 𝑒 ∈ 𝐽 π‘₯ = ( 𝑒 ∩ π‘Œ ) ) )
130 23 128 129 syl2an2r ⊒ ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ π‘Œ βŠ† 𝑋 ) β†’ ( π‘₯ ∈ ( 𝐽 β†Ύt π‘Œ ) ↔ βˆƒ 𝑒 ∈ 𝐽 π‘₯ = ( 𝑒 ∩ π‘Œ ) ) )
131 xmetres2 ⊒ ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ π‘Œ βŠ† 𝑋 ) β†’ ( 𝐢 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ∈ ( ∞Met β€˜ π‘Œ ) )
132 1 131 eqeltrid ⊒ ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ π‘Œ βŠ† 𝑋 ) β†’ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) )
133 3 elmopn2 ⊒ ( 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) β†’ ( π‘₯ ∈ 𝐾 ↔ ( π‘₯ βŠ† π‘Œ ∧ βˆ€ 𝑦 ∈ π‘₯ βˆƒ π‘Ÿ ∈ ℝ+ ( 𝑦 ( ball β€˜ 𝐷 ) π‘Ÿ ) βŠ† π‘₯ ) ) )
134 132 133 syl ⊒ ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ π‘Œ βŠ† 𝑋 ) β†’ ( π‘₯ ∈ 𝐾 ↔ ( π‘₯ βŠ† π‘Œ ∧ βˆ€ 𝑦 ∈ π‘₯ βˆƒ π‘Ÿ ∈ ℝ+ ( 𝑦 ( ball β€˜ 𝐷 ) π‘Ÿ ) βŠ† π‘₯ ) ) )
135 124 130 134 3bitr4d ⊒ ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ π‘Œ βŠ† 𝑋 ) β†’ ( π‘₯ ∈ ( 𝐽 β†Ύt π‘Œ ) ↔ π‘₯ ∈ 𝐾 ) )
136 135 eqrdv ⊒ ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ π‘Œ βŠ† 𝑋 ) β†’ ( 𝐽 β†Ύt π‘Œ ) = 𝐾 )