Step | Hyp | Ref
| Expression |
1 | | sconnpconn 32762 |
. . 3
⊢ (𝑅 ∈ SConn → 𝑅 ∈ PConn) |
2 | | sconnpconn 32762 |
. . 3
⊢ (𝑆 ∈ SConn → 𝑆 ∈ PConn) |
3 | | txpconn 32767 |
. . 3
⊢ ((𝑅 ∈ PConn ∧ 𝑆 ∈ PConn) → (𝑅 ×t 𝑆) ∈ PConn) |
4 | 1, 2, 3 | syl2an 599 |
. 2
⊢ ((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) → (𝑅 ×t 𝑆) ∈ PConn) |
5 | | simpll 767 |
. . . . . . . . 9
⊢ (((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) ∧ (𝑓 ∈ (II Cn (𝑅 ×t 𝑆)) ∧ (𝑓‘0) = (𝑓‘1))) → 𝑅 ∈ SConn) |
6 | | simprl 771 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) ∧ (𝑓 ∈ (II Cn (𝑅 ×t 𝑆)) ∧ (𝑓‘0) = (𝑓‘1))) → 𝑓 ∈ (II Cn (𝑅 ×t 𝑆))) |
7 | | sconntop 32763 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ SConn → 𝑅 ∈ Top) |
8 | 7 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) ∧ (𝑓 ∈ (II Cn (𝑅 ×t 𝑆)) ∧ (𝑓‘0) = (𝑓‘1))) → 𝑅 ∈ Top) |
9 | | eqid 2738 |
. . . . . . . . . . . . 13
⊢ ∪ 𝑅 =
∪ 𝑅 |
10 | 9 | toptopon 21670 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ Top ↔ 𝑅 ∈ (TopOn‘∪ 𝑅)) |
11 | 8, 10 | sylib 221 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) ∧ (𝑓 ∈ (II Cn (𝑅 ×t 𝑆)) ∧ (𝑓‘0) = (𝑓‘1))) → 𝑅 ∈ (TopOn‘∪ 𝑅)) |
12 | | sconntop 32763 |
. . . . . . . . . . . . 13
⊢ (𝑆 ∈ SConn → 𝑆 ∈ Top) |
13 | 12 | ad2antlr 727 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) ∧ (𝑓 ∈ (II Cn (𝑅 ×t 𝑆)) ∧ (𝑓‘0) = (𝑓‘1))) → 𝑆 ∈ Top) |
14 | | eqid 2738 |
. . . . . . . . . . . . 13
⊢ ∪ 𝑆 =
∪ 𝑆 |
15 | 14 | toptopon 21670 |
. . . . . . . . . . . 12
⊢ (𝑆 ∈ Top ↔ 𝑆 ∈ (TopOn‘∪ 𝑆)) |
16 | 13, 15 | sylib 221 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) ∧ (𝑓 ∈ (II Cn (𝑅 ×t 𝑆)) ∧ (𝑓‘0) = (𝑓‘1))) → 𝑆 ∈ (TopOn‘∪ 𝑆)) |
17 | | tx1cn 22362 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ (TopOn‘∪ 𝑅)
∧ 𝑆 ∈
(TopOn‘∪ 𝑆)) → (1st ↾ (∪ 𝑅
× ∪ 𝑆)) ∈ ((𝑅 ×t 𝑆) Cn 𝑅)) |
18 | 11, 16, 17 | syl2anc 587 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) ∧ (𝑓 ∈ (II Cn (𝑅 ×t 𝑆)) ∧ (𝑓‘0) = (𝑓‘1))) → (1st ↾
(∪ 𝑅 × ∪ 𝑆)) ∈ ((𝑅 ×t 𝑆) Cn 𝑅)) |
19 | | cnco 22019 |
. . . . . . . . . 10
⊢ ((𝑓 ∈ (II Cn (𝑅 ×t 𝑆)) ∧ (1st ↾
(∪ 𝑅 × ∪ 𝑆)) ∈ ((𝑅 ×t 𝑆) Cn 𝑅)) → ((1st ↾ (∪ 𝑅
× ∪ 𝑆)) ∘ 𝑓) ∈ (II Cn 𝑅)) |
20 | 6, 18, 19 | syl2anc 587 |
. . . . . . . . 9
⊢ (((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) ∧ (𝑓 ∈ (II Cn (𝑅 ×t 𝑆)) ∧ (𝑓‘0) = (𝑓‘1))) → ((1st ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓) ∈ (II Cn 𝑅)) |
21 | | simprr 773 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) ∧ (𝑓 ∈ (II Cn (𝑅 ×t 𝑆)) ∧ (𝑓‘0) = (𝑓‘1))) → (𝑓‘0) = (𝑓‘1)) |
22 | 21 | fveq2d 6680 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) ∧ (𝑓 ∈ (II Cn (𝑅 ×t 𝑆)) ∧ (𝑓‘0) = (𝑓‘1))) → ((1st ↾
(∪ 𝑅 × ∪ 𝑆))‘(𝑓‘0)) = ((1st ↾ (∪ 𝑅
× ∪ 𝑆))‘(𝑓‘1))) |
23 | | iitopon 23633 |
. . . . . . . . . . . . 13
⊢ II ∈
(TopOn‘(0[,]1)) |
24 | 23 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) ∧ (𝑓 ∈ (II Cn (𝑅 ×t 𝑆)) ∧ (𝑓‘0) = (𝑓‘1))) → II ∈
(TopOn‘(0[,]1))) |
25 | | txtopon 22344 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ (TopOn‘∪ 𝑅)
∧ 𝑆 ∈
(TopOn‘∪ 𝑆)) → (𝑅 ×t 𝑆) ∈ (TopOn‘(∪ 𝑅
× ∪ 𝑆))) |
26 | 11, 16, 25 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) ∧ (𝑓 ∈ (II Cn (𝑅 ×t 𝑆)) ∧ (𝑓‘0) = (𝑓‘1))) → (𝑅 ×t 𝑆) ∈ (TopOn‘(∪ 𝑅
× ∪ 𝑆))) |
27 | | cnf2 22002 |
. . . . . . . . . . . 12
⊢ ((II
∈ (TopOn‘(0[,]1)) ∧ (𝑅 ×t 𝑆) ∈ (TopOn‘(∪ 𝑅
× ∪ 𝑆)) ∧ 𝑓 ∈ (II Cn (𝑅 ×t 𝑆))) → 𝑓:(0[,]1)⟶(∪
𝑅 × ∪ 𝑆)) |
28 | 24, 26, 6, 27 | syl3anc 1372 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) ∧ (𝑓 ∈ (II Cn (𝑅 ×t 𝑆)) ∧ (𝑓‘0) = (𝑓‘1))) → 𝑓:(0[,]1)⟶(∪
𝑅 × ∪ 𝑆)) |
29 | | 0elunit 12945 |
. . . . . . . . . . 11
⊢ 0 ∈
(0[,]1) |
30 | | fvco3 6769 |
. . . . . . . . . . 11
⊢ ((𝑓:(0[,]1)⟶(∪ 𝑅
× ∪ 𝑆) ∧ 0 ∈ (0[,]1)) →
(((1st ↾ (∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘0) = ((1st ↾ (∪ 𝑅
× ∪ 𝑆))‘(𝑓‘0))) |
31 | 28, 29, 30 | sylancl 589 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) ∧ (𝑓 ∈ (II Cn (𝑅 ×t 𝑆)) ∧ (𝑓‘0) = (𝑓‘1))) → (((1st ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘0) = ((1st ↾ (∪ 𝑅
× ∪ 𝑆))‘(𝑓‘0))) |
32 | | 1elunit 12946 |
. . . . . . . . . . 11
⊢ 1 ∈
(0[,]1) |
33 | | fvco3 6769 |
. . . . . . . . . . 11
⊢ ((𝑓:(0[,]1)⟶(∪ 𝑅
× ∪ 𝑆) ∧ 1 ∈ (0[,]1)) →
(((1st ↾ (∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘1) = ((1st ↾ (∪ 𝑅
× ∪ 𝑆))‘(𝑓‘1))) |
34 | 28, 32, 33 | sylancl 589 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) ∧ (𝑓 ∈ (II Cn (𝑅 ×t 𝑆)) ∧ (𝑓‘0) = (𝑓‘1))) → (((1st ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘1) = ((1st ↾ (∪ 𝑅
× ∪ 𝑆))‘(𝑓‘1))) |
35 | 22, 31, 34 | 3eqtr4d 2783 |
. . . . . . . . 9
⊢ (((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) ∧ (𝑓 ∈ (II Cn (𝑅 ×t 𝑆)) ∧ (𝑓‘0) = (𝑓‘1))) → (((1st ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘0) = (((1st ↾ (∪ 𝑅
× ∪ 𝑆)) ∘ 𝑓)‘1)) |
36 | | sconnpht 32764 |
. . . . . . . . 9
⊢ ((𝑅 ∈ SConn ∧
((1st ↾ (∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓) ∈ (II Cn 𝑅) ∧ (((1st ↾ (∪ 𝑅
× ∪ 𝑆)) ∘ 𝑓)‘0) = (((1st ↾ (∪ 𝑅
× ∪ 𝑆)) ∘ 𝑓)‘1)) → ((1st ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)( ≃ph‘𝑅)((0[,]1) ×
{(((1st ↾ (∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘0)})) |
37 | 5, 20, 35, 36 | syl3anc 1372 |
. . . . . . . 8
⊢ (((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) ∧ (𝑓 ∈ (II Cn (𝑅 ×t 𝑆)) ∧ (𝑓‘0) = (𝑓‘1))) → ((1st ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)( ≃ph‘𝑅)((0[,]1) ×
{(((1st ↾ (∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘0)})) |
38 | | isphtpc 23748 |
. . . . . . . 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 221 |
. . . . . . 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 1145 |
. . . . . 6
⊢ (((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) ∧ (𝑓 ∈ (II Cn (𝑅 ×t 𝑆)) ∧ (𝑓‘0) = (𝑓‘1))) → (((1st ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)(PHtpy‘𝑅)((0[,]1) × {(((1st ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘0)})) ≠ ∅) |
41 | | n0 4235 |
. . . . . 6
⊢
((((1st ↾ (∪ 𝑅 × ∪ 𝑆))
∘ 𝑓)(PHtpy‘𝑅)((0[,]1) × {(((1st ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘0)})) ≠ ∅ ↔
∃𝑔 𝑔 ∈ (((1st ↾ (∪ 𝑅
× ∪ 𝑆)) ∘ 𝑓)(PHtpy‘𝑅)((0[,]1) × {(((1st ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘0)}))) |
42 | 40, 41 | sylib 221 |
. . . . 5
⊢ (((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) ∧ (𝑓 ∈ (II Cn (𝑅 ×t 𝑆)) ∧ (𝑓‘0) = (𝑓‘1))) → ∃𝑔 𝑔 ∈ (((1st ↾ (∪ 𝑅
× ∪ 𝑆)) ∘ 𝑓)(PHtpy‘𝑅)((0[,]1) × {(((1st ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘0)}))) |
43 | | simplr 769 |
. . . . . . . . 9
⊢ (((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) ∧ (𝑓 ∈ (II Cn (𝑅 ×t 𝑆)) ∧ (𝑓‘0) = (𝑓‘1))) → 𝑆 ∈ SConn) |
44 | | tx2cn 22363 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ (TopOn‘∪ 𝑅)
∧ 𝑆 ∈
(TopOn‘∪ 𝑆)) → (2nd ↾ (∪ 𝑅
× ∪ 𝑆)) ∈ ((𝑅 ×t 𝑆) Cn 𝑆)) |
45 | 11, 16, 44 | syl2anc 587 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) ∧ (𝑓 ∈ (II Cn (𝑅 ×t 𝑆)) ∧ (𝑓‘0) = (𝑓‘1))) → (2nd ↾
(∪ 𝑅 × ∪ 𝑆)) ∈ ((𝑅 ×t 𝑆) Cn 𝑆)) |
46 | | cnco 22019 |
. . . . . . . . . 10
⊢ ((𝑓 ∈ (II Cn (𝑅 ×t 𝑆)) ∧ (2nd ↾
(∪ 𝑅 × ∪ 𝑆)) ∈ ((𝑅 ×t 𝑆) Cn 𝑆)) → ((2nd ↾ (∪ 𝑅
× ∪ 𝑆)) ∘ 𝑓) ∈ (II Cn 𝑆)) |
47 | 6, 45, 46 | syl2anc 587 |
. . . . . . . . 9
⊢ (((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) ∧ (𝑓 ∈ (II Cn (𝑅 ×t 𝑆)) ∧ (𝑓‘0) = (𝑓‘1))) → ((2nd ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓) ∈ (II Cn 𝑆)) |
48 | 21 | fveq2d 6680 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) ∧ (𝑓 ∈ (II Cn (𝑅 ×t 𝑆)) ∧ (𝑓‘0) = (𝑓‘1))) → ((2nd ↾
(∪ 𝑅 × ∪ 𝑆))‘(𝑓‘0)) = ((2nd ↾ (∪ 𝑅
× ∪ 𝑆))‘(𝑓‘1))) |
49 | | fvco3 6769 |
. . . . . . . . . . 11
⊢ ((𝑓:(0[,]1)⟶(∪ 𝑅
× ∪ 𝑆) ∧ 0 ∈ (0[,]1)) →
(((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘0) = ((2nd ↾ (∪ 𝑅
× ∪ 𝑆))‘(𝑓‘0))) |
50 | 28, 29, 49 | sylancl 589 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) ∧ (𝑓 ∈ (II Cn (𝑅 ×t 𝑆)) ∧ (𝑓‘0) = (𝑓‘1))) → (((2nd ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘0) = ((2nd ↾ (∪ 𝑅
× ∪ 𝑆))‘(𝑓‘0))) |
51 | | fvco3 6769 |
. . . . . . . . . . 11
⊢ ((𝑓:(0[,]1)⟶(∪ 𝑅
× ∪ 𝑆) ∧ 1 ∈ (0[,]1)) →
(((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘1) = ((2nd ↾ (∪ 𝑅
× ∪ 𝑆))‘(𝑓‘1))) |
52 | 28, 32, 51 | sylancl 589 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) ∧ (𝑓 ∈ (II Cn (𝑅 ×t 𝑆)) ∧ (𝑓‘0) = (𝑓‘1))) → (((2nd ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘1) = ((2nd ↾ (∪ 𝑅
× ∪ 𝑆))‘(𝑓‘1))) |
53 | 48, 50, 52 | 3eqtr4d 2783 |
. . . . . . . . 9
⊢ (((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) ∧ (𝑓 ∈ (II Cn (𝑅 ×t 𝑆)) ∧ (𝑓‘0) = (𝑓‘1))) → (((2nd ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘0) = (((2nd ↾ (∪ 𝑅
× ∪ 𝑆)) ∘ 𝑓)‘1)) |
54 | | sconnpht 32764 |
. . . . . . . . 9
⊢ ((𝑆 ∈ SConn ∧
((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓) ∈ (II Cn 𝑆) ∧ (((2nd ↾ (∪ 𝑅
× ∪ 𝑆)) ∘ 𝑓)‘0) = (((2nd ↾ (∪ 𝑅
× ∪ 𝑆)) ∘ 𝑓)‘1)) → ((2nd ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)( ≃ph‘𝑆)((0[,]1) ×
{(((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘0)})) |
55 | 43, 47, 53, 54 | syl3anc 1372 |
. . . . . . . 8
⊢ (((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) ∧ (𝑓 ∈ (II Cn (𝑅 ×t 𝑆)) ∧ (𝑓‘0) = (𝑓‘1))) → ((2nd ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)( ≃ph‘𝑆)((0[,]1) ×
{(((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘0)})) |
56 | | isphtpc 23748 |
. . . . . . . 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 221 |
. . . . . . 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 1145 |
. . . . . 6
⊢ (((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) ∧ (𝑓 ∈ (II Cn (𝑅 ×t 𝑆)) ∧ (𝑓‘0) = (𝑓‘1))) → (((2nd ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)(PHtpy‘𝑆)((0[,]1) × {(((2nd ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘0)})) ≠ ∅) |
59 | | n0 4235 |
. . . . . 6
⊢
((((2nd ↾ (∪ 𝑅 × ∪ 𝑆))
∘ 𝑓)(PHtpy‘𝑆)((0[,]1) × {(((2nd ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘0)})) ≠ ∅ ↔
∃ℎ ℎ ∈ (((2nd ↾ (∪ 𝑅
× ∪ 𝑆)) ∘ 𝑓)(PHtpy‘𝑆)((0[,]1) × {(((2nd ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘0)}))) |
60 | 58, 59 | sylib 221 |
. . . . 5
⊢ (((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) ∧ (𝑓 ∈ (II Cn (𝑅 ×t 𝑆)) ∧ (𝑓‘0) = (𝑓‘1))) → ∃ℎ ℎ ∈ (((2nd ↾ (∪ 𝑅
× ∪ 𝑆)) ∘ 𝑓)(PHtpy‘𝑆)((0[,]1) × {(((2nd ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘0)}))) |
61 | | exdistrv 1963 |
. . . . . 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 484 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) ∧ (𝑓 ∈ (II Cn (𝑅 ×t 𝑆)) ∧ (𝑓‘0) = (𝑓‘1))) ∧ (𝑔 ∈ (((1st ↾ (∪ 𝑅
× ∪ 𝑆)) ∘ 𝑓)(PHtpy‘𝑅)((0[,]1) × {(((1st ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘0)})) ∧ ℎ ∈ (((2nd ↾ (∪ 𝑅
× ∪ 𝑆)) ∘ 𝑓)(PHtpy‘𝑆)((0[,]1) × {(((2nd ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘0)})))) → 𝑅 ∈ Top) |
63 | 13 | adantr 484 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) ∧ (𝑓 ∈ (II Cn (𝑅 ×t 𝑆)) ∧ (𝑓‘0) = (𝑓‘1))) ∧ (𝑔 ∈ (((1st ↾ (∪ 𝑅
× ∪ 𝑆)) ∘ 𝑓)(PHtpy‘𝑅)((0[,]1) × {(((1st ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘0)})) ∧ ℎ ∈ (((2nd ↾ (∪ 𝑅
× ∪ 𝑆)) ∘ 𝑓)(PHtpy‘𝑆)((0[,]1) × {(((2nd ↾
(∪ 𝑅 × ∪ 𝑆)) ∘ 𝑓)‘0)})))) → 𝑆 ∈ Top) |
64 | 6 | adantr 484 |
. . . . . . . . 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 771 |
. . . . . . . . 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 773 |
. . . . . . . . 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 32775 |
. . . . . . . 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 416 |
. . . . . . 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 1941 |
. . . . . 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 246 |
. . . . 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 699 |
. . . 4
⊢ (((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) ∧ (𝑓 ∈ (II Cn (𝑅 ×t 𝑆)) ∧ (𝑓‘0) = (𝑓‘1))) → 𝑓( ≃ph‘(𝑅 ×t 𝑆))((0[,]1) × {(𝑓‘0)})) |
74 | 73 | expr 460 |
. . 3
⊢ (((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) ∧ 𝑓 ∈ (II Cn (𝑅 ×t 𝑆))) → ((𝑓‘0) = (𝑓‘1) → 𝑓( ≃ph‘(𝑅 ×t 𝑆))((0[,]1) × {(𝑓‘0)}))) |
75 | 74 | ralrimiva 3096 |
. 2
⊢ ((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) →
∀𝑓 ∈ (II Cn
(𝑅 ×t
𝑆))((𝑓‘0) = (𝑓‘1) → 𝑓( ≃ph‘(𝑅 ×t 𝑆))((0[,]1) × {(𝑓‘0)}))) |
76 | | issconn 32761 |
. 2
⊢ ((𝑅 ×t 𝑆) ∈ SConn ↔ ((𝑅 ×t 𝑆) ∈ PConn ∧
∀𝑓 ∈ (II Cn
(𝑅 ×t
𝑆))((𝑓‘0) = (𝑓‘1) → 𝑓( ≃ph‘(𝑅 ×t 𝑆))((0[,]1) × {(𝑓‘0)})))) |
77 | 4, 75, 76 | sylanbrc 586 |
1
⊢ ((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) → (𝑅 ×t 𝑆) ∈ SConn) |