Metamath Proof Explorer

Definition df-cplmet

Description: A function which completes the given metric space. (Contributed by Mario Carneiro, 2-Dec-2014)

Ref Expression
Assertion df-cplmet cplMetSp = ( 𝑤 ∈ V ↦ ⦋ ( ( 𝑤 ↑s ℕ ) ↾s ( Cau ‘ ( dist ‘ 𝑤 ) ) ) / 𝑟 ⦌ ⦋ ( Base ‘ 𝑟 ) / 𝑣 ⦌ ⦋ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ 𝑣 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℤ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ( ( 𝑔 ‘ 𝑗 ) ( ball ‘ ( dist ‘ 𝑤 ) ) 𝑥 ) ) } / 𝑒 ⦌ ( ( 𝑟 /s 𝑒 ) sSet { ⟨ ( dist ‘ ndx ) , { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ∃ 𝑝 ∈ 𝑣 ∃ 𝑞 ∈ 𝑣 ( ( 𝑥 = [ 𝑝 ] 𝑒 ∧ 𝑦 = [ 𝑞 ] 𝑒 ) ∧ ( 𝑝 ∘f ( dist ‘ 𝑟 ) 𝑞 ) ⇝ 𝑧 ) } ⟩ } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccpms ⊢ cplMetSp
1 vw ⊢ 𝑤
2 cvv ⊢ V
3 1 cv ⊢ 𝑤
4 cpws ⊢ ↑s
5 cn ⊢ ℕ
6 3 5 4 co ⊢ ( 𝑤 ↑s ℕ )
7 cress ⊢ ↾s
8 ccau ⊢ Cau
9 cds ⊢ dist
10 3 9 cfv ⊢ ( dist ‘ 𝑤 )
11 10 8 cfv ⊢ ( Cau ‘ ( dist ‘ 𝑤 ) )
12 6 11 7 co ⊢ ( ( 𝑤 ↑s ℕ ) ↾s ( Cau ‘ ( dist ‘ 𝑤 ) ) )
13 vr ⊢ 𝑟
14 cbs ⊢ Base
15 13 cv ⊢ 𝑟
16 15 14 cfv ⊢ ( Base ‘ 𝑟 )
17 vv ⊢ 𝑣
18 vf ⊢ 𝑓
19 vg ⊢ 𝑔
20 18 cv ⊢ 𝑓
21 19 cv ⊢ 𝑔
22 20 21 cpr ⊢ { 𝑓 , 𝑔 }
23 17 cv ⊢ 𝑣
24 22 23 wss ⊢ { 𝑓 , 𝑔 } ⊆ 𝑣
25 vx ⊢ 𝑥
26 crp ⊢ ℝ+
27 vj ⊢ 𝑗
28 cz ⊢ ℤ
29 cuz ⊢ ℤ≥
30 27 cv ⊢ 𝑗
31 30 29 cfv ⊢ ( ℤ≥ ‘ 𝑗 )
32 20 31 cres ⊢ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑗 ) )
33 30 21 cfv ⊢ ( 𝑔 ‘ 𝑗 )
34 cbl ⊢ ball
35 10 34 cfv ⊢ ( ball ‘ ( dist ‘ 𝑤 ) )
36 25 cv ⊢ 𝑥
37 33 36 35 co ⊢ ( ( 𝑔 ‘ 𝑗 ) ( ball ‘ ( dist ‘ 𝑤 ) ) 𝑥 )
38 31 37 32 wf ⊢ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ( ( 𝑔 ‘ 𝑗 ) ( ball ‘ ( dist ‘ 𝑤 ) ) 𝑥 )
39 38 27 28 wrex ⊢ ∃ 𝑗 ∈ ℤ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ( ( 𝑔 ‘ 𝑗 ) ( ball ‘ ( dist ‘ 𝑤 ) ) 𝑥 )
40 39 25 26 wral ⊢ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℤ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ( ( 𝑔 ‘ 𝑗 ) ( ball ‘ ( dist ‘ 𝑤 ) ) 𝑥 )
41 24 40 wa ⊢ ( { 𝑓 , 𝑔 } ⊆ 𝑣 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℤ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ( ( 𝑔 ‘ 𝑗 ) ( ball ‘ ( dist ‘ 𝑤 ) ) 𝑥 ) )
42 41 18 19 copab ⊢ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ 𝑣 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℤ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ( ( 𝑔 ‘ 𝑗 ) ( ball ‘ ( dist ‘ 𝑤 ) ) 𝑥 ) ) }
43 ve ⊢ 𝑒
44 cqus ⊢ /s
45 43 cv ⊢ 𝑒
46 15 45 44 co ⊢ ( 𝑟 /s 𝑒 )
47 csts ⊢ sSet
48 cnx ⊢ ndx
49 48 9 cfv ⊢ ( dist ‘ ndx )
50 vy ⊢ 𝑦
51 vz ⊢ 𝑧
52 vp ⊢ 𝑝
53 vq ⊢ 𝑞
54 52 cv ⊢ 𝑝
55 54 45 cec ⊢ [ 𝑝 ] 𝑒
56 36 55 wceq ⊢ 𝑥 = [ 𝑝 ] 𝑒
57 50 cv ⊢ 𝑦
58 53 cv ⊢ 𝑞
59 58 45 cec ⊢ [ 𝑞 ] 𝑒
60 57 59 wceq ⊢ 𝑦 = [ 𝑞 ] 𝑒
61 56 60 wa ⊢ ( 𝑥 = [ 𝑝 ] 𝑒 ∧ 𝑦 = [ 𝑞 ] 𝑒 )
62 15 9 cfv ⊢ ( dist ‘ 𝑟 )
63 62 cof ⊢ ∘f ( dist ‘ 𝑟 )
64 54 58 63 co ⊢ ( 𝑝 ∘f ( dist ‘ 𝑟 ) 𝑞 )
65 cli ⊢ ⇝
66 51 cv ⊢ 𝑧
67 64 66 65 wbr ⊢ ( 𝑝 ∘f ( dist ‘ 𝑟 ) 𝑞 ) ⇝ 𝑧
68 61 67 wa ⊢ ( ( 𝑥 = [ 𝑝 ] 𝑒 ∧ 𝑦 = [ 𝑞 ] 𝑒 ) ∧ ( 𝑝 ∘f ( dist ‘ 𝑟 ) 𝑞 ) ⇝ 𝑧 )
69 68 53 23 wrex ⊢ ∃ 𝑞 ∈ 𝑣 ( ( 𝑥 = [ 𝑝 ] 𝑒 ∧ 𝑦 = [ 𝑞 ] 𝑒 ) ∧ ( 𝑝 ∘f ( dist ‘ 𝑟 ) 𝑞 ) ⇝ 𝑧 )
70 69 52 23 wrex ⊢ ∃ 𝑝 ∈ 𝑣 ∃ 𝑞 ∈ 𝑣 ( ( 𝑥 = [ 𝑝 ] 𝑒 ∧ 𝑦 = [ 𝑞 ] 𝑒 ) ∧ ( 𝑝 ∘f ( dist ‘ 𝑟 ) 𝑞 ) ⇝ 𝑧 )
71 70 25 50 51 coprab ⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ∃ 𝑝 ∈ 𝑣 ∃ 𝑞 ∈ 𝑣 ( ( 𝑥 = [ 𝑝 ] 𝑒 ∧ 𝑦 = [ 𝑞 ] 𝑒 ) ∧ ( 𝑝 ∘f ( dist ‘ 𝑟 ) 𝑞 ) ⇝ 𝑧 ) }
72 49 71 cop ⊢ ⟨ ( dist ‘ ndx ) , { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ∃ 𝑝 ∈ 𝑣 ∃ 𝑞 ∈ 𝑣 ( ( 𝑥 = [ 𝑝 ] 𝑒 ∧ 𝑦 = [ 𝑞 ] 𝑒 ) ∧ ( 𝑝 ∘f ( dist ‘ 𝑟 ) 𝑞 ) ⇝ 𝑧 ) } ⟩
73 72 csn ⊢ { ⟨ ( dist ‘ ndx ) , { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ∃ 𝑝 ∈ 𝑣 ∃ 𝑞 ∈ 𝑣 ( ( 𝑥 = [ 𝑝 ] 𝑒 ∧ 𝑦 = [ 𝑞 ] 𝑒 ) ∧ ( 𝑝 ∘f ( dist ‘ 𝑟 ) 𝑞 ) ⇝ 𝑧 ) } ⟩ }
74 46 73 47 co ⊢ ( ( 𝑟 /s 𝑒 ) sSet { ⟨ ( dist ‘ ndx ) , { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ∃ 𝑝 ∈ 𝑣 ∃ 𝑞 ∈ 𝑣 ( ( 𝑥 = [ 𝑝 ] 𝑒 ∧ 𝑦 = [ 𝑞 ] 𝑒 ) ∧ ( 𝑝 ∘f ( dist ‘ 𝑟 ) 𝑞 ) ⇝ 𝑧 ) } ⟩ } )
75 43 42 74 csb ⊢ ⦋ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ 𝑣 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℤ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ( ( 𝑔 ‘ 𝑗 ) ( ball ‘ ( dist ‘ 𝑤 ) ) 𝑥 ) ) } / 𝑒 ⦌ ( ( 𝑟 /s 𝑒 ) sSet { ⟨ ( dist ‘ ndx ) , { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ∃ 𝑝 ∈ 𝑣 ∃ 𝑞 ∈ 𝑣 ( ( 𝑥 = [ 𝑝 ] 𝑒 ∧ 𝑦 = [ 𝑞 ] 𝑒 ) ∧ ( 𝑝 ∘f ( dist ‘ 𝑟 ) 𝑞 ) ⇝ 𝑧 ) } ⟩ } )
76 17 16 75 csb ⊢ ⦋ ( Base ‘ 𝑟 ) / 𝑣 ⦌ ⦋ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ 𝑣 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℤ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ( ( 𝑔 ‘ 𝑗 ) ( ball ‘ ( dist ‘ 𝑤 ) ) 𝑥 ) ) } / 𝑒 ⦌ ( ( 𝑟 /s 𝑒 ) sSet { ⟨ ( dist ‘ ndx ) , { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ∃ 𝑝 ∈ 𝑣 ∃ 𝑞 ∈ 𝑣 ( ( 𝑥 = [ 𝑝 ] 𝑒 ∧ 𝑦 = [ 𝑞 ] 𝑒 ) ∧ ( 𝑝 ∘f ( dist ‘ 𝑟 ) 𝑞 ) ⇝ 𝑧 ) } ⟩ } )
77 13 12 76 csb ⊢ ⦋ ( ( 𝑤 ↑s ℕ ) ↾s ( Cau ‘ ( dist ‘ 𝑤 ) ) ) / 𝑟 ⦌ ⦋ ( Base ‘ 𝑟 ) / 𝑣 ⦌ ⦋ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ 𝑣 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℤ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ( ( 𝑔 ‘ 𝑗 ) ( ball ‘ ( dist ‘ 𝑤 ) ) 𝑥 ) ) } / 𝑒 ⦌ ( ( 𝑟 /s 𝑒 ) sSet { ⟨ ( dist ‘ ndx ) , { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ∃ 𝑝 ∈ 𝑣 ∃ 𝑞 ∈ 𝑣 ( ( 𝑥 = [ 𝑝 ] 𝑒 ∧ 𝑦 = [ 𝑞 ] 𝑒 ) ∧ ( 𝑝 ∘f ( dist ‘ 𝑟 ) 𝑞 ) ⇝ 𝑧 ) } ⟩ } )
78 1 2 77 cmpt ⊢ ( 𝑤 ∈ V ↦ ⦋ ( ( 𝑤 ↑s ℕ ) ↾s ( Cau ‘ ( dist ‘ 𝑤 ) ) ) / 𝑟 ⦌ ⦋ ( Base ‘ 𝑟 ) / 𝑣 ⦌ ⦋ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ 𝑣 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℤ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ( ( 𝑔 ‘ 𝑗 ) ( ball ‘ ( dist ‘ 𝑤 ) ) 𝑥 ) ) } / 𝑒 ⦌ ( ( 𝑟 /s 𝑒 ) sSet { ⟨ ( dist ‘ ndx ) , { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ∃ 𝑝 ∈ 𝑣 ∃ 𝑞 ∈ 𝑣 ( ( 𝑥 = [ 𝑝 ] 𝑒 ∧ 𝑦 = [ 𝑞 ] 𝑒 ) ∧ ( 𝑝 ∘f ( dist ‘ 𝑟 ) 𝑞 ) ⇝ 𝑧 ) } ⟩ } ) )
79 0 78 wceq ⊢ cplMetSp = ( 𝑤 ∈ V ↦ ⦋ ( ( 𝑤 ↑s ℕ ) ↾s ( Cau ‘ ( dist ‘ 𝑤 ) ) ) / 𝑟 ⦌ ⦋ ( Base ‘ 𝑟 ) / 𝑣 ⦌ ⦋ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ 𝑣 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℤ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ( ( 𝑔 ‘ 𝑗 ) ( ball ‘ ( dist ‘ 𝑤 ) ) 𝑥 ) ) } / 𝑒 ⦌ ( ( 𝑟 /s 𝑒 ) sSet { ⟨ ( dist ‘ ndx ) , { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ∃ 𝑝 ∈ 𝑣 ∃ 𝑞 ∈ 𝑣 ( ( 𝑥 = [ 𝑝 ] 𝑒 ∧ 𝑦 = [ 𝑞 ] 𝑒 ) ∧ ( 𝑝 ∘f ( dist ‘ 𝑟 ) 𝑞 ) ⇝ 𝑧 ) } ⟩ } ) )