Metamath Proof Explorer

Theorem isphtpc

Description: The relation "is path homotopic to". (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 5-Sep-2015)

Ref Expression
Assertion isphtpc ( 𝐹 ( ≃ph ‘ 𝐽 ) 𝐺 ↔ ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ 𝐺 ∈ ( II Cn 𝐽 ) ∧ ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐺 ) ≠ ∅ ) )

Proof

Step Hyp Ref Expression
1 df-br ⊢ ( 𝐹 ( ≃ph ‘ 𝐽 ) 𝐺 ↔ ⟨ 𝐹 , 𝐺 ⟩ ∈ ( ≃ph ‘ 𝐽 ) )
2 df-phtpc ⊢ ≃ph = ( 𝑗 ∈ Top ↦ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ ( II Cn 𝑗 ) ∧ ( 𝑓 ( PHtpy ‘ 𝑗 ) 𝑔 ) ≠ ∅ ) } )
3 2 mptrcl ⊢ ( ⟨ 𝐹 , 𝐺 ⟩ ∈ ( ≃ph ‘ 𝐽 ) → 𝐽 ∈ Top )
4 1 3 sylbi ⊢ ( 𝐹 ( ≃ph ‘ 𝐽 ) 𝐺 → 𝐽 ∈ Top )
5 cntop2 ⊢ ( 𝐹 ∈ ( II Cn 𝐽 ) → 𝐽 ∈ Top )
6 5 3ad2ant1 ⊢ ( ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ 𝐺 ∈ ( II Cn 𝐽 ) ∧ ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐺 ) ≠ ∅ ) → 𝐽 ∈ Top )
7 oveq2 ⊢ ( 𝑗 = 𝐽 → ( II Cn 𝑗 ) = ( II Cn 𝐽 ) )
8 7 sseq2d ⊢ ( 𝑗 = 𝐽 → ( { 𝑓 , 𝑔 } ⊆ ( II Cn 𝑗 ) ↔ { 𝑓 , 𝑔 } ⊆ ( II Cn 𝐽 ) ) )
9 vex ⊢ 𝑓 ∈ V
10 vex ⊢ 𝑔 ∈ V
11 9 10 prss ⊢ ( ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ 𝑔 ∈ ( II Cn 𝐽 ) ) ↔ { 𝑓 , 𝑔 } ⊆ ( II Cn 𝐽 ) )
12 8 11 bitr4di ⊢ ( 𝑗 = 𝐽 → ( { 𝑓 , 𝑔 } ⊆ ( II Cn 𝑗 ) ↔ ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ 𝑔 ∈ ( II Cn 𝐽 ) ) ) )
13 fveq2 ⊢ ( 𝑗 = 𝐽 → ( PHtpy ‘ 𝑗 ) = ( PHtpy ‘ 𝐽 ) )
14 13 oveqd ⊢ ( 𝑗 = 𝐽 → ( 𝑓 ( PHtpy ‘ 𝑗 ) 𝑔 ) = ( 𝑓 ( PHtpy ‘ 𝐽 ) 𝑔 ) )
15 14 neeq1d ⊢ ( 𝑗 = 𝐽 → ( ( 𝑓 ( PHtpy ‘ 𝑗 ) 𝑔 ) ≠ ∅ ↔ ( 𝑓 ( PHtpy ‘ 𝐽 ) 𝑔 ) ≠ ∅ ) )
16 12 15 anbi12d ⊢ ( 𝑗 = 𝐽 → ( ( { 𝑓 , 𝑔 } ⊆ ( II Cn 𝑗 ) ∧ ( 𝑓 ( PHtpy ‘ 𝑗 ) 𝑔 ) ≠ ∅ ) ↔ ( ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ 𝑔 ∈ ( II Cn 𝐽 ) ) ∧ ( 𝑓 ( PHtpy ‘ 𝐽 ) 𝑔 ) ≠ ∅ ) ) )
17 16 opabbidv ⊢ ( 𝑗 = 𝐽 → { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ ( II Cn 𝑗 ) ∧ ( 𝑓 ( PHtpy ‘ 𝑗 ) 𝑔 ) ≠ ∅ ) } = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ 𝑔 ∈ ( II Cn 𝐽 ) ) ∧ ( 𝑓 ( PHtpy ‘ 𝐽 ) 𝑔 ) ≠ ∅ ) } )
18 ovex ⊢ ( II Cn 𝐽 ) ∈ V
19 18 18 xpex ⊢ ( ( II Cn 𝐽 ) × ( II Cn 𝐽 ) ) ∈ V
20 opabssxp ⊢ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ 𝑔 ∈ ( II Cn 𝐽 ) ) ∧ ( 𝑓 ( PHtpy ‘ 𝐽 ) 𝑔 ) ≠ ∅ ) } ⊆ ( ( II Cn 𝐽 ) × ( II Cn 𝐽 ) )
21 19 20 ssexi ⊢ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ 𝑔 ∈ ( II Cn 𝐽 ) ) ∧ ( 𝑓 ( PHtpy ‘ 𝐽 ) 𝑔 ) ≠ ∅ ) } ∈ V
22 17 2 21 fvmpt ⊢ ( 𝐽 ∈ Top → ( ≃ph ‘ 𝐽 ) = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ 𝑔 ∈ ( II Cn 𝐽 ) ) ∧ ( 𝑓 ( PHtpy ‘ 𝐽 ) 𝑔 ) ≠ ∅ ) } )
23 22 breqd ⊢ ( 𝐽 ∈ Top → ( 𝐹 ( ≃ph ‘ 𝐽 ) 𝐺 ↔ 𝐹 { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ 𝑔 ∈ ( II Cn 𝐽 ) ) ∧ ( 𝑓 ( PHtpy ‘ 𝐽 ) 𝑔 ) ≠ ∅ ) } 𝐺 ) )
24 oveq12 ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( 𝑓 ( PHtpy ‘ 𝐽 ) 𝑔 ) = ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐺 ) )
25 24 neeq1d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( ( 𝑓 ( PHtpy ‘ 𝐽 ) 𝑔 ) ≠ ∅ ↔ ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐺 ) ≠ ∅ ) )
26 eqid ⊢ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ 𝑔 ∈ ( II Cn 𝐽 ) ) ∧ ( 𝑓 ( PHtpy ‘ 𝐽 ) 𝑔 ) ≠ ∅ ) } = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ 𝑔 ∈ ( II Cn 𝐽 ) ) ∧ ( 𝑓 ( PHtpy ‘ 𝐽 ) 𝑔 ) ≠ ∅ ) }
27 25 26 brab2a ⊢ ( 𝐹 { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ 𝑔 ∈ ( II Cn 𝐽 ) ) ∧ ( 𝑓 ( PHtpy ‘ 𝐽 ) 𝑔 ) ≠ ∅ ) } 𝐺 ↔ ( ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ 𝐺 ∈ ( II Cn 𝐽 ) ) ∧ ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐺 ) ≠ ∅ ) )
28 df-3an ⊢ ( ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ 𝐺 ∈ ( II Cn 𝐽 ) ∧ ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐺 ) ≠ ∅ ) ↔ ( ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ 𝐺 ∈ ( II Cn 𝐽 ) ) ∧ ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐺 ) ≠ ∅ ) )
29 27 28 bitr4i ⊢ ( 𝐹 { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ 𝑔 ∈ ( II Cn 𝐽 ) ) ∧ ( 𝑓 ( PHtpy ‘ 𝐽 ) 𝑔 ) ≠ ∅ ) } 𝐺 ↔ ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ 𝐺 ∈ ( II Cn 𝐽 ) ∧ ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐺 ) ≠ ∅ ) )
30 23 29 bitrdi ⊢ ( 𝐽 ∈ Top → ( 𝐹 ( ≃ph ‘ 𝐽 ) 𝐺 ↔ ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ 𝐺 ∈ ( II Cn 𝐽 ) ∧ ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐺 ) ≠ ∅ ) ) )
31 4 6 30 pm5.21nii ⊢ ( 𝐹 ( ≃ph ‘ 𝐽 ) 𝐺 ↔ ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ 𝐺 ∈ ( II Cn 𝐽 ) ∧ ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐺 ) ≠ ∅ ) )