Metamath Proof Explorer

Theorem pcofval

Description: The value of the path concatenation function on a topological space. (Contributed by Jeff Madsen, 15-Jun-2010) (Revised by Mario Carneiro, 7-Jun-2014) (Proof shortened by AV, 2-Mar-2024)

Ref Expression
Assertion pcofval ⊢ * 𝑝 ⁡ J = f ∈ II Cn J , g ∈ II Cn J ⟼ x ∈ 0 1 ⟼ if x ≤ 1 2 f ⁡ 2 ⁢ x g ⁡ 2 ⁢ x − 1

Proof

Step Hyp Ref Expression
1 oveq2 ⊢ j = J → II Cn j = II Cn J
2 eqidd ⊢ j = J → x ∈ 0 1 ⟼ if x ≤ 1 2 f ⁡ 2 ⁢ x g ⁡ 2 ⁢ x − 1 = x ∈ 0 1 ⟼ if x ≤ 1 2 f ⁡ 2 ⁢ x g ⁡ 2 ⁢ x − 1
3 1 1 2 mpoeq123dv ⊢ j = J → f ∈ II Cn j , g ∈ II Cn j ⟼ x ∈ 0 1 ⟼ if x ≤ 1 2 f ⁡ 2 ⁢ x g ⁡ 2 ⁢ x − 1 = f ∈ II Cn J , g ∈ II Cn J ⟼ x ∈ 0 1 ⟼ if x ≤ 1 2 f ⁡ 2 ⁢ x g ⁡ 2 ⁢ x − 1
4 df-pco ⊢ * 𝑝 = j ∈ Top ⟼ f ∈ II Cn j , g ∈ II Cn j ⟼ x ∈ 0 1 ⟼ if x ≤ 1 2 f ⁡ 2 ⁢ x g ⁡ 2 ⁢ x − 1
5 ovex ⊢ II Cn J ∈ V
6 5 5 mpoex ⊢ f ∈ II Cn J , g ∈ II Cn J ⟼ x ∈ 0 1 ⟼ if x ≤ 1 2 f ⁡ 2 ⁢ x g ⁡ 2 ⁢ x − 1 ∈ V
7 3 4 6 fvmpt ⊢ J ∈ Top → * 𝑝 ⁡ J = f ∈ II Cn J , g ∈ II Cn J ⟼ x ∈ 0 1 ⟼ if x ≤ 1 2 f ⁡ 2 ⁢ x g ⁡ 2 ⁢ x − 1
8 4 fvmptndm ⊢ ¬ J ∈ Top → * 𝑝 ⁡ J = ∅
9 cntop2 ⊢ f ∈ II Cn J → J ∈ Top
10 9 con3i ⊢ ¬ J ∈ Top → ¬ f ∈ II Cn J
11 10 eq0rdv ⊢ ¬ J ∈ Top → II Cn J = ∅
12 11 olcd ⊢ ¬ J ∈ Top → II Cn J = ∅ ∨ II Cn J = ∅
13 0mpo0 ⊢ II Cn J = ∅ ∨ II Cn J = ∅ → f ∈ II Cn J , g ∈ II Cn J ⟼ x ∈ 0 1 ⟼ if x ≤ 1 2 f ⁡ 2 ⁢ x g ⁡ 2 ⁢ x − 1 = ∅
14 12 13 syl ⊢ ¬ J ∈ Top → f ∈ II Cn J , g ∈ II Cn J ⟼ x ∈ 0 1 ⟼ if x ≤ 1 2 f ⁡ 2 ⁢ x g ⁡ 2 ⁢ x − 1 = ∅
15 8 14 eqtr4d ⊢ ¬ J ∈ Top → * 𝑝 ⁡ J = f ∈ II Cn J , g ∈ II Cn J ⟼ x ∈ 0 1 ⟼ if x ≤ 1 2 f ⁡ 2 ⁢ x g ⁡ 2 ⁢ x − 1
16 7 15 pm2.61i ⊢ * 𝑝 ⁡ J = f ∈ II Cn J , g ∈ II Cn J ⟼ x ∈ 0 1 ⟼ if x ≤ 1 2 f ⁡ 2 ⁢ x g ⁡ 2 ⁢ x − 1