Step | Hyp | Ref
| Expression |
1 | | sconnpconn 33885 |
. . 3
β’ (π
β SConn β π
β PConn) |
2 | | sconnpconn 33885 |
. . 3
β’ (π β SConn β π β PConn) |
3 | | txpconn 33890 |
. . 3
β’ ((π
β PConn β§ π β PConn) β (π
Γt π) β PConn) |
4 | 1, 2, 3 | syl2an 597 |
. 2
β’ ((π
β SConn β§ π β SConn) β (π
Γt π) β PConn) |
5 | | simpll 766 |
. . . . . . . . 9
β’ (((π
β SConn β§ π β SConn) β§ (π β (II Cn (π
Γt π)) β§ (πβ0) = (πβ1))) β π
β SConn) |
6 | | simprl 770 |
. . . . . . . . . 10
β’ (((π
β SConn β§ π β SConn) β§ (π β (II Cn (π
Γt π)) β§ (πβ0) = (πβ1))) β π β (II Cn (π
Γt π))) |
7 | | sconntop 33886 |
. . . . . . . . . . . . 13
β’ (π
β SConn β π
β Top) |
8 | 7 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π
β SConn β§ π β SConn) β§ (π β (II Cn (π
Γt π)) β§ (πβ0) = (πβ1))) β π
β Top) |
9 | | eqid 2733 |
. . . . . . . . . . . . 13
β’ βͺ π
=
βͺ π
|
10 | 9 | toptopon 22289 |
. . . . . . . . . . . 12
β’ (π
β Top β π
β (TopOnββͺ π
)) |
11 | 8, 10 | sylib 217 |
. . . . . . . . . . 11
β’ (((π
β SConn β§ π β SConn) β§ (π β (II Cn (π
Γt π)) β§ (πβ0) = (πβ1))) β π
β (TopOnββͺ π
)) |
12 | | sconntop 33886 |
. . . . . . . . . . . . 13
β’ (π β SConn β π β Top) |
13 | 12 | ad2antlr 726 |
. . . . . . . . . . . 12
β’ (((π
β SConn β§ π β SConn) β§ (π β (II Cn (π
Γt π)) β§ (πβ0) = (πβ1))) β π β Top) |
14 | | eqid 2733 |
. . . . . . . . . . . . 13
β’ βͺ π =
βͺ π |
15 | 14 | toptopon 22289 |
. . . . . . . . . . . 12
β’ (π β Top β π β (TopOnββͺ π)) |
16 | 13, 15 | sylib 217 |
. . . . . . . . . . 11
β’ (((π
β SConn β§ π β SConn) β§ (π β (II Cn (π
Γt π)) β§ (πβ0) = (πβ1))) β π β (TopOnββͺ π)) |
17 | | tx1cn 22983 |
. . . . . . . . . . 11
β’ ((π
β (TopOnββͺ π
)
β§ π β
(TopOnββͺ π)) β (1st βΎ (βͺ π
Γ βͺ π)) β ((π
Γt π) Cn π
)) |
18 | 11, 16, 17 | syl2anc 585 |
. . . . . . . . . 10
β’ (((π
β SConn β§ π β SConn) β§ (π β (II Cn (π
Γt π)) β§ (πβ0) = (πβ1))) β (1st βΎ
(βͺ π
Γ βͺ π)) β ((π
Γt π) Cn π
)) |
19 | | cnco 22640 |
. . . . . . . . . 10
β’ ((π β (II Cn (π
Γt π)) β§ (1st βΎ
(βͺ π
Γ βͺ π)) β ((π
Γt π) Cn π
)) β ((1st βΎ (βͺ π
Γ βͺ π)) β π) β (II Cn π
)) |
20 | 6, 18, 19 | syl2anc 585 |
. . . . . . . . 9
β’ (((π
β SConn β§ π β SConn) β§ (π β (II Cn (π
Γt π)) β§ (πβ0) = (πβ1))) β ((1st βΎ
(βͺ π
Γ βͺ π)) β π) β (II Cn π
)) |
21 | | simprr 772 |
. . . . . . . . . . 11
β’ (((π
β SConn β§ π β SConn) β§ (π β (II Cn (π
Γt π)) β§ (πβ0) = (πβ1))) β (πβ0) = (πβ1)) |
22 | 21 | fveq2d 6850 |
. . . . . . . . . 10
β’ (((π
β SConn β§ π β SConn) β§ (π β (II Cn (π
Γt π)) β§ (πβ0) = (πβ1))) β ((1st βΎ
(βͺ π
Γ βͺ π))β(πβ0)) = ((1st βΎ (βͺ π
Γ βͺ π))β(πβ1))) |
23 | | iitopon 24265 |
. . . . . . . . . . . . 13
β’ II β
(TopOnβ(0[,]1)) |
24 | 23 | a1i 11 |
. . . . . . . . . . . 12
β’ (((π
β SConn β§ π β SConn) β§ (π β (II Cn (π
Γt π)) β§ (πβ0) = (πβ1))) β II β
(TopOnβ(0[,]1))) |
25 | | txtopon 22965 |
. . . . . . . . . . . . 13
β’ ((π
β (TopOnββͺ π
)
β§ π β
(TopOnββͺ π)) β (π
Γt π) β (TopOnβ(βͺ π
Γ βͺ π))) |
26 | 11, 16, 25 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (((π
β SConn β§ π β SConn) β§ (π β (II Cn (π
Γt π)) β§ (πβ0) = (πβ1))) β (π
Γt π) β (TopOnβ(βͺ π
Γ βͺ π))) |
27 | | cnf2 22623 |
. . . . . . . . . . . 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 13395 |
. . . . . . . . . . 11
β’ 0 β
(0[,]1) |
30 | | fvco3 6944 |
. . . . . . . . . . 11
β’ ((π:(0[,]1)βΆ(βͺ π
Γ βͺ π) β§ 0 β (0[,]1)) β
(((1st βΎ (βͺ π
Γ βͺ π)) β π)β0) = ((1st βΎ (βͺ π
Γ βͺ π))β(πβ0))) |
31 | 28, 29, 30 | sylancl 587 |
. . . . . . . . . 10
β’ (((π
β SConn β§ π β SConn) β§ (π β (II Cn (π
Γt π)) β§ (πβ0) = (πβ1))) β (((1st βΎ
(βͺ π
Γ βͺ π)) β π)β0) = ((1st βΎ (βͺ π
Γ βͺ π))β(πβ0))) |
32 | | 1elunit 13396 |
. . . . . . . . . . 11
β’ 1 β
(0[,]1) |
33 | | fvco3 6944 |
. . . . . . . . . . 11
β’ ((π:(0[,]1)βΆ(βͺ π
Γ βͺ π) β§ 1 β (0[,]1)) β
(((1st βΎ (βͺ π
Γ βͺ π)) β π)β1) = ((1st βΎ (βͺ π
Γ βͺ π))β(πβ1))) |
34 | 28, 32, 33 | sylancl 587 |
. . . . . . . . . 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 33887 |
. . . . . . . . 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 24380 |
. . . . . . . 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 1145 |
. . . . . 6
β’ (((π
β SConn β§ π β SConn) β§ (π β (II Cn (π
Γt π)) β§ (πβ0) = (πβ1))) β (((1st βΎ
(βͺ π
Γ βͺ π)) β π)(PHtpyβπ
)((0[,]1) Γ {(((1st βΎ
(βͺ π
Γ βͺ π)) β π)β0)})) β β
) |
41 | | n0 4310 |
. . . . . 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 768 |
. . . . . . . . 9
β’ (((π
β SConn β§ π β SConn) β§ (π β (II Cn (π
Γt π)) β§ (πβ0) = (πβ1))) β π β SConn) |
44 | | tx2cn 22984 |
. . . . . . . . . . 11
β’ ((π
β (TopOnββͺ π
)
β§ π β
(TopOnββͺ π)) β (2nd βΎ (βͺ π
Γ βͺ π)) β ((π
Γt π) Cn π)) |
45 | 11, 16, 44 | syl2anc 585 |
. . . . . . . . . 10
β’ (((π
β SConn β§ π β SConn) β§ (π β (II Cn (π
Γt π)) β§ (πβ0) = (πβ1))) β (2nd βΎ
(βͺ π
Γ βͺ π)) β ((π
Γt π) Cn π)) |
46 | | cnco 22640 |
. . . . . . . . . 10
β’ ((π β (II Cn (π
Γt π)) β§ (2nd βΎ
(βͺ π
Γ βͺ π)) β ((π
Γt π) Cn π)) β ((2nd βΎ (βͺ π
Γ βͺ π)) β π) β (II Cn π)) |
47 | 6, 45, 46 | syl2anc 585 |
. . . . . . . . 9
β’ (((π
β SConn β§ π β SConn) β§ (π β (II Cn (π
Γt π)) β§ (πβ0) = (πβ1))) β ((2nd βΎ
(βͺ π
Γ βͺ π)) β π) β (II Cn π)) |
48 | 21 | fveq2d 6850 |
. . . . . . . . . 10
β’ (((π
β SConn β§ π β SConn) β§ (π β (II Cn (π
Γt π)) β§ (πβ0) = (πβ1))) β ((2nd βΎ
(βͺ π
Γ βͺ π))β(πβ0)) = ((2nd βΎ (βͺ π
Γ βͺ π))β(πβ1))) |
49 | | fvco3 6944 |
. . . . . . . . . . 11
β’ ((π:(0[,]1)βΆ(βͺ π
Γ βͺ π) β§ 0 β (0[,]1)) β
(((2nd βΎ (βͺ π
Γ βͺ π)) β π)β0) = ((2nd βΎ (βͺ π
Γ βͺ π))β(πβ0))) |
50 | 28, 29, 49 | sylancl 587 |
. . . . . . . . . 10
β’ (((π
β SConn β§ π β SConn) β§ (π β (II Cn (π
Γt π)) β§ (πβ0) = (πβ1))) β (((2nd βΎ
(βͺ π
Γ βͺ π)) β π)β0) = ((2nd βΎ (βͺ π
Γ βͺ π))β(πβ0))) |
51 | | fvco3 6944 |
. . . . . . . . . . 11
β’ ((π:(0[,]1)βΆ(βͺ π
Γ βͺ π) β§ 1 β (0[,]1)) β
(((2nd βΎ (βͺ π
Γ βͺ π)) β π)β1) = ((2nd βΎ (βͺ π
Γ βͺ π))β(πβ1))) |
52 | 28, 32, 51 | sylancl 587 |
. . . . . . . . . 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 33887 |
. . . . . . . . 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 24380 |
. . . . . . . 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 1145 |
. . . . . 6
β’ (((π
β SConn β§ π β SConn) β§ (π β (II Cn (π
Γt π)) β§ (πβ0) = (πβ1))) β (((2nd βΎ
(βͺ π
Γ βͺ π)) β π)(PHtpyβπ)((0[,]1) Γ {(((2nd βΎ
(βͺ π
Γ βͺ π)) β π)β0)})) β β
) |
59 | | n0 4310 |
. . . . . 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 1960 |
. . . . . 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 482 |
. . . . . . . . 9
β’ ((((π
β SConn β§ π β SConn) β§ (π β (II Cn (π
Γt π)) β§ (πβ0) = (πβ1))) β§ (π β (((1st βΎ (βͺ π
Γ βͺ π)) β π)(PHtpyβπ
)((0[,]1) Γ {(((1st βΎ
(βͺ π
Γ βͺ π)) β π)β0)})) β§ β β (((2nd βΎ (βͺ π
Γ βͺ π)) β π)(PHtpyβπ)((0[,]1) Γ {(((2nd βΎ
(βͺ π
Γ βͺ π)) β π)β0)})))) β π
β Top) |
63 | 13 | adantr 482 |
. . . . . . . . 9
β’ ((((π
β SConn β§ π β SConn) β§ (π β (II Cn (π
Γt π)) β§ (πβ0) = (πβ1))) β§ (π β (((1st βΎ (βͺ π
Γ βͺ π)) β π)(PHtpyβπ
)((0[,]1) Γ {(((1st βΎ
(βͺ π
Γ βͺ π)) β π)β0)})) β§ β β (((2nd βΎ (βͺ π
Γ βͺ π)) β π)(PHtpyβπ)((0[,]1) Γ {(((2nd βΎ
(βͺ π
Γ βͺ π)) β π)β0)})))) β π β Top) |
64 | 6 | adantr 482 |
. . . . . . . . 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 2733 |
. . . . . . . . 9
β’
((1st βΎ (βͺ π
Γ βͺ π)) β π) = ((1st βΎ (βͺ π
Γ βͺ π)) β π) |
66 | | eqid 2733 |
. . . . . . . . 9
β’
((2nd βΎ (βͺ π
Γ βͺ π)) β π) = ((2nd βΎ (βͺ π
Γ βͺ π)) β π) |
67 | | simprl 770 |
. . . . . . . . 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 772 |
. . . . . . . . 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 33898 |
. . . . . . . 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 414 |
. . . . . . 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 1938 |
. . . . . 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 | biimtrrid 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 698 |
. . . 4
β’ (((π
β SConn β§ π β SConn) β§ (π β (II Cn (π
Γt π)) β§ (πβ0) = (πβ1))) β π( βphβ(π
Γt π))((0[,]1) Γ {(πβ0)})) |
74 | 73 | expr 458 |
. . 3
β’ (((π
β SConn β§ π β SConn) β§ π β (II Cn (π
Γt π))) β ((πβ0) = (πβ1) β π( βphβ(π
Γt π))((0[,]1) Γ {(πβ0)}))) |
75 | 74 | ralrimiva 3140 |
. 2
β’ ((π
β SConn β§ π β SConn) β
βπ β (II Cn
(π
Γt
π))((πβ0) = (πβ1) β π( βphβ(π
Γt π))((0[,]1) Γ {(πβ0)}))) |
76 | | issconn 33884 |
. 2
β’ ((π
Γt π) β SConn β ((π
Γt π) β PConn β§
βπ β (II Cn
(π
Γt
π))((πβ0) = (πβ1) β π( βphβ(π
Γt π))((0[,]1) Γ {(πβ0)})))) |
77 | 4, 75, 76 | sylanbrc 584 |
1
β’ ((π
β SConn β§ π β SConn) β (π
Γt π) β SConn) |