Theorem isphtpc 23163

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

Assertion

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

Proof of Theorem isphtpc

Dummy variables 𝑓 𝑔 𝑗 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-br 4874	. . 3 ⊢ (𝐹( ≃ph‘𝐽)𝐺 ↔ ⟨𝐹, 𝐺⟩ ∈ ( ≃ph‘𝐽))
2		df-phtpc 23161	. . . . 5 ⊢ ≃ph = (𝑗 ∈ Top ↦ {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ (II Cn 𝑗) ∧ (𝑓(PHtpy‘𝑗)𝑔) ≠ ∅)})
3	2	dmmptss 5872	. . . 4 ⊢ dom ≃ph ⊆ Top
4		elfvdm 6465	. . . 4 ⊢ (⟨𝐹, 𝐺⟩ ∈ ( ≃ph‘𝐽) → 𝐽 ∈ dom ≃ph)
5	3, 4	sseldi 3825	. . 3 ⊢ (⟨𝐹, 𝐺⟩ ∈ ( ≃ph‘𝐽) → 𝐽 ∈ Top)
6	1, 5	sylbi 209	. 2 ⊢ (𝐹( ≃ph‘𝐽)𝐺 → 𝐽 ∈ Top)
7		cntop2 21416	. . 3 ⊢ (𝐹 ∈ (II Cn 𝐽) → 𝐽 ∈ Top)
8	7	3ad2ant1 1167	. 2 ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝐺 ∈ (II Cn 𝐽) ∧ (𝐹(PHtpy‘𝐽)𝐺) ≠ ∅) → 𝐽 ∈ Top)
9		oveq2 6913	. . . . . . . . 9 ⊢ (𝑗 = 𝐽 → (II Cn 𝑗) = (II Cn 𝐽))
10	9	sseq2d 3858	. . . . . . . 8 ⊢ (𝑗 = 𝐽 → ({𝑓, 𝑔} ⊆ (II Cn 𝑗) ↔ {𝑓, 𝑔} ⊆ (II Cn 𝐽)))
11		vex 3417	. . . . . . . . 9 ⊢ 𝑓 ∈ V
12		vex 3417	. . . . . . . . 9 ⊢ 𝑔 ∈ V
13	11, 12	prss 4569	. . . . . . . 8 ⊢ ((𝑓 ∈ (II Cn 𝐽) ∧ 𝑔 ∈ (II Cn 𝐽)) ↔ {𝑓, 𝑔} ⊆ (II Cn 𝐽))
14	10, 13	syl6bbr 281	. . . . . . 7 ⊢ (𝑗 = 𝐽 → ({𝑓, 𝑔} ⊆ (II Cn 𝑗) ↔ (𝑓 ∈ (II Cn 𝐽) ∧ 𝑔 ∈ (II Cn 𝐽))))
15		fveq2 6433	. . . . . . . . 9 ⊢ (𝑗 = 𝐽 → (PHtpy‘𝑗) = (PHtpy‘𝐽))
16	15	oveqd 6922	. . . . . . . 8 ⊢ (𝑗 = 𝐽 → (𝑓(PHtpy‘𝑗)𝑔) = (𝑓(PHtpy‘𝐽)𝑔))
17	16	neeq1d 3058	. . . . . . 7 ⊢ (𝑗 = 𝐽 → ((𝑓(PHtpy‘𝑗)𝑔) ≠ ∅ ↔ (𝑓(PHtpy‘𝐽)𝑔) ≠ ∅))
18	14, 17	anbi12d 624	. . . . . 6 ⊢ (𝑗 = 𝐽 → (({𝑓, 𝑔} ⊆ (II Cn 𝑗) ∧ (𝑓(PHtpy‘𝑗)𝑔) ≠ ∅) ↔ ((𝑓 ∈ (II Cn 𝐽) ∧ 𝑔 ∈ (II Cn 𝐽)) ∧ (𝑓(PHtpy‘𝐽)𝑔) ≠ ∅)))
19	18	opabbidv 4939	. . . . 5 ⊢ (𝑗 = 𝐽 → {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ (II Cn 𝑗) ∧ (𝑓(PHtpy‘𝑗)𝑔) ≠ ∅)} = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (II Cn 𝐽) ∧ 𝑔 ∈ (II Cn 𝐽)) ∧ (𝑓(PHtpy‘𝐽)𝑔) ≠ ∅)})
20		ovex 6937	. . . . . . 7 ⊢ (II Cn 𝐽) ∈ V
21	20, 20	xpex 7223	. . . . . 6 ⊢ ((II Cn 𝐽) × (II Cn 𝐽)) ∈ V
22		opabssxp 5428	. . . . . 6 ⊢ {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (II Cn 𝐽) ∧ 𝑔 ∈ (II Cn 𝐽)) ∧ (𝑓(PHtpy‘𝐽)𝑔) ≠ ∅)} ⊆ ((II Cn 𝐽) × (II Cn 𝐽))
23	21, 22	ssexi 5028	. . . . 5 ⊢ {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (II Cn 𝐽) ∧ 𝑔 ∈ (II Cn 𝐽)) ∧ (𝑓(PHtpy‘𝐽)𝑔) ≠ ∅)} ∈ V
24	19, 2, 23	fvmpt 6529	. . . 4 ⊢ (𝐽 ∈ Top → ( ≃ph‘𝐽) = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (II Cn 𝐽) ∧ 𝑔 ∈ (II Cn 𝐽)) ∧ (𝑓(PHtpy‘𝐽)𝑔) ≠ ∅)})
25	24	breqd 4884	. . 3 ⊢ (𝐽 ∈ Top → (𝐹( ≃ph‘𝐽)𝐺 ↔ 𝐹{⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (II Cn 𝐽) ∧ 𝑔 ∈ (II Cn 𝐽)) ∧ (𝑓(PHtpy‘𝐽)𝑔) ≠ ∅)}𝐺))
26		oveq12 6914	. . . . . 6 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝑓(PHtpy‘𝐽)𝑔) = (𝐹(PHtpy‘𝐽)𝐺))
27	26	neeq1d 3058	. . . . 5 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → ((𝑓(PHtpy‘𝐽)𝑔) ≠ ∅ ↔ (𝐹(PHtpy‘𝐽)𝐺) ≠ ∅))
28		eqid 2825	. . . . 5 ⊢ {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (II Cn 𝐽) ∧ 𝑔 ∈ (II Cn 𝐽)) ∧ (𝑓(PHtpy‘𝐽)𝑔) ≠ ∅)} = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (II Cn 𝐽) ∧ 𝑔 ∈ (II Cn 𝐽)) ∧ (𝑓(PHtpy‘𝐽)𝑔) ≠ ∅)}
29	27, 28	brab2a 5429	. . . 4 ⊢ (𝐹{⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (II Cn 𝐽) ∧ 𝑔 ∈ (II Cn 𝐽)) ∧ (𝑓(PHtpy‘𝐽)𝑔) ≠ ∅)}𝐺 ↔ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝐺 ∈ (II Cn 𝐽)) ∧ (𝐹(PHtpy‘𝐽)𝐺) ≠ ∅))
30		df-3an 1113	. . . 4 ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝐺 ∈ (II Cn 𝐽) ∧ (𝐹(PHtpy‘𝐽)𝐺) ≠ ∅) ↔ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝐺 ∈ (II Cn 𝐽)) ∧ (𝐹(PHtpy‘𝐽)𝐺) ≠ ∅))
31	29, 30	bitr4i 270	. . 3 ⊢ (𝐹{⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (II Cn 𝐽) ∧ 𝑔 ∈ (II Cn 𝐽)) ∧ (𝑓(PHtpy‘𝐽)𝑔) ≠ ∅)}𝐺 ↔ (𝐹 ∈ (II Cn 𝐽) ∧ 𝐺 ∈ (II Cn 𝐽) ∧ (𝐹(PHtpy‘𝐽)𝐺) ≠ ∅))
32	25, 31	syl6bb 279	. 2 ⊢ (𝐽 ∈ Top → (𝐹( ≃ph‘𝐽)𝐺 ↔ (𝐹 ∈ (II Cn 𝐽) ∧ 𝐺 ∈ (II Cn 𝐽) ∧ (𝐹(PHtpy‘𝐽)𝐺) ≠ ∅)))
33	6, 8, 32	pm5.21nii 370	1 ⊢ (𝐹( ≃ph‘𝐽)𝐺 ↔ (𝐹 ∈ (II Cn 𝐽) ∧ 𝐺 ∈ (II Cn 𝐽) ∧ (𝐹(PHtpy‘𝐽)𝐺) ≠ ∅))

Syntax hints:   ↔ wb 198   ∧ wa 386   ∧ w3a 1111   = wceq 1656   ∈ wcel 2164   ≠ wne 2999   ⊆ wss 3798  ∅c0 4144  {cpr 4399  ⟨cop 4403   class class class wbr 4873  {copab 4935   × cxp 5340  dom cdm 5342  ‘cfv 6123  (class class class)co 6905  Topctop 21068   Cn ccn 21399  IIcii 23048  PHtpycphtpy 23137   ≃_phcphtpc 23138

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-8 2166  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803  ax-sep 5005  ax-nul 5013  ax-pow 5065  ax-pr 5127  ax-un 7209

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-3an 1113  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ne 3000  df-ral 3122  df-rex 3123  df-rab 3126  df-v 3416  df-sbc 3663  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4145  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-op 4404  df-uni 4659  df-br 4874  df-opab 4936  df-mpt 4953  df-id 5250  df-xp 5348  df-rel 5349  df-cnv 5350  df-co 5351  df-dm 5352  df-rn 5353  df-res 5354  df-ima 5355  df-iota 6086  df-fun 6125  df-fn 6126  df-f 6127  df-fv 6131  df-ov 6908  df-oprab 6909  df-mpt2 6910  df-map 8124  df-top 21069  df-topon 21086  df-cn 21402  df-phtpc 23161

This theorem is referenced by:  phtpcer  23164  phtpc01  23165  reparpht  23167  phtpcco2  23168  pcohtpylem  23188  pcohtpy  23189  pcorevlem  23195  pi1blem  23208  txsconnlem  31757  txsconn  31758  cvxsconn  31760  cvmliftpht  31835