Step | Hyp | Ref
| Expression |
1 | | sconnpconn 33189 |
. . 3
⊢ (𝑅 ∈ SConn → 𝑅 ∈ PConn) |
2 | | sconnpconn 33189 |
. . 3
⊢ (𝑆 ∈ SConn → 𝑆 ∈ PConn) |
3 | | txpconn 33194 |
. . 3
⊢ ((𝑅 ∈ PConn ∧ 𝑆 ∈ PConn) → (𝑅 ×t 𝑆) ∈ PConn) |
4 | 1, 2, 3 | syl2an 596 |
. 2
⊢ ((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) → (𝑅 ×t 𝑆) ∈ PConn) |
5 | | simpll 764 |
. . . . . . . . 9
⊢ (((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) ∧ (𝑓 ∈ (II Cn (𝑅 ×t 𝑆)) ∧ (𝑓‘0) = (𝑓‘1))) → 𝑅 ∈ SConn) |
6 | | simprl 768 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) ∧ (𝑓 ∈ (II Cn (𝑅 ×t 𝑆)) ∧ (𝑓‘0) = (𝑓‘1))) → 𝑓 ∈ (II Cn (𝑅 ×t 𝑆))) |
7 | | sconntop 33190 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ SConn → 𝑅 ∈ Top) |
8 | 7 | ad2antrr 723 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) ∧ (𝑓 ∈ (II Cn (𝑅 ×t 𝑆)) ∧ (𝑓‘0) = (𝑓‘1))) → 𝑅 ∈ Top) |
9 | | eqid 2738 |
. . . . . . . . . . . . 13
⊢ ∪ 𝑅 =
∪ 𝑅 |
10 | 9 | toptopon 22066 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ Top ↔ 𝑅 ∈ (TopOn‘∪ 𝑅)) |
11 | 8, 10 | sylib 217 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) ∧ (𝑓 ∈ (II Cn (𝑅 ×t 𝑆)) ∧ (𝑓‘0) = (𝑓‘1))) → 𝑅 ∈ (TopOn‘∪ 𝑅)) |
12 | | sconntop 33190 |
. . . . . . . . . . . . 13
⊢ (𝑆 ∈ SConn → 𝑆 ∈ Top) |
13 | 12 | ad2antlr 724 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) ∧ (𝑓 ∈ (II Cn (𝑅 ×t 𝑆)) ∧ (𝑓‘0) = (𝑓‘1))) → 𝑆 ∈ Top) |
14 | | eqid 2738 |
. . . . . . . . . . . . 13
⊢ ∪ 𝑆 =
∪ 𝑆 |
15 | 14 | toptopon 22066 |
. . . . . . . . . . . 12
⊢ (𝑆 ∈ Top ↔ 𝑆 ∈ (TopOn‘∪ 𝑆)) |
16 | 13, 15 | sylib 217 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) ∧ (𝑓 ∈ (II Cn (𝑅 ×t 𝑆)) ∧ (𝑓‘0) = (𝑓‘1))) → 𝑆 ∈ (TopOn‘∪ 𝑆)) |
17 | | tx1cn 22760 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ (TopOn‘∪ 𝑅)
∧ 𝑆 ∈
(TopOn‘∪ 𝑆)) → (1st ↾ (∪ 𝑅
× ∪ 𝑆)) ∈ ((𝑅 ×t 𝑆) Cn 𝑅)) |
18 | 11, 16, 17 | syl2anc 584 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) ∧ (𝑓 ∈ (II Cn (𝑅 ×t 𝑆)) ∧ (𝑓‘0) = (𝑓‘1))) → (1st ↾
(∪ 𝑅 × ∪ 𝑆)) ∈ ((𝑅 ×t 𝑆) Cn 𝑅)) |
19 | | cnco 22417 |
. . . . . . . . . 10
⊢ ((𝑓 ∈ (II Cn (𝑅 ×t 𝑆)) ∧ (1st ↾
(∪ 𝑅 × ∪ 𝑆)) ∈ ((𝑅 ×t 𝑆) Cn 𝑅)) → ((1st ↾ (∪ 𝑅
× ∪ 𝑆)) ∘ 𝑓) ∈ (II Cn 𝑅)) |
20 | 6, 18, 19 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) ∧ (𝑓 ∈ (II Cn (𝑅 ×t 𝑆)) ∧ (𝑓‘0) = (𝑓‘1))) → ((1st ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓) ∈ (II Cn 𝑅)) |
21 | | simprr 770 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) ∧ (𝑓 ∈ (II Cn (𝑅 ×t 𝑆)) ∧ (𝑓‘0) = (𝑓‘1))) → (𝑓‘0) = (𝑓‘1)) |
22 | 21 | fveq2d 6778 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) ∧ (𝑓 ∈ (II Cn (𝑅 ×t 𝑆)) ∧ (𝑓‘0) = (𝑓‘1))) → ((1st ↾
(∪ 𝑅 × ∪ 𝑆))‘(𝑓‘0)) = ((1st ↾ (∪ 𝑅
× ∪ 𝑆))‘(𝑓‘1))) |
23 | | iitopon 24042 |
. . . . . . . . . . . . 13
⊢ II ∈
(TopOn‘(0[,]1)) |
24 | 23 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) ∧ (𝑓 ∈ (II Cn (𝑅 ×t 𝑆)) ∧ (𝑓‘0) = (𝑓‘1))) → II ∈
(TopOn‘(0[,]1))) |
25 | | txtopon 22742 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ (TopOn‘∪ 𝑅)
∧ 𝑆 ∈
(TopOn‘∪ 𝑆)) → (𝑅 ×t 𝑆) ∈ (TopOn‘(∪ 𝑅
× ∪ 𝑆))) |
26 | 11, 16, 25 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) ∧ (𝑓 ∈ (II Cn (𝑅 ×t 𝑆)) ∧ (𝑓‘0) = (𝑓‘1))) → (𝑅 ×t 𝑆) ∈ (TopOn‘(∪ 𝑅
× ∪ 𝑆))) |
27 | | cnf2 22400 |
. . . . . . . . . . . 12
⊢ ((II
∈ (TopOn‘(0[,]1)) ∧ (𝑅 ×t 𝑆) ∈ (TopOn‘(∪ 𝑅
× ∪ 𝑆)) ∧ 𝑓 ∈ (II Cn (𝑅 ×t 𝑆))) → 𝑓:(0[,]1)⟶(∪
𝑅 × ∪ 𝑆)) |
28 | 24, 26, 6, 27 | syl3anc 1370 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) ∧ (𝑓 ∈ (II Cn (𝑅 ×t 𝑆)) ∧ (𝑓‘0) = (𝑓‘1))) → 𝑓:(0[,]1)⟶(∪
𝑅 × ∪ 𝑆)) |
29 | | 0elunit 13201 |
. . . . . . . . . . 11
⊢ 0 ∈
(0[,]1) |
30 | | fvco3 6867 |
. . . . . . . . . . 11
⊢ ((𝑓:(0[,]1)⟶(∪ 𝑅
× ∪ 𝑆) ∧ 0 ∈ (0[,]1)) →
(((1st ↾ (∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘0) = ((1st ↾ (∪ 𝑅
× ∪ 𝑆))‘(𝑓‘0))) |
31 | 28, 29, 30 | sylancl 586 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) ∧ (𝑓 ∈ (II Cn (𝑅 ×t 𝑆)) ∧ (𝑓‘0) = (𝑓‘1))) → (((1st ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘0) = ((1st ↾ (∪ 𝑅
× ∪ 𝑆))‘(𝑓‘0))) |
32 | | 1elunit 13202 |
. . . . . . . . . . 11
⊢ 1 ∈
(0[,]1) |
33 | | fvco3 6867 |
. . . . . . . . . . 11
⊢ ((𝑓:(0[,]1)⟶(∪ 𝑅
× ∪ 𝑆) ∧ 1 ∈ (0[,]1)) →
(((1st ↾ (∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘1) = ((1st ↾ (∪ 𝑅
× ∪ 𝑆))‘(𝑓‘1))) |
34 | 28, 32, 33 | sylancl 586 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) ∧ (𝑓 ∈ (II Cn (𝑅 ×t 𝑆)) ∧ (𝑓‘0) = (𝑓‘1))) → (((1st ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘1) = ((1st ↾ (∪ 𝑅
× ∪ 𝑆))‘(𝑓‘1))) |
35 | 22, 31, 34 | 3eqtr4d 2788 |
. . . . . . . . 9
⊢ (((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) ∧ (𝑓 ∈ (II Cn (𝑅 ×t 𝑆)) ∧ (𝑓‘0) = (𝑓‘1))) → (((1st ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘0) = (((1st ↾ (∪ 𝑅
× ∪ 𝑆)) ∘ 𝑓)‘1)) |
36 | | sconnpht 33191 |
. . . . . . . . 9
⊢ ((𝑅 ∈ SConn ∧
((1st ↾ (∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓) ∈ (II Cn 𝑅) ∧ (((1st ↾ (∪ 𝑅
× ∪ 𝑆)) ∘ 𝑓)‘0) = (((1st ↾ (∪ 𝑅
× ∪ 𝑆)) ∘ 𝑓)‘1)) → ((1st ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)( ≃ph‘𝑅)((0[,]1) ×
{(((1st ↾ (∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘0)})) |
37 | 5, 20, 35, 36 | syl3anc 1370 |
. . . . . . . 8
⊢ (((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) ∧ (𝑓 ∈ (II Cn (𝑅 ×t 𝑆)) ∧ (𝑓‘0) = (𝑓‘1))) → ((1st ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)( ≃ph‘𝑅)((0[,]1) ×
{(((1st ↾ (∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘0)})) |
38 | | isphtpc 24157 |
. . . . . . . 8
⊢
(((1st ↾ (∪ 𝑅 × ∪ 𝑆))
∘ 𝑓)(
≃ph‘𝑅)((0[,]1) × {(((1st ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘0)}) ↔ (((1st ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓) ∈ (II Cn 𝑅) ∧ ((0[,]1) × {(((1st
↾ (∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘0)}) ∈ (II Cn 𝑅) ∧ (((1st ↾ (∪ 𝑅
× ∪ 𝑆)) ∘ 𝑓)(PHtpy‘𝑅)((0[,]1) × {(((1st ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘0)})) ≠ ∅)) |
39 | 37, 38 | sylib 217 |
. . . . . . 7
⊢ (((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) ∧ (𝑓 ∈ (II Cn (𝑅 ×t 𝑆)) ∧ (𝑓‘0) = (𝑓‘1))) → (((1st ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓) ∈ (II Cn 𝑅) ∧ ((0[,]1) × {(((1st
↾ (∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘0)}) ∈ (II Cn 𝑅) ∧ (((1st ↾ (∪ 𝑅
× ∪ 𝑆)) ∘ 𝑓)(PHtpy‘𝑅)((0[,]1) × {(((1st ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘0)})) ≠ ∅)) |
40 | 39 | simp3d 1143 |
. . . . . 6
⊢ (((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) ∧ (𝑓 ∈ (II Cn (𝑅 ×t 𝑆)) ∧ (𝑓‘0) = (𝑓‘1))) → (((1st ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)(PHtpy‘𝑅)((0[,]1) × {(((1st ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘0)})) ≠ ∅) |
41 | | n0 4280 |
. . . . . 6
⊢
((((1st ↾ (∪ 𝑅 × ∪ 𝑆))
∘ 𝑓)(PHtpy‘𝑅)((0[,]1) × {(((1st ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘0)})) ≠ ∅ ↔
∃𝑔 𝑔 ∈ (((1st ↾ (∪ 𝑅
× ∪ 𝑆)) ∘ 𝑓)(PHtpy‘𝑅)((0[,]1) × {(((1st ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘0)}))) |
42 | 40, 41 | sylib 217 |
. . . . 5
⊢ (((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) ∧ (𝑓 ∈ (II Cn (𝑅 ×t 𝑆)) ∧ (𝑓‘0) = (𝑓‘1))) → ∃𝑔 𝑔 ∈ (((1st ↾ (∪ 𝑅
× ∪ 𝑆)) ∘ 𝑓)(PHtpy‘𝑅)((0[,]1) × {(((1st ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘0)}))) |
43 | | simplr 766 |
. . . . . . . . 9
⊢ (((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) ∧ (𝑓 ∈ (II Cn (𝑅 ×t 𝑆)) ∧ (𝑓‘0) = (𝑓‘1))) → 𝑆 ∈ SConn) |
44 | | tx2cn 22761 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ (TopOn‘∪ 𝑅)
∧ 𝑆 ∈
(TopOn‘∪ 𝑆)) → (2nd ↾ (∪ 𝑅
× ∪ 𝑆)) ∈ ((𝑅 ×t 𝑆) Cn 𝑆)) |
45 | 11, 16, 44 | syl2anc 584 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) ∧ (𝑓 ∈ (II Cn (𝑅 ×t 𝑆)) ∧ (𝑓‘0) = (𝑓‘1))) → (2nd ↾
(∪ 𝑅 × ∪ 𝑆)) ∈ ((𝑅 ×t 𝑆) Cn 𝑆)) |
46 | | cnco 22417 |
. . . . . . . . . 10
⊢ ((𝑓 ∈ (II Cn (𝑅 ×t 𝑆)) ∧ (2nd ↾
(∪ 𝑅 × ∪ 𝑆)) ∈ ((𝑅 ×t 𝑆) Cn 𝑆)) → ((2nd ↾ (∪ 𝑅
× ∪ 𝑆)) ∘ 𝑓) ∈ (II Cn 𝑆)) |
47 | 6, 45, 46 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) ∧ (𝑓 ∈ (II Cn (𝑅 ×t 𝑆)) ∧ (𝑓‘0) = (𝑓‘1))) → ((2nd ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓) ∈ (II Cn 𝑆)) |
48 | 21 | fveq2d 6778 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) ∧ (𝑓 ∈ (II Cn (𝑅 ×t 𝑆)) ∧ (𝑓‘0) = (𝑓‘1))) → ((2nd ↾
(∪ 𝑅 × ∪ 𝑆))‘(𝑓‘0)) = ((2nd ↾ (∪ 𝑅
× ∪ 𝑆))‘(𝑓‘1))) |
49 | | fvco3 6867 |
. . . . . . . . . . 11
⊢ ((𝑓:(0[,]1)⟶(∪ 𝑅
× ∪ 𝑆) ∧ 0 ∈ (0[,]1)) →
(((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘0) = ((2nd ↾ (∪ 𝑅
× ∪ 𝑆))‘(𝑓‘0))) |
50 | 28, 29, 49 | sylancl 586 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) ∧ (𝑓 ∈ (II Cn (𝑅 ×t 𝑆)) ∧ (𝑓‘0) = (𝑓‘1))) → (((2nd ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘0) = ((2nd ↾ (∪ 𝑅
× ∪ 𝑆))‘(𝑓‘0))) |
51 | | fvco3 6867 |
. . . . . . . . . . 11
⊢ ((𝑓:(0[,]1)⟶(∪ 𝑅
× ∪ 𝑆) ∧ 1 ∈ (0[,]1)) →
(((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘1) = ((2nd ↾ (∪ 𝑅
× ∪ 𝑆))‘(𝑓‘1))) |
52 | 28, 32, 51 | sylancl 586 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) ∧ (𝑓 ∈ (II Cn (𝑅 ×t 𝑆)) ∧ (𝑓‘0) = (𝑓‘1))) → (((2nd ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘1) = ((2nd ↾ (∪ 𝑅
× ∪ 𝑆))‘(𝑓‘1))) |
53 | 48, 50, 52 | 3eqtr4d 2788 |
. . . . . . . . 9
⊢ (((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) ∧ (𝑓 ∈ (II Cn (𝑅 ×t 𝑆)) ∧ (𝑓‘0) = (𝑓‘1))) → (((2nd ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘0) = (((2nd ↾ (∪ 𝑅
× ∪ 𝑆)) ∘ 𝑓)‘1)) |
54 | | sconnpht 33191 |
. . . . . . . . 9
⊢ ((𝑆 ∈ SConn ∧
((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓) ∈ (II Cn 𝑆) ∧ (((2nd ↾ (∪ 𝑅
× ∪ 𝑆)) ∘ 𝑓)‘0) = (((2nd ↾ (∪ 𝑅
× ∪ 𝑆)) ∘ 𝑓)‘1)) → ((2nd ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)( ≃ph‘𝑆)((0[,]1) ×
{(((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘0)})) |
55 | 43, 47, 53, 54 | syl3anc 1370 |
. . . . . . . 8
⊢ (((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) ∧ (𝑓 ∈ (II Cn (𝑅 ×t 𝑆)) ∧ (𝑓‘0) = (𝑓‘1))) → ((2nd ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)( ≃ph‘𝑆)((0[,]1) ×
{(((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘0)})) |
56 | | isphtpc 24157 |
. . . . . . . 8
⊢
(((2nd ↾ (∪ 𝑅 × ∪ 𝑆))
∘ 𝑓)(
≃ph‘𝑆)((0[,]1) × {(((2nd ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘0)}) ↔ (((2nd ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓) ∈ (II Cn 𝑆) ∧ ((0[,]1) × {(((2nd
↾ (∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘0)}) ∈ (II Cn 𝑆) ∧ (((2nd ↾ (∪ 𝑅
× ∪ 𝑆)) ∘ 𝑓)(PHtpy‘𝑆)((0[,]1) × {(((2nd ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘0)})) ≠ ∅)) |
57 | 55, 56 | sylib 217 |
. . . . . . 7
⊢ (((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) ∧ (𝑓 ∈ (II Cn (𝑅 ×t 𝑆)) ∧ (𝑓‘0) = (𝑓‘1))) → (((2nd ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓) ∈ (II Cn 𝑆) ∧ ((0[,]1) × {(((2nd
↾ (∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘0)}) ∈ (II Cn 𝑆) ∧ (((2nd ↾ (∪ 𝑅
× ∪ 𝑆)) ∘ 𝑓)(PHtpy‘𝑆)((0[,]1) × {(((2nd ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘0)})) ≠ ∅)) |
58 | 57 | simp3d 1143 |
. . . . . 6
⊢ (((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) ∧ (𝑓 ∈ (II Cn (𝑅 ×t 𝑆)) ∧ (𝑓‘0) = (𝑓‘1))) → (((2nd ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)(PHtpy‘𝑆)((0[,]1) × {(((2nd ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘0)})) ≠ ∅) |
59 | | n0 4280 |
. . . . . 6
⊢
((((2nd ↾ (∪ 𝑅 × ∪ 𝑆))
∘ 𝑓)(PHtpy‘𝑆)((0[,]1) × {(((2nd ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘0)})) ≠ ∅ ↔
∃ℎ ℎ ∈ (((2nd ↾ (∪ 𝑅
× ∪ 𝑆)) ∘ 𝑓)(PHtpy‘𝑆)((0[,]1) × {(((2nd ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘0)}))) |
60 | 58, 59 | sylib 217 |
. . . . 5
⊢ (((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) ∧ (𝑓 ∈ (II Cn (𝑅 ×t 𝑆)) ∧ (𝑓‘0) = (𝑓‘1))) → ∃ℎ ℎ ∈ (((2nd ↾ (∪ 𝑅
× ∪ 𝑆)) ∘ 𝑓)(PHtpy‘𝑆)((0[,]1) × {(((2nd ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘0)}))) |
61 | | exdistrv 1959 |
. . . . . 6
⊢
(∃𝑔∃ℎ(𝑔 ∈ (((1st ↾ (∪ 𝑅
× ∪ 𝑆)) ∘ 𝑓)(PHtpy‘𝑅)((0[,]1) × {(((1st ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘0)})) ∧ ℎ ∈ (((2nd ↾ (∪ 𝑅
× ∪ 𝑆)) ∘ 𝑓)(PHtpy‘𝑆)((0[,]1) × {(((2nd ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘0)}))) ↔ (∃𝑔 𝑔 ∈ (((1st ↾ (∪ 𝑅
× ∪ 𝑆)) ∘ 𝑓)(PHtpy‘𝑅)((0[,]1) × {(((1st ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘0)})) ∧ ∃ℎ ℎ ∈ (((2nd ↾ (∪ 𝑅
× ∪ 𝑆)) ∘ 𝑓)(PHtpy‘𝑆)((0[,]1) × {(((2nd ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘0)})))) |
62 | 8 | adantr 481 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) ∧ (𝑓 ∈ (II Cn (𝑅 ×t 𝑆)) ∧ (𝑓‘0) = (𝑓‘1))) ∧ (𝑔 ∈ (((1st ↾ (∪ 𝑅
× ∪ 𝑆)) ∘ 𝑓)(PHtpy‘𝑅)((0[,]1) × {(((1st ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘0)})) ∧ ℎ ∈ (((2nd ↾ (∪ 𝑅
× ∪ 𝑆)) ∘ 𝑓)(PHtpy‘𝑆)((0[,]1) × {(((2nd ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘0)})))) → 𝑅 ∈ Top) |
63 | 13 | adantr 481 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) ∧ (𝑓 ∈ (II Cn (𝑅 ×t 𝑆)) ∧ (𝑓‘0) = (𝑓‘1))) ∧ (𝑔 ∈ (((1st ↾ (∪ 𝑅
× ∪ 𝑆)) ∘ 𝑓)(PHtpy‘𝑅)((0[,]1) × {(((1st ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘0)})) ∧ ℎ ∈ (((2nd ↾ (∪ 𝑅
× ∪ 𝑆)) ∘ 𝑓)(PHtpy‘𝑆)((0[,]1) × {(((2nd ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘0)})))) → 𝑆 ∈ Top) |
64 | 6 | adantr 481 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) ∧ (𝑓 ∈ (II Cn (𝑅 ×t 𝑆)) ∧ (𝑓‘0) = (𝑓‘1))) ∧ (𝑔 ∈ (((1st ↾ (∪ 𝑅
× ∪ 𝑆)) ∘ 𝑓)(PHtpy‘𝑅)((0[,]1) × {(((1st ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘0)})) ∧ ℎ ∈ (((2nd ↾ (∪ 𝑅
× ∪ 𝑆)) ∘ 𝑓)(PHtpy‘𝑆)((0[,]1) × {(((2nd ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘0)})))) → 𝑓 ∈ (II Cn (𝑅 ×t 𝑆))) |
65 | | eqid 2738 |
. . . . . . . . 9
⊢
((1st ↾ (∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓) = ((1st ↾ (∪ 𝑅
× ∪ 𝑆)) ∘ 𝑓) |
66 | | eqid 2738 |
. . . . . . . . 9
⊢
((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓) = ((2nd ↾ (∪ 𝑅
× ∪ 𝑆)) ∘ 𝑓) |
67 | | simprl 768 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) ∧ (𝑓 ∈ (II Cn (𝑅 ×t 𝑆)) ∧ (𝑓‘0) = (𝑓‘1))) ∧ (𝑔 ∈ (((1st ↾ (∪ 𝑅
× ∪ 𝑆)) ∘ 𝑓)(PHtpy‘𝑅)((0[,]1) × {(((1st ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘0)})) ∧ ℎ ∈ (((2nd ↾ (∪ 𝑅
× ∪ 𝑆)) ∘ 𝑓)(PHtpy‘𝑆)((0[,]1) × {(((2nd ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘0)})))) → 𝑔 ∈ (((1st ↾ (∪ 𝑅
× ∪ 𝑆)) ∘ 𝑓)(PHtpy‘𝑅)((0[,]1) × {(((1st ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘0)}))) |
68 | | simprr 770 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) ∧ (𝑓 ∈ (II Cn (𝑅 ×t 𝑆)) ∧ (𝑓‘0) = (𝑓‘1))) ∧ (𝑔 ∈ (((1st ↾ (∪ 𝑅
× ∪ 𝑆)) ∘ 𝑓)(PHtpy‘𝑅)((0[,]1) × {(((1st ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘0)})) ∧ ℎ ∈ (((2nd ↾ (∪ 𝑅
× ∪ 𝑆)) ∘ 𝑓)(PHtpy‘𝑆)((0[,]1) × {(((2nd ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘0)})))) → ℎ ∈ (((2nd ↾ (∪ 𝑅
× ∪ 𝑆)) ∘ 𝑓)(PHtpy‘𝑆)((0[,]1) × {(((2nd ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘0)}))) |
69 | 62, 63, 64, 65, 66, 67, 68 | txsconnlem 33202 |
. . . . . . . 8
⊢ ((((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) ∧ (𝑓 ∈ (II Cn (𝑅 ×t 𝑆)) ∧ (𝑓‘0) = (𝑓‘1))) ∧ (𝑔 ∈ (((1st ↾ (∪ 𝑅
× ∪ 𝑆)) ∘ 𝑓)(PHtpy‘𝑅)((0[,]1) × {(((1st ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘0)})) ∧ ℎ ∈ (((2nd ↾ (∪ 𝑅
× ∪ 𝑆)) ∘ 𝑓)(PHtpy‘𝑆)((0[,]1) × {(((2nd ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘0)})))) → 𝑓( ≃ph‘(𝑅 ×t 𝑆))((0[,]1) × {(𝑓‘0)})) |
70 | 69 | ex 413 |
. . . . . . 7
⊢ (((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) ∧ (𝑓 ∈ (II Cn (𝑅 ×t 𝑆)) ∧ (𝑓‘0) = (𝑓‘1))) → ((𝑔 ∈ (((1st ↾ (∪ 𝑅
× ∪ 𝑆)) ∘ 𝑓)(PHtpy‘𝑅)((0[,]1) × {(((1st ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘0)})) ∧ ℎ ∈ (((2nd ↾ (∪ 𝑅
× ∪ 𝑆)) ∘ 𝑓)(PHtpy‘𝑆)((0[,]1) × {(((2nd ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘0)}))) → 𝑓( ≃ph‘(𝑅 ×t 𝑆))((0[,]1) × {(𝑓‘0)}))) |
71 | 70 | exlimdvv 1937 |
. . . . . 6
⊢ (((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) ∧ (𝑓 ∈ (II Cn (𝑅 ×t 𝑆)) ∧ (𝑓‘0) = (𝑓‘1))) → (∃𝑔∃ℎ(𝑔 ∈ (((1st ↾ (∪ 𝑅
× ∪ 𝑆)) ∘ 𝑓)(PHtpy‘𝑅)((0[,]1) × {(((1st ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘0)})) ∧ ℎ ∈ (((2nd ↾ (∪ 𝑅
× ∪ 𝑆)) ∘ 𝑓)(PHtpy‘𝑆)((0[,]1) × {(((2nd ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘0)}))) → 𝑓( ≃ph‘(𝑅 ×t 𝑆))((0[,]1) × {(𝑓‘0)}))) |
72 | 61, 71 | syl5bir 242 |
. . . . 5
⊢ (((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) ∧ (𝑓 ∈ (II Cn (𝑅 ×t 𝑆)) ∧ (𝑓‘0) = (𝑓‘1))) → ((∃𝑔 𝑔 ∈ (((1st ↾ (∪ 𝑅
× ∪ 𝑆)) ∘ 𝑓)(PHtpy‘𝑅)((0[,]1) × {(((1st ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘0)})) ∧ ∃ℎ ℎ ∈ (((2nd ↾ (∪ 𝑅
× ∪ 𝑆)) ∘ 𝑓)(PHtpy‘𝑆)((0[,]1) × {(((2nd ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘0)}))) → 𝑓( ≃ph‘(𝑅 ×t 𝑆))((0[,]1) × {(𝑓‘0)}))) |
73 | 42, 60, 72 | mp2and 696 |
. . . 4
⊢ (((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) ∧ (𝑓 ∈ (II Cn (𝑅 ×t 𝑆)) ∧ (𝑓‘0) = (𝑓‘1))) → 𝑓( ≃ph‘(𝑅 ×t 𝑆))((0[,]1) × {(𝑓‘0)})) |
74 | 73 | expr 457 |
. . 3
⊢ (((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) ∧ 𝑓 ∈ (II Cn (𝑅 ×t 𝑆))) → ((𝑓‘0) = (𝑓‘1) → 𝑓( ≃ph‘(𝑅 ×t 𝑆))((0[,]1) × {(𝑓‘0)}))) |
75 | 74 | ralrimiva 3103 |
. 2
⊢ ((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) →
∀𝑓 ∈ (II Cn
(𝑅 ×t
𝑆))((𝑓‘0) = (𝑓‘1) → 𝑓( ≃ph‘(𝑅 ×t 𝑆))((0[,]1) × {(𝑓‘0)}))) |
76 | | issconn 33188 |
. 2
⊢ ((𝑅 ×t 𝑆) ∈ SConn ↔ ((𝑅 ×t 𝑆) ∈ PConn ∧
∀𝑓 ∈ (II Cn
(𝑅 ×t
𝑆))((𝑓‘0) = (𝑓‘1) → 𝑓( ≃ph‘(𝑅 ×t 𝑆))((0[,]1) × {(𝑓‘0)})))) |
77 | 4, 75, 76 | sylanbrc 583 |
1
⊢ ((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) → (𝑅 ×t 𝑆) ∈ SConn) |