Theorem ispconn 34500

Description: The property of being a path-connected topological space. (Contributed by Mario Carneiro, 11-Feb-2015.)

Hypothesis

Ref	Expression
ispconn.1	⊢ 𝑋 = ∪ 𝐽

Assertion

Ref	Expression
ispconn	⊢ (𝐽 ∈ PConn ↔ (𝐽 ∈ Top ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)))

Distinct variable groups:   𝑥,𝑓,𝑦,𝐽   𝑥,𝑋,𝑦

Allowed substitution hint:   𝑋(𝑓)

Proof of Theorem ispconn

Dummy variable 𝑗 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		unieq 4919	. . . 4 ⊢ (𝑗 = 𝐽 → ∪ 𝑗 = ∪ 𝐽)
2		ispconn.1	. . . 4 ⊢ 𝑋 = ∪ 𝐽
3	1, 2	eqtr4di 2790	. . 3 ⊢ (𝑗 = 𝐽 → ∪ 𝑗 = 𝑋)
4		oveq2 7419	. . . . 5 ⊢ (𝑗 = 𝐽 → (II Cn 𝑗) = (II Cn 𝐽))
5	4	rexeqdv 3326	. . . 4 ⊢ (𝑗 = 𝐽 → (∃𝑓 ∈ (II Cn 𝑗)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦) ↔ ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)))
6	3, 5	raleqbidv 3342	. . 3 ⊢ (𝑗 = 𝐽 → (∀𝑦 ∈ ∪ 𝑗∃𝑓 ∈ (II Cn 𝑗)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦) ↔ ∀𝑦 ∈ 𝑋 ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)))
7	3, 6	raleqbidv 3342	. 2 ⊢ (𝑗 = 𝐽 → (∀𝑥 ∈ ∪ 𝑗∀𝑦 ∈ ∪ 𝑗∃𝑓 ∈ (II Cn 𝑗)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦) ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)))
8		df-pconn 34498	. 2 ⊢ PConn = {𝑗 ∈ Top ∣ ∀𝑥 ∈ ∪ 𝑗∀𝑦 ∈ ∪ 𝑗∃𝑓 ∈ (II Cn 𝑗)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)}
9	7, 8	elrab2 3686	1 ⊢ (𝐽 ∈ PConn ↔ (𝐽 ∈ Top ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)))

Syntax hints:   ↔ wb 205   ∧ wa 396   = wceq 1541   ∈ wcel 2106  ∀wral 3061  ∃wrex 3070  ∪ cuni 4908  ‘cfv 6543  (class class class)co 7411  0cc0 11112  1c1 11113  Topctop 22615   Cn ccn 22948  IIcii 24615  PConncpconn 34496

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-iota 6495  df-fv 6551  df-ov 7414  df-pconn 34498

This theorem is referenced by:  pconncn  34501  pconntop  34502  cnpconn  34507  txpconn  34509  ptpconn  34510  indispconn  34511  connpconn  34512  cvxpconn  34519