Metamath Proof Explorer

Theorem txpconn

Description: The topological product of two path-connected spaces is path-connected. (Contributed by Mario Carneiro, 12-Feb-2015)

Ref Expression
Assertion txpconn ( ( 𝑅 ∈ PConn ∧ 𝑆 ∈ PConn ) → ( 𝑅 ×t 𝑆 ) ∈ PConn )

Proof

Step Hyp Ref Expression
1 pconntop ⊢ ( 𝑅 ∈ PConn → 𝑅 ∈ Top )
2 pconntop ⊢ ( 𝑆 ∈ PConn → 𝑆 ∈ Top )
3 txtop ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( 𝑅 ×t 𝑆 ) ∈ Top )
4 1 2 3 syl2an ⊢ ( ( 𝑅 ∈ PConn ∧ 𝑆 ∈ PConn ) → ( 𝑅 ×t 𝑆 ) ∈ Top )
5 an6 ⊢ ( ( ( 𝑅 ∈ PConn ∧ 𝑥 ∈ ∪ 𝑅 ∧ 𝑧 ∈ ∪ 𝑅 ) ∧ ( 𝑆 ∈ PConn ∧ 𝑦 ∈ ∪ 𝑆 ∧ 𝑤 ∈ ∪ 𝑆 ) ) ↔ ( ( 𝑅 ∈ PConn ∧ 𝑆 ∈ PConn ) ∧ ( 𝑥 ∈ ∪ 𝑅 ∧ 𝑦 ∈ ∪ 𝑆 ) ∧ ( 𝑧 ∈ ∪ 𝑅 ∧ 𝑤 ∈ ∪ 𝑆 ) ) )
6 eqid ⊢ ∪ 𝑅 = ∪ 𝑅
7 6 pconncn ⊢ ( ( 𝑅 ∈ PConn ∧ 𝑥 ∈ ∪ 𝑅 ∧ 𝑧 ∈ ∪ 𝑅 ) → ∃ 𝑔 ∈ ( II Cn 𝑅 ) ( ( 𝑔 ‘ 0 ) = 𝑥 ∧ ( 𝑔 ‘ 1 ) = 𝑧 ) )
8 eqid ⊢ ∪ 𝑆 = ∪ 𝑆
9 8 pconncn ⊢ ( ( 𝑆 ∈ PConn ∧ 𝑦 ∈ ∪ 𝑆 ∧ 𝑤 ∈ ∪ 𝑆 ) → ∃ ℎ ∈ ( II Cn 𝑆 ) ( ( ℎ ‘ 0 ) = 𝑦 ∧ ( ℎ ‘ 1 ) = 𝑤 ) )
10 7 9 anim12i ⊢ ( ( ( 𝑅 ∈ PConn ∧ 𝑥 ∈ ∪ 𝑅 ∧ 𝑧 ∈ ∪ 𝑅 ) ∧ ( 𝑆 ∈ PConn ∧ 𝑦 ∈ ∪ 𝑆 ∧ 𝑤 ∈ ∪ 𝑆 ) ) → ( ∃ 𝑔 ∈ ( II Cn 𝑅 ) ( ( 𝑔 ‘ 0 ) = 𝑥 ∧ ( 𝑔 ‘ 1 ) = 𝑧 ) ∧ ∃ ℎ ∈ ( II Cn 𝑆 ) ( ( ℎ ‘ 0 ) = 𝑦 ∧ ( ℎ ‘ 1 ) = 𝑤 ) ) )
11 5 10 sylbir ⊢ ( ( ( 𝑅 ∈ PConn ∧ 𝑆 ∈ PConn ) ∧ ( 𝑥 ∈ ∪ 𝑅 ∧ 𝑦 ∈ ∪ 𝑆 ) ∧ ( 𝑧 ∈ ∪ 𝑅 ∧ 𝑤 ∈ ∪ 𝑆 ) ) → ( ∃ 𝑔 ∈ ( II Cn 𝑅 ) ( ( 𝑔 ‘ 0 ) = 𝑥 ∧ ( 𝑔 ‘ 1 ) = 𝑧 ) ∧ ∃ ℎ ∈ ( II Cn 𝑆 ) ( ( ℎ ‘ 0 ) = 𝑦 ∧ ( ℎ ‘ 1 ) = 𝑤 ) ) )
12 reeanv ⊢ ( ∃ 𝑔 ∈ ( II Cn 𝑅 ) ∃ ℎ ∈ ( II Cn 𝑆 ) ( ( ( 𝑔 ‘ 0 ) = 𝑥 ∧ ( 𝑔 ‘ 1 ) = 𝑧 ) ∧ ( ( ℎ ‘ 0 ) = 𝑦 ∧ ( ℎ ‘ 1 ) = 𝑤 ) ) ↔ ( ∃ 𝑔 ∈ ( II Cn 𝑅 ) ( ( 𝑔 ‘ 0 ) = 𝑥 ∧ ( 𝑔 ‘ 1 ) = 𝑧 ) ∧ ∃ ℎ ∈ ( II Cn 𝑆 ) ( ( ℎ ‘ 0 ) = 𝑦 ∧ ( ℎ ‘ 1 ) = 𝑤 ) ) )
13 11 12 sylibr ⊢ ( ( ( 𝑅 ∈ PConn ∧ 𝑆 ∈ PConn ) ∧ ( 𝑥 ∈ ∪ 𝑅 ∧ 𝑦 ∈ ∪ 𝑆 ) ∧ ( 𝑧 ∈ ∪ 𝑅 ∧ 𝑤 ∈ ∪ 𝑆 ) ) → ∃ 𝑔 ∈ ( II Cn 𝑅 ) ∃ ℎ ∈ ( II Cn 𝑆 ) ( ( ( 𝑔 ‘ 0 ) = 𝑥 ∧ ( 𝑔 ‘ 1 ) = 𝑧 ) ∧ ( ( ℎ ‘ 0 ) = 𝑦 ∧ ( ℎ ‘ 1 ) = 𝑤 ) ) )
14 iiuni ⊢ ( 0 [,] 1 ) = ∪ II
15 eqid ⊢ ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ⟨ ( 𝑔 ‘ 𝑡 ) , ( ℎ ‘ 𝑡 ) ⟩ ) = ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ⟨ ( 𝑔 ‘ 𝑡 ) , ( ℎ ‘ 𝑡 ) ⟩ )
16 14 15 txcnmpt ⊢ ( ( 𝑔 ∈ ( II Cn 𝑅 ) ∧ ℎ ∈ ( II Cn 𝑆 ) ) → ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ⟨ ( 𝑔 ‘ 𝑡 ) , ( ℎ ‘ 𝑡 ) ⟩ ) ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) )
17 16 ad2antrl ⊢ ( ( ( ( 𝑅 ∈ PConn ∧ 𝑆 ∈ PConn ) ∧ ( 𝑥 ∈ ∪ 𝑅 ∧ 𝑦 ∈ ∪ 𝑆 ) ∧ ( 𝑧 ∈ ∪ 𝑅 ∧ 𝑤 ∈ ∪ 𝑆 ) ) ∧ ( ( 𝑔 ∈ ( II Cn 𝑅 ) ∧ ℎ ∈ ( II Cn 𝑆 ) ) ∧ ( ( ( 𝑔 ‘ 0 ) = 𝑥 ∧ ( 𝑔 ‘ 1 ) = 𝑧 ) ∧ ( ( ℎ ‘ 0 ) = 𝑦 ∧ ( ℎ ‘ 1 ) = 𝑤 ) ) ) ) → ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ⟨ ( 𝑔 ‘ 𝑡 ) , ( ℎ ‘ 𝑡 ) ⟩ ) ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) )
18 0elunit ⊢ 0 ∈ ( 0 [,] 1 )
19 fveq2 ⊢ ( 𝑡 = 0 → ( 𝑔 ‘ 𝑡 ) = ( 𝑔 ‘ 0 ) )
20 fveq2 ⊢ ( 𝑡 = 0 → ( ℎ ‘ 𝑡 ) = ( ℎ ‘ 0 ) )
21 19 20 opeq12d ⊢ ( 𝑡 = 0 → ⟨ ( 𝑔 ‘ 𝑡 ) , ( ℎ ‘ 𝑡 ) ⟩ = ⟨ ( 𝑔 ‘ 0 ) , ( ℎ ‘ 0 ) ⟩ )
22 opex ⊢ ⟨ ( 𝑔 ‘ 0 ) , ( ℎ ‘ 0 ) ⟩ ∈ V
23 21 15 22 fvmpt ⊢ ( 0 ∈ ( 0 [,] 1 ) → ( ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ⟨ ( 𝑔 ‘ 𝑡 ) , ( ℎ ‘ 𝑡 ) ⟩ ) ‘ 0 ) = ⟨ ( 𝑔 ‘ 0 ) , ( ℎ ‘ 0 ) ⟩ )
24 18 23 ax-mp ⊢ ( ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ⟨ ( 𝑔 ‘ 𝑡 ) , ( ℎ ‘ 𝑡 ) ⟩ ) ‘ 0 ) = ⟨ ( 𝑔 ‘ 0 ) , ( ℎ ‘ 0 ) ⟩
25 simprrl ⊢ ( ( ( ( 𝑅 ∈ PConn ∧ 𝑆 ∈ PConn ) ∧ ( 𝑥 ∈ ∪ 𝑅 ∧ 𝑦 ∈ ∪ 𝑆 ) ∧ ( 𝑧 ∈ ∪ 𝑅 ∧ 𝑤 ∈ ∪ 𝑆 ) ) ∧ ( ( 𝑔 ∈ ( II Cn 𝑅 ) ∧ ℎ ∈ ( II Cn 𝑆 ) ) ∧ ( ( ( 𝑔 ‘ 0 ) = 𝑥 ∧ ( 𝑔 ‘ 1 ) = 𝑧 ) ∧ ( ( ℎ ‘ 0 ) = 𝑦 ∧ ( ℎ ‘ 1 ) = 𝑤 ) ) ) ) → ( ( 𝑔 ‘ 0 ) = 𝑥 ∧ ( 𝑔 ‘ 1 ) = 𝑧 ) )
26 25 simpld ⊢ ( ( ( ( 𝑅 ∈ PConn ∧ 𝑆 ∈ PConn ) ∧ ( 𝑥 ∈ ∪ 𝑅 ∧ 𝑦 ∈ ∪ 𝑆 ) ∧ ( 𝑧 ∈ ∪ 𝑅 ∧ 𝑤 ∈ ∪ 𝑆 ) ) ∧ ( ( 𝑔 ∈ ( II Cn 𝑅 ) ∧ ℎ ∈ ( II Cn 𝑆 ) ) ∧ ( ( ( 𝑔 ‘ 0 ) = 𝑥 ∧ ( 𝑔 ‘ 1 ) = 𝑧 ) ∧ ( ( ℎ ‘ 0 ) = 𝑦 ∧ ( ℎ ‘ 1 ) = 𝑤 ) ) ) ) → ( 𝑔 ‘ 0 ) = 𝑥 )
27 simprrr ⊢ ( ( ( ( 𝑅 ∈ PConn ∧ 𝑆 ∈ PConn ) ∧ ( 𝑥 ∈ ∪ 𝑅 ∧ 𝑦 ∈ ∪ 𝑆 ) ∧ ( 𝑧 ∈ ∪ 𝑅 ∧ 𝑤 ∈ ∪ 𝑆 ) ) ∧ ( ( 𝑔 ∈ ( II Cn 𝑅 ) ∧ ℎ ∈ ( II Cn 𝑆 ) ) ∧ ( ( ( 𝑔 ‘ 0 ) = 𝑥 ∧ ( 𝑔 ‘ 1 ) = 𝑧 ) ∧ ( ( ℎ ‘ 0 ) = 𝑦 ∧ ( ℎ ‘ 1 ) = 𝑤 ) ) ) ) → ( ( ℎ ‘ 0 ) = 𝑦 ∧ ( ℎ ‘ 1 ) = 𝑤 ) )
28 27 simpld ⊢ ( ( ( ( 𝑅 ∈ PConn ∧ 𝑆 ∈ PConn ) ∧ ( 𝑥 ∈ ∪ 𝑅 ∧ 𝑦 ∈ ∪ 𝑆 ) ∧ ( 𝑧 ∈ ∪ 𝑅 ∧ 𝑤 ∈ ∪ 𝑆 ) ) ∧ ( ( 𝑔 ∈ ( II Cn 𝑅 ) ∧ ℎ ∈ ( II Cn 𝑆 ) ) ∧ ( ( ( 𝑔 ‘ 0 ) = 𝑥 ∧ ( 𝑔 ‘ 1 ) = 𝑧 ) ∧ ( ( ℎ ‘ 0 ) = 𝑦 ∧ ( ℎ ‘ 1 ) = 𝑤 ) ) ) ) → ( ℎ ‘ 0 ) = 𝑦 )
29 26 28 opeq12d ⊢ ( ( ( ( 𝑅 ∈ PConn ∧ 𝑆 ∈ PConn ) ∧ ( 𝑥 ∈ ∪ 𝑅 ∧ 𝑦 ∈ ∪ 𝑆 ) ∧ ( 𝑧 ∈ ∪ 𝑅 ∧ 𝑤 ∈ ∪ 𝑆 ) ) ∧ ( ( 𝑔 ∈ ( II Cn 𝑅 ) ∧ ℎ ∈ ( II Cn 𝑆 ) ) ∧ ( ( ( 𝑔 ‘ 0 ) = 𝑥 ∧ ( 𝑔 ‘ 1 ) = 𝑧 ) ∧ ( ( ℎ ‘ 0 ) = 𝑦 ∧ ( ℎ ‘ 1 ) = 𝑤 ) ) ) ) → ⟨ ( 𝑔 ‘ 0 ) , ( ℎ ‘ 0 ) ⟩ = ⟨ 𝑥 , 𝑦 ⟩ )
30 24 29 eqtrid ⊢ ( ( ( ( 𝑅 ∈ PConn ∧ 𝑆 ∈ PConn ) ∧ ( 𝑥 ∈ ∪ 𝑅 ∧ 𝑦 ∈ ∪ 𝑆 ) ∧ ( 𝑧 ∈ ∪ 𝑅 ∧ 𝑤 ∈ ∪ 𝑆 ) ) ∧ ( ( 𝑔 ∈ ( II Cn 𝑅 ) ∧ ℎ ∈ ( II Cn 𝑆 ) ) ∧ ( ( ( 𝑔 ‘ 0 ) = 𝑥 ∧ ( 𝑔 ‘ 1 ) = 𝑧 ) ∧ ( ( ℎ ‘ 0 ) = 𝑦 ∧ ( ℎ ‘ 1 ) = 𝑤 ) ) ) ) → ( ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ⟨ ( 𝑔 ‘ 𝑡 ) , ( ℎ ‘ 𝑡 ) ⟩ ) ‘ 0 ) = ⟨ 𝑥 , 𝑦 ⟩ )
31 1elunit ⊢ 1 ∈ ( 0 [,] 1 )
32 fveq2 ⊢ ( 𝑡 = 1 → ( 𝑔 ‘ 𝑡 ) = ( 𝑔 ‘ 1 ) )
33 fveq2 ⊢ ( 𝑡 = 1 → ( ℎ ‘ 𝑡 ) = ( ℎ ‘ 1 ) )
34 32 33 opeq12d ⊢ ( 𝑡 = 1 → ⟨ ( 𝑔 ‘ 𝑡 ) , ( ℎ ‘ 𝑡 ) ⟩ = ⟨ ( 𝑔 ‘ 1 ) , ( ℎ ‘ 1 ) ⟩ )
35 opex ⊢ ⟨ ( 𝑔 ‘ 1 ) , ( ℎ ‘ 1 ) ⟩ ∈ V
36 34 15 35 fvmpt ⊢ ( 1 ∈ ( 0 [,] 1 ) → ( ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ⟨ ( 𝑔 ‘ 𝑡 ) , ( ℎ ‘ 𝑡 ) ⟩ ) ‘ 1 ) = ⟨ ( 𝑔 ‘ 1 ) , ( ℎ ‘ 1 ) ⟩ )
37 31 36 ax-mp ⊢ ( ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ⟨ ( 𝑔 ‘ 𝑡 ) , ( ℎ ‘ 𝑡 ) ⟩ ) ‘ 1 ) = ⟨ ( 𝑔 ‘ 1 ) , ( ℎ ‘ 1 ) ⟩
38 25 simprd ⊢ ( ( ( ( 𝑅 ∈ PConn ∧ 𝑆 ∈ PConn ) ∧ ( 𝑥 ∈ ∪ 𝑅 ∧ 𝑦 ∈ ∪ 𝑆 ) ∧ ( 𝑧 ∈ ∪ 𝑅 ∧ 𝑤 ∈ ∪ 𝑆 ) ) ∧ ( ( 𝑔 ∈ ( II Cn 𝑅 ) ∧ ℎ ∈ ( II Cn 𝑆 ) ) ∧ ( ( ( 𝑔 ‘ 0 ) = 𝑥 ∧ ( 𝑔 ‘ 1 ) = 𝑧 ) ∧ ( ( ℎ ‘ 0 ) = 𝑦 ∧ ( ℎ ‘ 1 ) = 𝑤 ) ) ) ) → ( 𝑔 ‘ 1 ) = 𝑧 )
39 27 simprd ⊢ ( ( ( ( 𝑅 ∈ PConn ∧ 𝑆 ∈ PConn ) ∧ ( 𝑥 ∈ ∪ 𝑅 ∧ 𝑦 ∈ ∪ 𝑆 ) ∧ ( 𝑧 ∈ ∪ 𝑅 ∧ 𝑤 ∈ ∪ 𝑆 ) ) ∧ ( ( 𝑔 ∈ ( II Cn 𝑅 ) ∧ ℎ ∈ ( II Cn 𝑆 ) ) ∧ ( ( ( 𝑔 ‘ 0 ) = 𝑥 ∧ ( 𝑔 ‘ 1 ) = 𝑧 ) ∧ ( ( ℎ ‘ 0 ) = 𝑦 ∧ ( ℎ ‘ 1 ) = 𝑤 ) ) ) ) → ( ℎ ‘ 1 ) = 𝑤 )
40 38 39 opeq12d ⊢ ( ( ( ( 𝑅 ∈ PConn ∧ 𝑆 ∈ PConn ) ∧ ( 𝑥 ∈ ∪ 𝑅 ∧ 𝑦 ∈ ∪ 𝑆 ) ∧ ( 𝑧 ∈ ∪ 𝑅 ∧ 𝑤 ∈ ∪ 𝑆 ) ) ∧ ( ( 𝑔 ∈ ( II Cn 𝑅 ) ∧ ℎ ∈ ( II Cn 𝑆 ) ) ∧ ( ( ( 𝑔 ‘ 0 ) = 𝑥 ∧ ( 𝑔 ‘ 1 ) = 𝑧 ) ∧ ( ( ℎ ‘ 0 ) = 𝑦 ∧ ( ℎ ‘ 1 ) = 𝑤 ) ) ) ) → ⟨ ( 𝑔 ‘ 1 ) , ( ℎ ‘ 1 ) ⟩ = ⟨ 𝑧 , 𝑤 ⟩ )
41 37 40 eqtrid ⊢ ( ( ( ( 𝑅 ∈ PConn ∧ 𝑆 ∈ PConn ) ∧ ( 𝑥 ∈ ∪ 𝑅 ∧ 𝑦 ∈ ∪ 𝑆 ) ∧ ( 𝑧 ∈ ∪ 𝑅 ∧ 𝑤 ∈ ∪ 𝑆 ) ) ∧ ( ( 𝑔 ∈ ( II Cn 𝑅 ) ∧ ℎ ∈ ( II Cn 𝑆 ) ) ∧ ( ( ( 𝑔 ‘ 0 ) = 𝑥 ∧ ( 𝑔 ‘ 1 ) = 𝑧 ) ∧ ( ( ℎ ‘ 0 ) = 𝑦 ∧ ( ℎ ‘ 1 ) = 𝑤 ) ) ) ) → ( ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ⟨ ( 𝑔 ‘ 𝑡 ) , ( ℎ ‘ 𝑡 ) ⟩ ) ‘ 1 ) = ⟨ 𝑧 , 𝑤 ⟩ )
42 fveq1 ⊢ ( 𝑓 = ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ⟨ ( 𝑔 ‘ 𝑡 ) , ( ℎ ‘ 𝑡 ) ⟩ ) → ( 𝑓 ‘ 0 ) = ( ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ⟨ ( 𝑔 ‘ 𝑡 ) , ( ℎ ‘ 𝑡 ) ⟩ ) ‘ 0 ) )
43 42 eqeq1d ⊢ ( 𝑓 = ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ⟨ ( 𝑔 ‘ 𝑡 ) , ( ℎ ‘ 𝑡 ) ⟩ ) → ( ( 𝑓 ‘ 0 ) = ⟨ 𝑥 , 𝑦 ⟩ ↔ ( ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ⟨ ( 𝑔 ‘ 𝑡 ) , ( ℎ ‘ 𝑡 ) ⟩ ) ‘ 0 ) = ⟨ 𝑥 , 𝑦 ⟩ ) )
44 fveq1 ⊢ ( 𝑓 = ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ⟨ ( 𝑔 ‘ 𝑡 ) , ( ℎ ‘ 𝑡 ) ⟩ ) → ( 𝑓 ‘ 1 ) = ( ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ⟨ ( 𝑔 ‘ 𝑡 ) , ( ℎ ‘ 𝑡 ) ⟩ ) ‘ 1 ) )
45 44 eqeq1d ⊢ ( 𝑓 = ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ⟨ ( 𝑔 ‘ 𝑡 ) , ( ℎ ‘ 𝑡 ) ⟩ ) → ( ( 𝑓 ‘ 1 ) = ⟨ 𝑧 , 𝑤 ⟩ ↔ ( ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ⟨ ( 𝑔 ‘ 𝑡 ) , ( ℎ ‘ 𝑡 ) ⟩ ) ‘ 1 ) = ⟨ 𝑧 , 𝑤 ⟩ ) )
46 43 45 anbi12d ⊢ ( 𝑓 = ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ⟨ ( 𝑔 ‘ 𝑡 ) , ( ℎ ‘ 𝑡 ) ⟩ ) → ( ( ( 𝑓 ‘ 0 ) = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑓 ‘ 1 ) = ⟨ 𝑧 , 𝑤 ⟩ ) ↔ ( ( ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ⟨ ( 𝑔 ‘ 𝑡 ) , ( ℎ ‘ 𝑡 ) ⟩ ) ‘ 0 ) = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ⟨ ( 𝑔 ‘ 𝑡 ) , ( ℎ ‘ 𝑡 ) ⟩ ) ‘ 1 ) = ⟨ 𝑧 , 𝑤 ⟩ ) ) )
47 46 rspcev ⊢ ( ( ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ⟨ ( 𝑔 ‘ 𝑡 ) , ( ℎ ‘ 𝑡 ) ⟩ ) ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) ∧ ( ( ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ⟨ ( 𝑔 ‘ 𝑡 ) , ( ℎ ‘ 𝑡 ) ⟩ ) ‘ 0 ) = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ⟨ ( 𝑔 ‘ 𝑡 ) , ( ℎ ‘ 𝑡 ) ⟩ ) ‘ 1 ) = ⟨ 𝑧 , 𝑤 ⟩ ) ) → ∃ 𝑓 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) ( ( 𝑓 ‘ 0 ) = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑓 ‘ 1 ) = ⟨ 𝑧 , 𝑤 ⟩ ) )
48 17 30 41 47 syl12anc ⊢ ( ( ( ( 𝑅 ∈ PConn ∧ 𝑆 ∈ PConn ) ∧ ( 𝑥 ∈ ∪ 𝑅 ∧ 𝑦 ∈ ∪ 𝑆 ) ∧ ( 𝑧 ∈ ∪ 𝑅 ∧ 𝑤 ∈ ∪ 𝑆 ) ) ∧ ( ( 𝑔 ∈ ( II Cn 𝑅 ) ∧ ℎ ∈ ( II Cn 𝑆 ) ) ∧ ( ( ( 𝑔 ‘ 0 ) = 𝑥 ∧ ( 𝑔 ‘ 1 ) = 𝑧 ) ∧ ( ( ℎ ‘ 0 ) = 𝑦 ∧ ( ℎ ‘ 1 ) = 𝑤 ) ) ) ) → ∃ 𝑓 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) ( ( 𝑓 ‘ 0 ) = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑓 ‘ 1 ) = ⟨ 𝑧 , 𝑤 ⟩ ) )
49 48 expr ⊢ ( ( ( ( 𝑅 ∈ PConn ∧ 𝑆 ∈ PConn ) ∧ ( 𝑥 ∈ ∪ 𝑅 ∧ 𝑦 ∈ ∪ 𝑆 ) ∧ ( 𝑧 ∈ ∪ 𝑅 ∧ 𝑤 ∈ ∪ 𝑆 ) ) ∧ ( 𝑔 ∈ ( II Cn 𝑅 ) ∧ ℎ ∈ ( II Cn 𝑆 ) ) ) → ( ( ( ( 𝑔 ‘ 0 ) = 𝑥 ∧ ( 𝑔 ‘ 1 ) = 𝑧 ) ∧ ( ( ℎ ‘ 0 ) = 𝑦 ∧ ( ℎ ‘ 1 ) = 𝑤 ) ) → ∃ 𝑓 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) ( ( 𝑓 ‘ 0 ) = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑓 ‘ 1 ) = ⟨ 𝑧 , 𝑤 ⟩ ) ) )
50 49 rexlimdvva ⊢ ( ( ( 𝑅 ∈ PConn ∧ 𝑆 ∈ PConn ) ∧ ( 𝑥 ∈ ∪ 𝑅 ∧ 𝑦 ∈ ∪ 𝑆 ) ∧ ( 𝑧 ∈ ∪ 𝑅 ∧ 𝑤 ∈ ∪ 𝑆 ) ) → ( ∃ 𝑔 ∈ ( II Cn 𝑅 ) ∃ ℎ ∈ ( II Cn 𝑆 ) ( ( ( 𝑔 ‘ 0 ) = 𝑥 ∧ ( 𝑔 ‘ 1 ) = 𝑧 ) ∧ ( ( ℎ ‘ 0 ) = 𝑦 ∧ ( ℎ ‘ 1 ) = 𝑤 ) ) → ∃ 𝑓 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) ( ( 𝑓 ‘ 0 ) = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑓 ‘ 1 ) = ⟨ 𝑧 , 𝑤 ⟩ ) ) )
51 13 50 mpd ⊢ ( ( ( 𝑅 ∈ PConn ∧ 𝑆 ∈ PConn ) ∧ ( 𝑥 ∈ ∪ 𝑅 ∧ 𝑦 ∈ ∪ 𝑆 ) ∧ ( 𝑧 ∈ ∪ 𝑅 ∧ 𝑤 ∈ ∪ 𝑆 ) ) → ∃ 𝑓 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) ( ( 𝑓 ‘ 0 ) = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑓 ‘ 1 ) = ⟨ 𝑧 , 𝑤 ⟩ ) )
52 51 3expa ⊢ ( ( ( ( 𝑅 ∈ PConn ∧ 𝑆 ∈ PConn ) ∧ ( 𝑥 ∈ ∪ 𝑅 ∧ 𝑦 ∈ ∪ 𝑆 ) ) ∧ ( 𝑧 ∈ ∪ 𝑅 ∧ 𝑤 ∈ ∪ 𝑆 ) ) → ∃ 𝑓 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) ( ( 𝑓 ‘ 0 ) = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑓 ‘ 1 ) = ⟨ 𝑧 , 𝑤 ⟩ ) )
53 52 ralrimivva ⊢ ( ( ( 𝑅 ∈ PConn ∧ 𝑆 ∈ PConn ) ∧ ( 𝑥 ∈ ∪ 𝑅 ∧ 𝑦 ∈ ∪ 𝑆 ) ) → ∀ 𝑧 ∈ ∪ 𝑅 ∀ 𝑤 ∈ ∪ 𝑆 ∃ 𝑓 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) ( ( 𝑓 ‘ 0 ) = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑓 ‘ 1 ) = ⟨ 𝑧 , 𝑤 ⟩ ) )
54 53 ralrimivva ⊢ ( ( 𝑅 ∈ PConn ∧ 𝑆 ∈ PConn ) → ∀ 𝑥 ∈ ∪ 𝑅 ∀ 𝑦 ∈ ∪ 𝑆 ∀ 𝑧 ∈ ∪ 𝑅 ∀ 𝑤 ∈ ∪ 𝑆 ∃ 𝑓 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) ( ( 𝑓 ‘ 0 ) = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑓 ‘ 1 ) = ⟨ 𝑧 , 𝑤 ⟩ ) )
55 eqeq2 ⊢ ( 𝑣 = ⟨ 𝑧 , 𝑤 ⟩ → ( ( 𝑓 ‘ 1 ) = 𝑣 ↔ ( 𝑓 ‘ 1 ) = ⟨ 𝑧 , 𝑤 ⟩ ) )
56 55 anbi2d ⊢ ( 𝑣 = ⟨ 𝑧 , 𝑤 ⟩ → ( ( ( 𝑓 ‘ 0 ) = 𝑢 ∧ ( 𝑓 ‘ 1 ) = 𝑣 ) ↔ ( ( 𝑓 ‘ 0 ) = 𝑢 ∧ ( 𝑓 ‘ 1 ) = ⟨ 𝑧 , 𝑤 ⟩ ) ) )
57 56 rexbidv ⊢ ( 𝑣 = ⟨ 𝑧 , 𝑤 ⟩ → ( ∃ 𝑓 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) ( ( 𝑓 ‘ 0 ) = 𝑢 ∧ ( 𝑓 ‘ 1 ) = 𝑣 ) ↔ ∃ 𝑓 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) ( ( 𝑓 ‘ 0 ) = 𝑢 ∧ ( 𝑓 ‘ 1 ) = ⟨ 𝑧 , 𝑤 ⟩ ) ) )
58 57 ralxp ⊢ ( ∀ 𝑣 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∃ 𝑓 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) ( ( 𝑓 ‘ 0 ) = 𝑢 ∧ ( 𝑓 ‘ 1 ) = 𝑣 ) ↔ ∀ 𝑧 ∈ ∪ 𝑅 ∀ 𝑤 ∈ ∪ 𝑆 ∃ 𝑓 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) ( ( 𝑓 ‘ 0 ) = 𝑢 ∧ ( 𝑓 ‘ 1 ) = ⟨ 𝑧 , 𝑤 ⟩ ) )
59 eqeq2 ⊢ ( 𝑢 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 𝑓 ‘ 0 ) = 𝑢 ↔ ( 𝑓 ‘ 0 ) = ⟨ 𝑥 , 𝑦 ⟩ ) )
60 59 anbi1d ⊢ ( 𝑢 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( ( 𝑓 ‘ 0 ) = 𝑢 ∧ ( 𝑓 ‘ 1 ) = ⟨ 𝑧 , 𝑤 ⟩ ) ↔ ( ( 𝑓 ‘ 0 ) = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑓 ‘ 1 ) = ⟨ 𝑧 , 𝑤 ⟩ ) ) )
61 60 rexbidv ⊢ ( 𝑢 = ⟨ 𝑥 , 𝑦 ⟩ → ( ∃ 𝑓 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) ( ( 𝑓 ‘ 0 ) = 𝑢 ∧ ( 𝑓 ‘ 1 ) = ⟨ 𝑧 , 𝑤 ⟩ ) ↔ ∃ 𝑓 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) ( ( 𝑓 ‘ 0 ) = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑓 ‘ 1 ) = ⟨ 𝑧 , 𝑤 ⟩ ) ) )
62 61 2ralbidv ⊢ ( 𝑢 = ⟨ 𝑥 , 𝑦 ⟩ → ( ∀ 𝑧 ∈ ∪ 𝑅 ∀ 𝑤 ∈ ∪ 𝑆 ∃ 𝑓 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) ( ( 𝑓 ‘ 0 ) = 𝑢 ∧ ( 𝑓 ‘ 1 ) = ⟨ 𝑧 , 𝑤 ⟩ ) ↔ ∀ 𝑧 ∈ ∪ 𝑅 ∀ 𝑤 ∈ ∪ 𝑆 ∃ 𝑓 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) ( ( 𝑓 ‘ 0 ) = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑓 ‘ 1 ) = ⟨ 𝑧 , 𝑤 ⟩ ) ) )
63 58 62 syl5bb ⊢ ( 𝑢 = ⟨ 𝑥 , 𝑦 ⟩ → ( ∀ 𝑣 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∃ 𝑓 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) ( ( 𝑓 ‘ 0 ) = 𝑢 ∧ ( 𝑓 ‘ 1 ) = 𝑣 ) ↔ ∀ 𝑧 ∈ ∪ 𝑅 ∀ 𝑤 ∈ ∪ 𝑆 ∃ 𝑓 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) ( ( 𝑓 ‘ 0 ) = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑓 ‘ 1 ) = ⟨ 𝑧 , 𝑤 ⟩ ) ) )
64 63 ralxp ⊢ ( ∀ 𝑢 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∀ 𝑣 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∃ 𝑓 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) ( ( 𝑓 ‘ 0 ) = 𝑢 ∧ ( 𝑓 ‘ 1 ) = 𝑣 ) ↔ ∀ 𝑥 ∈ ∪ 𝑅 ∀ 𝑦 ∈ ∪ 𝑆 ∀ 𝑧 ∈ ∪ 𝑅 ∀ 𝑤 ∈ ∪ 𝑆 ∃ 𝑓 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) ( ( 𝑓 ‘ 0 ) = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑓 ‘ 1 ) = ⟨ 𝑧 , 𝑤 ⟩ ) )
65 54 64 sylibr ⊢ ( ( 𝑅 ∈ PConn ∧ 𝑆 ∈ PConn ) → ∀ 𝑢 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∀ 𝑣 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∃ 𝑓 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) ( ( 𝑓 ‘ 0 ) = 𝑢 ∧ ( 𝑓 ‘ 1 ) = 𝑣 ) )
66 6 8 txuni ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( ∪ 𝑅 × ∪ 𝑆 ) = ∪ ( 𝑅 ×t 𝑆 ) )
67 1 2 66 syl2an ⊢ ( ( 𝑅 ∈ PConn ∧ 𝑆 ∈ PConn ) → ( ∪ 𝑅 × ∪ 𝑆 ) = ∪ ( 𝑅 ×t 𝑆 ) )
68 67 raleqdv ⊢ ( ( 𝑅 ∈ PConn ∧ 𝑆 ∈ PConn ) → ( ∀ 𝑣 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∃ 𝑓 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) ( ( 𝑓 ‘ 0 ) = 𝑢 ∧ ( 𝑓 ‘ 1 ) = 𝑣 ) ↔ ∀ 𝑣 ∈ ∪ ( 𝑅 ×t 𝑆 ) ∃ 𝑓 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) ( ( 𝑓 ‘ 0 ) = 𝑢 ∧ ( 𝑓 ‘ 1 ) = 𝑣 ) ) )
69 67 68 raleqbidv ⊢ ( ( 𝑅 ∈ PConn ∧ 𝑆 ∈ PConn ) → ( ∀ 𝑢 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∀ 𝑣 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∃ 𝑓 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) ( ( 𝑓 ‘ 0 ) = 𝑢 ∧ ( 𝑓 ‘ 1 ) = 𝑣 ) ↔ ∀ 𝑢 ∈ ∪ ( 𝑅 ×t 𝑆 ) ∀ 𝑣 ∈ ∪ ( 𝑅 ×t 𝑆 ) ∃ 𝑓 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) ( ( 𝑓 ‘ 0 ) = 𝑢 ∧ ( 𝑓 ‘ 1 ) = 𝑣 ) ) )
70 65 69 mpbid ⊢ ( ( 𝑅 ∈ PConn ∧ 𝑆 ∈ PConn ) → ∀ 𝑢 ∈ ∪ ( 𝑅 ×t 𝑆 ) ∀ 𝑣 ∈ ∪ ( 𝑅 ×t 𝑆 ) ∃ 𝑓 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) ( ( 𝑓 ‘ 0 ) = 𝑢 ∧ ( 𝑓 ‘ 1 ) = 𝑣 ) )
71 eqid ⊢ ∪ ( 𝑅 ×t 𝑆 ) = ∪ ( 𝑅 ×t 𝑆 )
72 71 ispconn ⊢ ( ( 𝑅 ×t 𝑆 ) ∈ PConn ↔ ( ( 𝑅 ×t 𝑆 ) ∈ Top ∧ ∀ 𝑢 ∈ ∪ ( 𝑅 ×t 𝑆 ) ∀ 𝑣 ∈ ∪ ( 𝑅 ×t 𝑆 ) ∃ 𝑓 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) ( ( 𝑓 ‘ 0 ) = 𝑢 ∧ ( 𝑓 ‘ 1 ) = 𝑣 ) ) )
73 4 70 72 sylanbrc ⊢ ( ( 𝑅 ∈ PConn ∧ 𝑆 ∈ PConn ) → ( 𝑅 ×t 𝑆 ) ∈ PConn )