Metamath Proof Explorer

Theorem cnpconn

Description: An image of a path-connected space is path-connected. (Contributed by Mario Carneiro, 24-Mar-2015)

Ref Expression
Hypothesis cnpconn.2 ⊢ 𝑌 = ∪ 𝐾
Assertion cnpconn ( ( 𝐽 ∈ PConn ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝐾 ∈ PConn )

Proof

Step Hyp Ref Expression
1 cnpconn.2 ⊢ 𝑌 = ∪ 𝐾
2 cntop2 ⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐾 ∈ Top )
3 2 3ad2ant3 ⊢ ( ( 𝐽 ∈ PConn ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝐾 ∈ Top )
4 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
5 4 pconncn ⊢ ( ( 𝐽 ∈ PConn ∧ 𝑢 ∈ ∪ 𝐽 ∧ 𝑣 ∈ ∪ 𝐽 ) → ∃ 𝑔 ∈ ( II Cn 𝐽 ) ( ( 𝑔 ‘ 0 ) = 𝑢 ∧ ( 𝑔 ‘ 1 ) = 𝑣 ) )
6 5 3expb ⊢ ( ( 𝐽 ∈ PConn ∧ ( 𝑢 ∈ ∪ 𝐽 ∧ 𝑣 ∈ ∪ 𝐽 ) ) → ∃ 𝑔 ∈ ( II Cn 𝐽 ) ( ( 𝑔 ‘ 0 ) = 𝑢 ∧ ( 𝑔 ‘ 1 ) = 𝑣 ) )
7 6 3ad2antl1 ⊢ ( ( ( 𝐽 ∈ PConn ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑢 ∈ ∪ 𝐽 ∧ 𝑣 ∈ ∪ 𝐽 ) ) → ∃ 𝑔 ∈ ( II Cn 𝐽 ) ( ( 𝑔 ‘ 0 ) = 𝑢 ∧ ( 𝑔 ‘ 1 ) = 𝑣 ) )
8 simprl ⊢ ( ( ( ( 𝐽 ∈ PConn ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑢 ∈ ∪ 𝐽 ∧ 𝑣 ∈ ∪ 𝐽 ) ) ∧ ( 𝑔 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑔 ‘ 0 ) = 𝑢 ∧ ( 𝑔 ‘ 1 ) = 𝑣 ) ) ) → 𝑔 ∈ ( II Cn 𝐽 ) )
9 simpll3 ⊢ ( ( ( ( 𝐽 ∈ PConn ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑢 ∈ ∪ 𝐽 ∧ 𝑣 ∈ ∪ 𝐽 ) ) ∧ ( 𝑔 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑔 ‘ 0 ) = 𝑢 ∧ ( 𝑔 ‘ 1 ) = 𝑣 ) ) ) → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
10 cnco ⊢ ( ( 𝑔 ∈ ( II Cn 𝐽 ) ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → ( 𝐹 ∘ 𝑔 ) ∈ ( II Cn 𝐾 ) )
11 8 9 10 syl2anc ⊢ ( ( ( ( 𝐽 ∈ PConn ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑢 ∈ ∪ 𝐽 ∧ 𝑣 ∈ ∪ 𝐽 ) ) ∧ ( 𝑔 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑔 ‘ 0 ) = 𝑢 ∧ ( 𝑔 ‘ 1 ) = 𝑣 ) ) ) → ( 𝐹 ∘ 𝑔 ) ∈ ( II Cn 𝐾 ) )
12 iiuni ⊢ ( 0 [,] 1 ) = ∪ II
13 12 4 cnf ⊢ ( 𝑔 ∈ ( II Cn 𝐽 ) → 𝑔 : ( 0 [,] 1 ) ⟶ ∪ 𝐽 )
14 8 13 syl ⊢ ( ( ( ( 𝐽 ∈ PConn ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑢 ∈ ∪ 𝐽 ∧ 𝑣 ∈ ∪ 𝐽 ) ) ∧ ( 𝑔 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑔 ‘ 0 ) = 𝑢 ∧ ( 𝑔 ‘ 1 ) = 𝑣 ) ) ) → 𝑔 : ( 0 [,] 1 ) ⟶ ∪ 𝐽 )
15 0elunit ⊢ 0 ∈ ( 0 [,] 1 )
16 fvco3 ⊢ ( ( 𝑔 : ( 0 [,] 1 ) ⟶ ∪ 𝐽 ∧ 0 ∈ ( 0 [,] 1 ) ) → ( ( 𝐹 ∘ 𝑔 ) ‘ 0 ) = ( 𝐹 ‘ ( 𝑔 ‘ 0 ) ) )
17 14 15 16 sylancl ⊢ ( ( ( ( 𝐽 ∈ PConn ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑢 ∈ ∪ 𝐽 ∧ 𝑣 ∈ ∪ 𝐽 ) ) ∧ ( 𝑔 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑔 ‘ 0 ) = 𝑢 ∧ ( 𝑔 ‘ 1 ) = 𝑣 ) ) ) → ( ( 𝐹 ∘ 𝑔 ) ‘ 0 ) = ( 𝐹 ‘ ( 𝑔 ‘ 0 ) ) )
18 simprrl ⊢ ( ( ( ( 𝐽 ∈ PConn ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑢 ∈ ∪ 𝐽 ∧ 𝑣 ∈ ∪ 𝐽 ) ) ∧ ( 𝑔 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑔 ‘ 0 ) = 𝑢 ∧ ( 𝑔 ‘ 1 ) = 𝑣 ) ) ) → ( 𝑔 ‘ 0 ) = 𝑢 )
19 18 fveq2d ⊢ ( ( ( ( 𝐽 ∈ PConn ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑢 ∈ ∪ 𝐽 ∧ 𝑣 ∈ ∪ 𝐽 ) ) ∧ ( 𝑔 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑔 ‘ 0 ) = 𝑢 ∧ ( 𝑔 ‘ 1 ) = 𝑣 ) ) ) → ( 𝐹 ‘ ( 𝑔 ‘ 0 ) ) = ( 𝐹 ‘ 𝑢 ) )
20 17 19 eqtrd ⊢ ( ( ( ( 𝐽 ∈ PConn ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑢 ∈ ∪ 𝐽 ∧ 𝑣 ∈ ∪ 𝐽 ) ) ∧ ( 𝑔 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑔 ‘ 0 ) = 𝑢 ∧ ( 𝑔 ‘ 1 ) = 𝑣 ) ) ) → ( ( 𝐹 ∘ 𝑔 ) ‘ 0 ) = ( 𝐹 ‘ 𝑢 ) )
21 1elunit ⊢ 1 ∈ ( 0 [,] 1 )
22 fvco3 ⊢ ( ( 𝑔 : ( 0 [,] 1 ) ⟶ ∪ 𝐽 ∧ 1 ∈ ( 0 [,] 1 ) ) → ( ( 𝐹 ∘ 𝑔 ) ‘ 1 ) = ( 𝐹 ‘ ( 𝑔 ‘ 1 ) ) )
23 14 21 22 sylancl ⊢ ( ( ( ( 𝐽 ∈ PConn ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑢 ∈ ∪ 𝐽 ∧ 𝑣 ∈ ∪ 𝐽 ) ) ∧ ( 𝑔 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑔 ‘ 0 ) = 𝑢 ∧ ( 𝑔 ‘ 1 ) = 𝑣 ) ) ) → ( ( 𝐹 ∘ 𝑔 ) ‘ 1 ) = ( 𝐹 ‘ ( 𝑔 ‘ 1 ) ) )
24 simprrr ⊢ ( ( ( ( 𝐽 ∈ PConn ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑢 ∈ ∪ 𝐽 ∧ 𝑣 ∈ ∪ 𝐽 ) ) ∧ ( 𝑔 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑔 ‘ 0 ) = 𝑢 ∧ ( 𝑔 ‘ 1 ) = 𝑣 ) ) ) → ( 𝑔 ‘ 1 ) = 𝑣 )
25 24 fveq2d ⊢ ( ( ( ( 𝐽 ∈ PConn ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑢 ∈ ∪ 𝐽 ∧ 𝑣 ∈ ∪ 𝐽 ) ) ∧ ( 𝑔 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑔 ‘ 0 ) = 𝑢 ∧ ( 𝑔 ‘ 1 ) = 𝑣 ) ) ) → ( 𝐹 ‘ ( 𝑔 ‘ 1 ) ) = ( 𝐹 ‘ 𝑣 ) )
26 23 25 eqtrd ⊢ ( ( ( ( 𝐽 ∈ PConn ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑢 ∈ ∪ 𝐽 ∧ 𝑣 ∈ ∪ 𝐽 ) ) ∧ ( 𝑔 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑔 ‘ 0 ) = 𝑢 ∧ ( 𝑔 ‘ 1 ) = 𝑣 ) ) ) → ( ( 𝐹 ∘ 𝑔 ) ‘ 1 ) = ( 𝐹 ‘ 𝑣 ) )
27 fveq1 ⊢ ( 𝑓 = ( 𝐹 ∘ 𝑔 ) → ( 𝑓 ‘ 0 ) = ( ( 𝐹 ∘ 𝑔 ) ‘ 0 ) )
28 27 eqeq1d ⊢ ( 𝑓 = ( 𝐹 ∘ 𝑔 ) → ( ( 𝑓 ‘ 0 ) = ( 𝐹 ‘ 𝑢 ) ↔ ( ( 𝐹 ∘ 𝑔 ) ‘ 0 ) = ( 𝐹 ‘ 𝑢 ) ) )
29 fveq1 ⊢ ( 𝑓 = ( 𝐹 ∘ 𝑔 ) → ( 𝑓 ‘ 1 ) = ( ( 𝐹 ∘ 𝑔 ) ‘ 1 ) )
30 29 eqeq1d ⊢ ( 𝑓 = ( 𝐹 ∘ 𝑔 ) → ( ( 𝑓 ‘ 1 ) = ( 𝐹 ‘ 𝑣 ) ↔ ( ( 𝐹 ∘ 𝑔 ) ‘ 1 ) = ( 𝐹 ‘ 𝑣 ) ) )
31 28 30 anbi12d ⊢ ( 𝑓 = ( 𝐹 ∘ 𝑔 ) → ( ( ( 𝑓 ‘ 0 ) = ( 𝐹 ‘ 𝑢 ) ∧ ( 𝑓 ‘ 1 ) = ( 𝐹 ‘ 𝑣 ) ) ↔ ( ( ( 𝐹 ∘ 𝑔 ) ‘ 0 ) = ( 𝐹 ‘ 𝑢 ) ∧ ( ( 𝐹 ∘ 𝑔 ) ‘ 1 ) = ( 𝐹 ‘ 𝑣 ) ) ) )
32 31 rspcev ⊢ ( ( ( 𝐹 ∘ 𝑔 ) ∈ ( II Cn 𝐾 ) ∧ ( ( ( 𝐹 ∘ 𝑔 ) ‘ 0 ) = ( 𝐹 ‘ 𝑢 ) ∧ ( ( 𝐹 ∘ 𝑔 ) ‘ 1 ) = ( 𝐹 ‘ 𝑣 ) ) ) → ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = ( 𝐹 ‘ 𝑢 ) ∧ ( 𝑓 ‘ 1 ) = ( 𝐹 ‘ 𝑣 ) ) )
33 11 20 26 32 syl12anc ⊢ ( ( ( ( 𝐽 ∈ PConn ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑢 ∈ ∪ 𝐽 ∧ 𝑣 ∈ ∪ 𝐽 ) ) ∧ ( 𝑔 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑔 ‘ 0 ) = 𝑢 ∧ ( 𝑔 ‘ 1 ) = 𝑣 ) ) ) → ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = ( 𝐹 ‘ 𝑢 ) ∧ ( 𝑓 ‘ 1 ) = ( 𝐹 ‘ 𝑣 ) ) )
34 7 33 rexlimddv ⊢ ( ( ( 𝐽 ∈ PConn ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑢 ∈ ∪ 𝐽 ∧ 𝑣 ∈ ∪ 𝐽 ) ) → ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = ( 𝐹 ‘ 𝑢 ) ∧ ( 𝑓 ‘ 1 ) = ( 𝐹 ‘ 𝑣 ) ) )
35 34 ralrimivva ⊢ ( ( 𝐽 ∈ PConn ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → ∀ 𝑢 ∈ ∪ 𝐽 ∀ 𝑣 ∈ ∪ 𝐽 ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = ( 𝐹 ‘ 𝑢 ) ∧ ( 𝑓 ‘ 1 ) = ( 𝐹 ‘ 𝑣 ) ) )
36 4 1 cnf ⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐹 : ∪ 𝐽 ⟶ 𝑌 )
37 36 3ad2ant3 ⊢ ( ( 𝐽 ∈ PConn ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝐹 : ∪ 𝐽 ⟶ 𝑌 )
38 forn ⊢ ( 𝐹 : 𝑋 –onto→ 𝑌 → ran 𝐹 = 𝑌 )
39 38 3ad2ant2 ⊢ ( ( 𝐽 ∈ PConn ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → ran 𝐹 = 𝑌 )
40 dffo2 ⊢ ( 𝐹 : ∪ 𝐽 –onto→ 𝑌 ↔ ( 𝐹 : ∪ 𝐽 ⟶ 𝑌 ∧ ran 𝐹 = 𝑌 ) )
41 37 39 40 sylanbrc ⊢ ( ( 𝐽 ∈ PConn ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝐹 : ∪ 𝐽 –onto→ 𝑌 )
42 eqeq2 ⊢ ( ( 𝐹 ‘ 𝑣 ) = 𝑦 → ( ( 𝑓 ‘ 1 ) = ( 𝐹 ‘ 𝑣 ) ↔ ( 𝑓 ‘ 1 ) = 𝑦 ) )
43 42 anbi2d ⊢ ( ( 𝐹 ‘ 𝑣 ) = 𝑦 → ( ( ( 𝑓 ‘ 0 ) = ( 𝐹 ‘ 𝑢 ) ∧ ( 𝑓 ‘ 1 ) = ( 𝐹 ‘ 𝑣 ) ) ↔ ( ( 𝑓 ‘ 0 ) = ( 𝐹 ‘ 𝑢 ) ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ) )
44 43 rexbidv ⊢ ( ( 𝐹 ‘ 𝑣 ) = 𝑦 → ( ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = ( 𝐹 ‘ 𝑢 ) ∧ ( 𝑓 ‘ 1 ) = ( 𝐹 ‘ 𝑣 ) ) ↔ ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = ( 𝐹 ‘ 𝑢 ) ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ) )
45 44 cbvfo ⊢ ( 𝐹 : ∪ 𝐽 –onto→ 𝑌 → ( ∀ 𝑣 ∈ ∪ 𝐽 ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = ( 𝐹 ‘ 𝑢 ) ∧ ( 𝑓 ‘ 1 ) = ( 𝐹 ‘ 𝑣 ) ) ↔ ∀ 𝑦 ∈ 𝑌 ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = ( 𝐹 ‘ 𝑢 ) ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ) )
46 41 45 syl ⊢ ( ( 𝐽 ∈ PConn ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → ( ∀ 𝑣 ∈ ∪ 𝐽 ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = ( 𝐹 ‘ 𝑢 ) ∧ ( 𝑓 ‘ 1 ) = ( 𝐹 ‘ 𝑣 ) ) ↔ ∀ 𝑦 ∈ 𝑌 ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = ( 𝐹 ‘ 𝑢 ) ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ) )
47 46 ralbidv ⊢ ( ( 𝐽 ∈ PConn ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → ( ∀ 𝑢 ∈ ∪ 𝐽 ∀ 𝑣 ∈ ∪ 𝐽 ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = ( 𝐹 ‘ 𝑢 ) ∧ ( 𝑓 ‘ 1 ) = ( 𝐹 ‘ 𝑣 ) ) ↔ ∀ 𝑢 ∈ ∪ 𝐽 ∀ 𝑦 ∈ 𝑌 ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = ( 𝐹 ‘ 𝑢 ) ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ) )
48 35 47 mpbid ⊢ ( ( 𝐽 ∈ PConn ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → ∀ 𝑢 ∈ ∪ 𝐽 ∀ 𝑦 ∈ 𝑌 ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = ( 𝐹 ‘ 𝑢 ) ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) )
49 eqeq2 ⊢ ( ( 𝐹 ‘ 𝑢 ) = 𝑥 → ( ( 𝑓 ‘ 0 ) = ( 𝐹 ‘ 𝑢 ) ↔ ( 𝑓 ‘ 0 ) = 𝑥 ) )
50 49 anbi1d ⊢ ( ( 𝐹 ‘ 𝑢 ) = 𝑥 → ( ( ( 𝑓 ‘ 0 ) = ( 𝐹 ‘ 𝑢 ) ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ↔ ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ) )
51 50 rexbidv ⊢ ( ( 𝐹 ‘ 𝑢 ) = 𝑥 → ( ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = ( 𝐹 ‘ 𝑢 ) ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ↔ ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ) )
52 51 ralbidv ⊢ ( ( 𝐹 ‘ 𝑢 ) = 𝑥 → ( ∀ 𝑦 ∈ 𝑌 ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = ( 𝐹 ‘ 𝑢 ) ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ↔ ∀ 𝑦 ∈ 𝑌 ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ) )
53 52 cbvfo ⊢ ( 𝐹 : ∪ 𝐽 –onto→ 𝑌 → ( ∀ 𝑢 ∈ ∪ 𝐽 ∀ 𝑦 ∈ 𝑌 ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = ( 𝐹 ‘ 𝑢 ) ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ↔ ∀ 𝑥 ∈ 𝑌 ∀ 𝑦 ∈ 𝑌 ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ) )
54 41 53 syl ⊢ ( ( 𝐽 ∈ PConn ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → ( ∀ 𝑢 ∈ ∪ 𝐽 ∀ 𝑦 ∈ 𝑌 ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = ( 𝐹 ‘ 𝑢 ) ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ↔ ∀ 𝑥 ∈ 𝑌 ∀ 𝑦 ∈ 𝑌 ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ) )
55 48 54 mpbid ⊢ ( ( 𝐽 ∈ PConn ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → ∀ 𝑥 ∈ 𝑌 ∀ 𝑦 ∈ 𝑌 ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) )
56 1 ispconn ⊢ ( 𝐾 ∈ PConn ↔ ( 𝐾 ∈ Top ∧ ∀ 𝑥 ∈ 𝑌 ∀ 𝑦 ∈ 𝑌 ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ) )
57 3 55 56 sylanbrc ⊢ ( ( 𝐽 ∈ PConn ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝐾 ∈ PConn )