Step | Hyp | Ref
| Expression |
1 | | nllytop 22840 |
. . 3
β’ (π
β π-Locally π΄ β π
β Top) |
2 | | nllytop 22840 |
. . 3
β’ (π β π-Locally π΄ β π β Top) |
3 | | txtop 22936 |
. . 3
β’ ((π
β Top β§ π β Top) β (π
Γt π) β Top) |
4 | 1, 2, 3 | syl2an 597 |
. 2
β’ ((π
β π-Locally π΄ β§ π β π-Locally π΄) β (π
Γt π) β Top) |
5 | | eltx 22935 |
. . . 4
β’ ((π
β π-Locally π΄ β§ π β π-Locally π΄) β (π₯ β (π
Γt π) β βπ¦ β π₯ βπ’ β π
βπ£ β π (π¦ β (π’ Γ π£) β§ (π’ Γ π£) β π₯))) |
6 | | simpll 766 |
. . . . . . . . 9
β’ (((π
β π-Locally π΄ β§ π β π-Locally π΄) β§ ((π’ β π
β§ π£ β π) β§ (π¦ β (π’ Γ π£) β§ (π’ Γ π£) β π₯))) β π
β π-Locally π΄) |
7 | | simprll 778 |
. . . . . . . . 9
β’ (((π
β π-Locally π΄ β§ π β π-Locally π΄) β§ ((π’ β π
β§ π£ β π) β§ (π¦ β (π’ Γ π£) β§ (π’ Γ π£) β π₯))) β π’ β π
) |
8 | | simprrl 780 |
. . . . . . . . . 10
β’ (((π
β π-Locally π΄ β§ π β π-Locally π΄) β§ ((π’ β π
β§ π£ β π) β§ (π¦ β (π’ Γ π£) β§ (π’ Γ π£) β π₯))) β π¦ β (π’ Γ π£)) |
9 | | xp1st 7954 |
. . . . . . . . . 10
β’ (π¦ β (π’ Γ π£) β (1st βπ¦) β π’) |
10 | 8, 9 | syl 17 |
. . . . . . . . 9
β’ (((π
β π-Locally π΄ β§ π β π-Locally π΄) β§ ((π’ β π
β§ π£ β π) β§ (π¦ β (π’ Γ π£) β§ (π’ Γ π£) β π₯))) β (1st βπ¦) β π’) |
11 | | nlly2i 22843 |
. . . . . . . . 9
β’ ((π
β π-Locally π΄ β§ π’ β π
β§ (1st βπ¦) β π’) β βπ β π« π’βπ β π
((1st βπ¦) β π β§ π β π β§ (π
βΎt π) β π΄)) |
12 | 6, 7, 10, 11 | syl3anc 1372 |
. . . . . . . 8
β’ (((π
β π-Locally π΄ β§ π β π-Locally π΄) β§ ((π’ β π
β§ π£ β π) β§ (π¦ β (π’ Γ π£) β§ (π’ Γ π£) β π₯))) β βπ β π« π’βπ β π
((1st βπ¦) β π β§ π β π β§ (π
βΎt π) β π΄)) |
13 | | simplr 768 |
. . . . . . . . 9
β’ (((π
β π-Locally π΄ β§ π β π-Locally π΄) β§ ((π’ β π
β§ π£ β π) β§ (π¦ β (π’ Γ π£) β§ (π’ Γ π£) β π₯))) β π β π-Locally π΄) |
14 | | simprlr 779 |
. . . . . . . . 9
β’ (((π
β π-Locally π΄ β§ π β π-Locally π΄) β§ ((π’ β π
β§ π£ β π) β§ (π¦ β (π’ Γ π£) β§ (π’ Γ π£) β π₯))) β π£ β π) |
15 | | xp2nd 7955 |
. . . . . . . . . 10
β’ (π¦ β (π’ Γ π£) β (2nd βπ¦) β π£) |
16 | 8, 15 | syl 17 |
. . . . . . . . 9
β’ (((π
β π-Locally π΄ β§ π β π-Locally π΄) β§ ((π’ β π
β§ π£ β π) β§ (π¦ β (π’ Γ π£) β§ (π’ Γ π£) β π₯))) β (2nd βπ¦) β π£) |
17 | | nlly2i 22843 |
. . . . . . . . 9
β’ ((π β π-Locally π΄ β§ π£ β π β§ (2nd βπ¦) β π£) β βπ β π« π£βπ β π ((2nd βπ¦) β π β§ π β π β§ (π βΎt π) β π΄)) |
18 | 13, 14, 16, 17 | syl3anc 1372 |
. . . . . . . 8
β’ (((π
β π-Locally π΄ β§ π β π-Locally π΄) β§ ((π’ β π
β§ π£ β π) β§ (π¦ β (π’ Γ π£) β§ (π’ Γ π£) β π₯))) β βπ β π« π£βπ β π ((2nd βπ¦) β π β§ π β π β§ (π βΎt π) β π΄)) |
19 | | reeanv 3216 |
. . . . . . . . 9
β’
(βπ β
π« π’βπ β π« π£(βπ β π
((1st βπ¦) β π β§ π β π β§ (π
βΎt π) β π΄) β§ βπ β π ((2nd βπ¦) β π β§ π β π β§ (π βΎt π) β π΄)) β (βπ β π« π’βπ β π
((1st βπ¦) β π β§ π β π β§ (π
βΎt π) β π΄) β§ βπ β π« π£βπ β π ((2nd βπ¦) β π β§ π β π β§ (π βΎt π) β π΄))) |
20 | | reeanv 3216 |
. . . . . . . . . . 11
β’
(βπ β
π
βπ β π (((1st βπ¦) β π β§ π β π β§ (π
βΎt π) β π΄) β§ ((2nd βπ¦) β π β§ π β π β§ (π βΎt π) β π΄)) β (βπ β π
((1st βπ¦) β π β§ π β π β§ (π
βΎt π) β π΄) β§ βπ β π ((2nd βπ¦) β π β§ π β π β§ (π βΎt π) β π΄))) |
21 | 4 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . 17
β’
(((((π
β
π-Locally π΄ β§
π β π-Locally
π΄) β§ ((π’ β π
β§ π£ β π) β§ (π¦ β (π’ Γ π£) β§ (π’ Γ π£) β π₯))) β§ ((π β π« π’ β§ π β π« π£) β§ (π β π
β§ π β π))) β§ (((1st βπ¦) β π β§ π β π β§ (π
βΎt π) β π΄) β§ ((2nd βπ¦) β π β§ π β π β§ (π βΎt π) β π΄))) β (π
Γt π) β Top) |
22 | 1 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π
β π-Locally π΄ β§ π β π-Locally π΄) β§ ((π’ β π
β§ π£ β π) β§ (π¦ β (π’ Γ π£) β§ (π’ Γ π£) β π₯))) β π
β Top) |
23 | 22 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π
β
π-Locally π΄ β§
π β π-Locally
π΄) β§ ((π’ β π
β§ π£ β π) β§ (π¦ β (π’ Γ π£) β§ (π’ Γ π£) β π₯))) β§ ((π β π« π’ β§ π β π« π£) β§ (π β π
β§ π β π))) β§ (((1st βπ¦) β π β§ π β π β§ (π
βΎt π) β π΄) β§ ((2nd βπ¦) β π β§ π β π β§ (π βΎt π) β π΄))) β π
β Top) |
24 | 13, 2 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π
β π-Locally π΄ β§ π β π-Locally π΄) β§ ((π’ β π
β§ π£ β π) β§ (π¦ β (π’ Γ π£) β§ (π’ Γ π£) β π₯))) β π β Top) |
25 | 24 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π
β
π-Locally π΄ β§
π β π-Locally
π΄) β§ ((π’ β π
β§ π£ β π) β§ (π¦ β (π’ Γ π£) β§ (π’ Γ π£) β π₯))) β§ ((π β π« π’ β§ π β π« π£) β§ (π β π
β§ π β π))) β§ (((1st βπ¦) β π β§ π β π β§ (π
βΎt π) β π΄) β§ ((2nd βπ¦) β π β§ π β π β§ (π βΎt π) β π΄))) β π β Top) |
26 | | simprrl 780 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π
β π-Locally π΄ β§ π β π-Locally π΄) β§ ((π’ β π
β§ π£ β π) β§ (π¦ β (π’ Γ π£) β§ (π’ Γ π£) β π₯))) β§ ((π β π« π’ β§ π β π« π£) β§ (π β π
β§ π β π))) β π β π
) |
27 | 26 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π
β
π-Locally π΄ β§
π β π-Locally
π΄) β§ ((π’ β π
β§ π£ β π) β§ (π¦ β (π’ Γ π£) β§ (π’ Γ π£) β π₯))) β§ ((π β π« π’ β§ π β π« π£) β§ (π β π
β§ π β π))) β§ (((1st βπ¦) β π β§ π β π β§ (π
βΎt π) β π΄) β§ ((2nd βπ¦) β π β§ π β π β§ (π βΎt π) β π΄))) β π β π
) |
28 | | simprrr 781 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π
β π-Locally π΄ β§ π β π-Locally π΄) β§ ((π’ β π
β§ π£ β π) β§ (π¦ β (π’ Γ π£) β§ (π’ Γ π£) β π₯))) β§ ((π β π« π’ β§ π β π« π£) β§ (π β π
β§ π β π))) β π β π) |
29 | 28 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π
β
π-Locally π΄ β§
π β π-Locally
π΄) β§ ((π’ β π
β§ π£ β π) β§ (π¦ β (π’ Γ π£) β§ (π’ Γ π£) β π₯))) β§ ((π β π« π’ β§ π β π« π£) β§ (π β π
β§ π β π))) β§ (((1st βπ¦) β π β§ π β π β§ (π
βΎt π) β π΄) β§ ((2nd βπ¦) β π β§ π β π β§ (π βΎt π) β π΄))) β π β π) |
30 | | txopn 22969 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π
β Top β§ π β Top) β§ (π β π
β§ π β π)) β (π Γ π ) β (π
Γt π)) |
31 | 23, 25, 27, 29, 30 | syl22anc 838 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π
β
π-Locally π΄ β§
π β π-Locally
π΄) β§ ((π’ β π
β§ π£ β π) β§ (π¦ β (π’ Γ π£) β§ (π’ Γ π£) β π₯))) β§ ((π β π« π’ β§ π β π« π£) β§ (π β π
β§ π β π))) β§ (((1st βπ¦) β π β§ π β π β§ (π
βΎt π) β π΄) β§ ((2nd βπ¦) β π β§ π β π β§ (π βΎt π) β π΄))) β (π Γ π ) β (π
Γt π)) |
32 | 8 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π
β
π-Locally π΄ β§
π β π-Locally
π΄) β§ ((π’ β π
β§ π£ β π) β§ (π¦ β (π’ Γ π£) β§ (π’ Γ π£) β π₯))) β§ ((π β π« π’ β§ π β π« π£) β§ (π β π
β§ π β π))) β§ (((1st βπ¦) β π β§ π β π β§ (π
βΎt π) β π΄) β§ ((2nd βπ¦) β π β§ π β π β§ (π βΎt π) β π΄))) β π¦ β (π’ Γ π£)) |
33 | | 1st2nd2 7961 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π¦ β (π’ Γ π£) β π¦ = β¨(1st βπ¦), (2nd βπ¦)β©) |
34 | 32, 33 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π
β
π-Locally π΄ β§
π β π-Locally
π΄) β§ ((π’ β π
β§ π£ β π) β§ (π¦ β (π’ Γ π£) β§ (π’ Γ π£) β π₯))) β§ ((π β π« π’ β§ π β π« π£) β§ (π β π
β§ π β π))) β§ (((1st βπ¦) β π β§ π β π β§ (π
βΎt π) β π΄) β§ ((2nd βπ¦) β π β§ π β π β§ (π βΎt π) β π΄))) β π¦ = β¨(1st βπ¦), (2nd βπ¦)β©) |
35 | | simprl1 1219 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π
β
π-Locally π΄ β§
π β π-Locally
π΄) β§ ((π’ β π
β§ π£ β π) β§ (π¦ β (π’ Γ π£) β§ (π’ Γ π£) β π₯))) β§ ((π β π« π’ β§ π β π« π£) β§ (π β π
β§ π β π))) β§ (((1st βπ¦) β π β§ π β π β§ (π
βΎt π) β π΄) β§ ((2nd βπ¦) β π β§ π β π β§ (π βΎt π) β π΄))) β (1st βπ¦) β π) |
36 | | simprr1 1222 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π
β
π-Locally π΄ β§
π β π-Locally
π΄) β§ ((π’ β π
β§ π£ β π) β§ (π¦ β (π’ Γ π£) β§ (π’ Γ π£) β π₯))) β§ ((π β π« π’ β§ π β π« π£) β§ (π β π
β§ π β π))) β§ (((1st βπ¦) β π β§ π β π β§ (π
βΎt π) β π΄) β§ ((2nd βπ¦) β π β§ π β π β§ (π βΎt π) β π΄))) β (2nd βπ¦) β π ) |
37 | 35, 36 | opelxpd 5672 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π
β
π-Locally π΄ β§
π β π-Locally
π΄) β§ ((π’ β π
β§ π£ β π) β§ (π¦ β (π’ Γ π£) β§ (π’ Γ π£) β π₯))) β§ ((π β π« π’ β§ π β π« π£) β§ (π β π
β§ π β π))) β§ (((1st βπ¦) β π β§ π β π β§ (π
βΎt π) β π΄) β§ ((2nd βπ¦) β π β§ π β π β§ (π βΎt π) β π΄))) β β¨(1st
βπ¦), (2nd
βπ¦)β© β
(π Γ π )) |
38 | 34, 37 | eqeltrd 2834 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π
β
π-Locally π΄ β§
π β π-Locally
π΄) β§ ((π’ β π
β§ π£ β π) β§ (π¦ β (π’ Γ π£) β§ (π’ Γ π£) β π₯))) β§ ((π β π« π’ β§ π β π« π£) β§ (π β π
β§ π β π))) β§ (((1st βπ¦) β π β§ π β π β§ (π
βΎt π) β π΄) β§ ((2nd βπ¦) β π β§ π β π β§ (π βΎt π) β π΄))) β π¦ β (π Γ π )) |
39 | | opnneip 22486 |
. . . . . . . . . . . . . . . . . 18
β’ (((π
Γt π) β Top β§ (π Γ π ) β (π
Γt π) β§ π¦ β (π Γ π )) β (π Γ π ) β ((neiβ(π
Γt π))β{π¦})) |
40 | 21, 31, 38, 39 | syl3anc 1372 |
. . . . . . . . . . . . . . . . 17
β’
(((((π
β
π-Locally π΄ β§
π β π-Locally
π΄) β§ ((π’ β π
β§ π£ β π) β§ (π¦ β (π’ Γ π£) β§ (π’ Γ π£) β π₯))) β§ ((π β π« π’ β§ π β π« π£) β§ (π β π
β§ π β π))) β§ (((1st βπ¦) β π β§ π β π β§ (π
βΎt π) β π΄) β§ ((2nd βπ¦) β π β§ π β π β§ (π βΎt π) β π΄))) β (π Γ π ) β ((neiβ(π
Γt π))β{π¦})) |
41 | | simprl2 1220 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π
β
π-Locally π΄ β§
π β π-Locally
π΄) β§ ((π’ β π
β§ π£ β π) β§ (π¦ β (π’ Γ π£) β§ (π’ Γ π£) β π₯))) β§ ((π β π« π’ β§ π β π« π£) β§ (π β π
β§ π β π))) β§ (((1st βπ¦) β π β§ π β π β§ (π
βΎt π) β π΄) β§ ((2nd βπ¦) β π β§ π β π β§ (π βΎt π) β π΄))) β π β π) |
42 | | simprr2 1223 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π
β
π-Locally π΄ β§
π β π-Locally
π΄) β§ ((π’ β π
β§ π£ β π) β§ (π¦ β (π’ Γ π£) β§ (π’ Γ π£) β π₯))) β§ ((π β π« π’ β§ π β π« π£) β§ (π β π
β§ π β π))) β§ (((1st βπ¦) β π β§ π β π β§ (π
βΎt π) β π΄) β§ ((2nd βπ¦) β π β§ π β π β§ (π βΎt π) β π΄))) β π β π) |
43 | | xpss12 5649 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β π β§ π β π) β (π Γ π ) β (π Γ π)) |
44 | 41, 42, 43 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
β’
(((((π
β
π-Locally π΄ β§
π β π-Locally
π΄) β§ ((π’ β π
β§ π£ β π) β§ (π¦ β (π’ Γ π£) β§ (π’ Γ π£) β π₯))) β§ ((π β π« π’ β§ π β π« π£) β§ (π β π
β§ π β π))) β§ (((1st βπ¦) β π β§ π β π β§ (π
βΎt π) β π΄) β§ ((2nd βπ¦) β π β§ π β π β§ (π βΎt π) β π΄))) β (π Γ π ) β (π Γ π)) |
45 | | simprll 778 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π
β π-Locally π΄ β§ π β π-Locally π΄) β§ ((π’ β π
β§ π£ β π) β§ (π¦ β (π’ Γ π£) β§ (π’ Γ π£) β π₯))) β§ ((π β π« π’ β§ π β π« π£) β§ (π β π
β§ π β π))) β π β π« π’) |
46 | 45 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π
β
π-Locally π΄ β§
π β π-Locally
π΄) β§ ((π’ β π
β§ π£ β π) β§ (π¦ β (π’ Γ π£) β§ (π’ Γ π£) β π₯))) β§ ((π β π« π’ β§ π β π« π£) β§ (π β π
β§ π β π))) β§ (((1st βπ¦) β π β§ π β π β§ (π
βΎt π) β π΄) β§ ((2nd βπ¦) β π β§ π β π β§ (π βΎt π) β π΄))) β π β π« π’) |
47 | 46 | elpwid 4570 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π
β
π-Locally π΄ β§
π β π-Locally
π΄) β§ ((π’ β π
β§ π£ β π) β§ (π¦ β (π’ Γ π£) β§ (π’ Γ π£) β π₯))) β§ ((π β π« π’ β§ π β π« π£) β§ (π β π
β§ π β π))) β§ (((1st βπ¦) β π β§ π β π β§ (π
βΎt π) β π΄) β§ ((2nd βπ¦) β π β§ π β π β§ (π βΎt π) β π΄))) β π β π’) |
48 | 7 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π
β
π-Locally π΄ β§
π β π-Locally
π΄) β§ ((π’ β π
β§ π£ β π) β§ (π¦ β (π’ Γ π£) β§ (π’ Γ π£) β π₯))) β§ ((π β π« π’ β§ π β π« π£) β§ (π β π
β§ π β π))) β§ (((1st βπ¦) β π β§ π β π β§ (π
βΎt π) β π΄) β§ ((2nd βπ¦) β π β§ π β π β§ (π βΎt π) β π΄))) β π’ β π
) |
49 | | elssuni 4899 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π’ β π
β π’ β βͺ π
) |
50 | 48, 49 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π
β
π-Locally π΄ β§
π β π-Locally
π΄) β§ ((π’ β π
β§ π£ β π) β§ (π¦ β (π’ Γ π£) β§ (π’ Γ π£) β π₯))) β§ ((π β π« π’ β§ π β π« π£) β§ (π β π
β§ π β π))) β§ (((1st βπ¦) β π β§ π β π β§ (π
βΎt π) β π΄) β§ ((2nd βπ¦) β π β§ π β π β§ (π βΎt π) β π΄))) β π’ β βͺ π
) |
51 | 47, 50 | sstrd 3955 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π
β
π-Locally π΄ β§
π β π-Locally
π΄) β§ ((π’ β π
β§ π£ β π) β§ (π¦ β (π’ Γ π£) β§ (π’ Γ π£) β π₯))) β§ ((π β π« π’ β§ π β π« π£) β§ (π β π
β§ π β π))) β§ (((1st βπ¦) β π β§ π β π β§ (π
βΎt π) β π΄) β§ ((2nd βπ¦) β π β§ π β π β§ (π βΎt π) β π΄))) β π β βͺ π
) |
52 | | simprlr 779 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π
β π-Locally π΄ β§ π β π-Locally π΄) β§ ((π’ β π
β§ π£ β π) β§ (π¦ β (π’ Γ π£) β§ (π’ Γ π£) β π₯))) β§ ((π β π« π’ β§ π β π« π£) β§ (π β π
β§ π β π))) β π β π« π£) |
53 | 52 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π
β
π-Locally π΄ β§
π β π-Locally
π΄) β§ ((π’ β π
β§ π£ β π) β§ (π¦ β (π’ Γ π£) β§ (π’ Γ π£) β π₯))) β§ ((π β π« π’ β§ π β π« π£) β§ (π β π
β§ π β π))) β§ (((1st βπ¦) β π β§ π β π β§ (π
βΎt π) β π΄) β§ ((2nd βπ¦) β π β§ π β π β§ (π βΎt π) β π΄))) β π β π« π£) |
54 | 53 | elpwid 4570 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π
β
π-Locally π΄ β§
π β π-Locally
π΄) β§ ((π’ β π
β§ π£ β π) β§ (π¦ β (π’ Γ π£) β§ (π’ Γ π£) β π₯))) β§ ((π β π« π’ β§ π β π« π£) β§ (π β π
β§ π β π))) β§ (((1st βπ¦) β π β§ π β π β§ (π
βΎt π) β π΄) β§ ((2nd βπ¦) β π β§ π β π β§ (π βΎt π) β π΄))) β π β π£) |
55 | 14 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π
β
π-Locally π΄ β§
π β π-Locally
π΄) β§ ((π’ β π
β§ π£ β π) β§ (π¦ β (π’ Γ π£) β§ (π’ Γ π£) β π₯))) β§ ((π β π« π’ β§ π β π« π£) β§ (π β π
β§ π β π))) β§ (((1st βπ¦) β π β§ π β π β§ (π
βΎt π) β π΄) β§ ((2nd βπ¦) β π β§ π β π β§ (π βΎt π) β π΄))) β π£ β π) |
56 | | elssuni 4899 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π£ β π β π£ β βͺ π) |
57 | 55, 56 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π
β
π-Locally π΄ β§
π β π-Locally
π΄) β§ ((π’ β π
β§ π£ β π) β§ (π¦ β (π’ Γ π£) β§ (π’ Γ π£) β π₯))) β§ ((π β π« π’ β§ π β π« π£) β§ (π β π
β§ π β π))) β§ (((1st βπ¦) β π β§ π β π β§ (π
βΎt π) β π΄) β§ ((2nd βπ¦) β π β§ π β π β§ (π βΎt π) β π΄))) β π£ β βͺ π) |
58 | 54, 57 | sstrd 3955 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π
β
π-Locally π΄ β§
π β π-Locally
π΄) β§ ((π’ β π
β§ π£ β π) β§ (π¦ β (π’ Γ π£) β§ (π’ Γ π£) β π₯))) β§ ((π β π« π’ β§ π β π« π£) β§ (π β π
β§ π β π))) β§ (((1st βπ¦) β π β§ π β π β§ (π
βΎt π) β π΄) β§ ((2nd βπ¦) β π β§ π β π β§ (π βΎt π) β π΄))) β π β βͺ π) |
59 | | xpss12 5649 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β βͺ π
β§ π β βͺ π)
β (π Γ π) β (βͺ π
Γ βͺ π)) |
60 | 51, 58, 59 | syl2anc 585 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π
β
π-Locally π΄ β§
π β π-Locally
π΄) β§ ((π’ β π
β§ π£ β π) β§ (π¦ β (π’ Γ π£) β§ (π’ Γ π£) β π₯))) β§ ((π β π« π’ β§ π β π« π£) β§ (π β π
β§ π β π))) β§ (((1st βπ¦) β π β§ π β π β§ (π
βΎt π) β π΄) β§ ((2nd βπ¦) β π β§ π β π β§ (π βΎt π) β π΄))) β (π Γ π) β (βͺ π
Γ βͺ π)) |
61 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . . 20
β’ βͺ π
=
βͺ π
|
62 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . . 20
β’ βͺ π =
βͺ π |
63 | 61, 62 | txuni 22959 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π
β Top β§ π β Top) β (βͺ π
Γ βͺ π) = βͺ (π
Γt π)) |
64 | 23, 25, 63 | syl2anc 585 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π
β
π-Locally π΄ β§
π β π-Locally
π΄) β§ ((π’ β π
β§ π£ β π) β§ (π¦ β (π’ Γ π£) β§ (π’ Γ π£) β π₯))) β§ ((π β π« π’ β§ π β π« π£) β§ (π β π
β§ π β π))) β§ (((1st βπ¦) β π β§ π β π β§ (π
βΎt π) β π΄) β§ ((2nd βπ¦) β π β§ π β π β§ (π βΎt π) β π΄))) β (βͺ
π
Γ βͺ π) =
βͺ (π
Γt π)) |
65 | 60, 64 | sseqtrd 3985 |
. . . . . . . . . . . . . . . . 17
β’
(((((π
β
π-Locally π΄ β§
π β π-Locally
π΄) β§ ((π’ β π
β§ π£ β π) β§ (π¦ β (π’ Γ π£) β§ (π’ Γ π£) β π₯))) β§ ((π β π« π’ β§ π β π« π£) β§ (π β π
β§ π β π))) β§ (((1st βπ¦) β π β§ π β π β§ (π
βΎt π) β π΄) β§ ((2nd βπ¦) β π β§ π β π β§ (π βΎt π) β π΄))) β (π Γ π) β βͺ (π
Γt π)) |
66 | | eqid 2733 |
. . . . . . . . . . . . . . . . . 18
β’ βͺ (π
Γt π) =
βͺ (π
Γt π) |
67 | 66 | ssnei2 22483 |
. . . . . . . . . . . . . . . . 17
β’ ((((π
Γt π) β Top β§ (π Γ π ) β ((neiβ(π
Γt π))β{π¦})) β§ ((π Γ π ) β (π Γ π) β§ (π Γ π) β βͺ (π
Γt π))) β (π Γ π) β ((neiβ(π
Γt π))β{π¦})) |
68 | 21, 40, 44, 65, 67 | syl22anc 838 |
. . . . . . . . . . . . . . . 16
β’
(((((π
β
π-Locally π΄ β§
π β π-Locally
π΄) β§ ((π’ β π
β§ π£ β π) β§ (π¦ β (π’ Γ π£) β§ (π’ Γ π£) β π₯))) β§ ((π β π« π’ β§ π β π« π£) β§ (π β π
β§ π β π))) β§ (((1st βπ¦) β π β§ π β π β§ (π
βΎt π) β π΄) β§ ((2nd βπ¦) β π β§ π β π β§ (π βΎt π) β π΄))) β (π Γ π) β ((neiβ(π
Γt π))β{π¦})) |
69 | | xpss12 5649 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β π’ β§ π β π£) β (π Γ π) β (π’ Γ π£)) |
70 | 47, 54, 69 | syl2anc 585 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π
β
π-Locally π΄ β§
π β π-Locally
π΄) β§ ((π’ β π
β§ π£ β π) β§ (π¦ β (π’ Γ π£) β§ (π’ Γ π£) β π₯))) β§ ((π β π« π’ β§ π β π« π£) β§ (π β π
β§ π β π))) β§ (((1st βπ¦) β π β§ π β π β§ (π
βΎt π) β π΄) β§ ((2nd βπ¦) β π β§ π β π β§ (π βΎt π) β π΄))) β (π Γ π) β (π’ Γ π£)) |
71 | | simprrr 781 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π
β π-Locally π΄ β§ π β π-Locally π΄) β§ ((π’ β π
β§ π£ β π) β§ (π¦ β (π’ Γ π£) β§ (π’ Γ π£) β π₯))) β (π’ Γ π£) β π₯) |
72 | 71 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π
β
π-Locally π΄ β§
π β π-Locally
π΄) β§ ((π’ β π
β§ π£ β π) β§ (π¦ β (π’ Γ π£) β§ (π’ Γ π£) β π₯))) β§ ((π β π« π’ β§ π β π« π£) β§ (π β π
β§ π β π))) β§ (((1st βπ¦) β π β§ π β π β§ (π
βΎt π) β π΄) β§ ((2nd βπ¦) β π β§ π β π β§ (π βΎt π) β π΄))) β (π’ Γ π£) β π₯) |
73 | 70, 72 | sstrd 3955 |
. . . . . . . . . . . . . . . . 17
β’
(((((π
β
π-Locally π΄ β§
π β π-Locally
π΄) β§ ((π’ β π
β§ π£ β π) β§ (π¦ β (π’ Γ π£) β§ (π’ Γ π£) β π₯))) β§ ((π β π« π’ β§ π β π« π£) β§ (π β π
β§ π β π))) β§ (((1st βπ¦) β π β§ π β π β§ (π
βΎt π) β π΄) β§ ((2nd βπ¦) β π β§ π β π β§ (π βΎt π) β π΄))) β (π Γ π) β π₯) |
74 | | vex 3448 |
. . . . . . . . . . . . . . . . . 18
β’ π₯ β V |
75 | 74 | elpw2 5303 |
. . . . . . . . . . . . . . . . 17
β’ ((π Γ π) β π« π₯ β (π Γ π) β π₯) |
76 | 73, 75 | sylibr 233 |
. . . . . . . . . . . . . . . 16
β’
(((((π
β
π-Locally π΄ β§
π β π-Locally
π΄) β§ ((π’ β π
β§ π£ β π) β§ (π¦ β (π’ Γ π£) β§ (π’ Γ π£) β π₯))) β§ ((π β π« π’ β§ π β π« π£) β§ (π β π
β§ π β π))) β§ (((1st βπ¦) β π β§ π β π β§ (π
βΎt π) β π΄) β§ ((2nd βπ¦) β π β§ π β π β§ (π βΎt π) β π΄))) β (π Γ π) β π« π₯) |
77 | 68, 76 | elind 4155 |
. . . . . . . . . . . . . . 15
β’
(((((π
β
π-Locally π΄ β§
π β π-Locally
π΄) β§ ((π’ β π
β§ π£ β π) β§ (π¦ β (π’ Γ π£) β§ (π’ Γ π£) β π₯))) β§ ((π β π« π’ β§ π β π« π£) β§ (π β π
β§ π β π))) β§ (((1st βπ¦) β π β§ π β π β§ (π
βΎt π) β π΄) β§ ((2nd βπ¦) β π β§ π β π β§ (π βΎt π) β π΄))) β (π Γ π) β (((neiβ(π
Γt π))β{π¦}) β© π« π₯)) |
78 | | txrest 22998 |
. . . . . . . . . . . . . . . . 17
β’ (((π
β Top β§ π β Top) β§ (π β π« π’ β§ π β π« π£)) β ((π
Γt π) βΎt (π Γ π)) = ((π
βΎt π) Γt (π βΎt π))) |
79 | 23, 25, 46, 53, 78 | syl22anc 838 |
. . . . . . . . . . . . . . . 16
β’
(((((π
β
π-Locally π΄ β§
π β π-Locally
π΄) β§ ((π’ β π
β§ π£ β π) β§ (π¦ β (π’ Γ π£) β§ (π’ Γ π£) β π₯))) β§ ((π β π« π’ β§ π β π« π£) β§ (π β π
β§ π β π))) β§ (((1st βπ¦) β π β§ π β π β§ (π
βΎt π) β π΄) β§ ((2nd βπ¦) β π β§ π β π β§ (π βΎt π) β π΄))) β ((π
Γt π) βΎt (π Γ π)) = ((π
βΎt π) Γt (π βΎt π))) |
80 | | simprl3 1221 |
. . . . . . . . . . . . . . . . 17
β’
(((((π
β
π-Locally π΄ β§
π β π-Locally
π΄) β§ ((π’ β π
β§ π£ β π) β§ (π¦ β (π’ Γ π£) β§ (π’ Γ π£) β π₯))) β§ ((π β π« π’ β§ π β π« π£) β§ (π β π
β§ π β π))) β§ (((1st βπ¦) β π β§ π β π β§ (π
βΎt π) β π΄) β§ ((2nd βπ¦) β π β§ π β π β§ (π βΎt π) β π΄))) β (π
βΎt π) β π΄) |
81 | | simprr3 1224 |
. . . . . . . . . . . . . . . . 17
β’
(((((π
β
π-Locally π΄ β§
π β π-Locally
π΄) β§ ((π’ β π
β§ π£ β π) β§ (π¦ β (π’ Γ π£) β§ (π’ Γ π£) β π₯))) β§ ((π β π« π’ β§ π β π« π£) β§ (π β π
β§ π β π))) β§ (((1st βπ¦) β π β§ π β π β§ (π
βΎt π) β π΄) β§ ((2nd βπ¦) β π β§ π β π β§ (π βΎt π) β π΄))) β (π βΎt π) β π΄) |
82 | | txlly.1 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β π΄ β§ π β π΄) β (π Γt π) β π΄) |
83 | 82 | caovcl 7549 |
. . . . . . . . . . . . . . . . 17
β’ (((π
βΎt π) β π΄ β§ (π βΎt π) β π΄) β ((π
βΎt π) Γt (π βΎt π)) β π΄) |
84 | 80, 81, 83 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’
(((((π
β
π-Locally π΄ β§
π β π-Locally
π΄) β§ ((π’ β π
β§ π£ β π) β§ (π¦ β (π’ Γ π£) β§ (π’ Γ π£) β π₯))) β§ ((π β π« π’ β§ π β π« π£) β§ (π β π
β§ π β π))) β§ (((1st βπ¦) β π β§ π β π β§ (π
βΎt π) β π΄) β§ ((2nd βπ¦) β π β§ π β π β§ (π βΎt π) β π΄))) β ((π
βΎt π) Γt (π βΎt π)) β π΄) |
85 | 79, 84 | eqeltrd 2834 |
. . . . . . . . . . . . . . 15
β’
(((((π
β
π-Locally π΄ β§
π β π-Locally
π΄) β§ ((π’ β π
β§ π£ β π) β§ (π¦ β (π’ Γ π£) β§ (π’ Γ π£) β π₯))) β§ ((π β π« π’ β§ π β π« π£) β§ (π β π
β§ π β π))) β§ (((1st βπ¦) β π β§ π β π β§ (π
βΎt π) β π΄) β§ ((2nd βπ¦) β π β§ π β π β§ (π βΎt π) β π΄))) β ((π
Γt π) βΎt (π Γ π)) β π΄) |
86 | | oveq2 7366 |
. . . . . . . . . . . . . . . . 17
β’ (π§ = (π Γ π) β ((π
Γt π) βΎt π§) = ((π
Γt π) βΎt (π Γ π))) |
87 | 86 | eleq1d 2819 |
. . . . . . . . . . . . . . . 16
β’ (π§ = (π Γ π) β (((π
Γt π) βΎt π§) β π΄ β ((π
Γt π) βΎt (π Γ π)) β π΄)) |
88 | 87 | rspcev 3580 |
. . . . . . . . . . . . . . 15
β’ (((π Γ π) β (((neiβ(π
Γt π))β{π¦}) β© π« π₯) β§ ((π
Γt π) βΎt (π Γ π)) β π΄) β βπ§ β (((neiβ(π
Γt π))β{π¦}) β© π« π₯)((π
Γt π) βΎt π§) β π΄) |
89 | 77, 85, 88 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’
(((((π
β
π-Locally π΄ β§
π β π-Locally
π΄) β§ ((π’ β π
β§ π£ β π) β§ (π¦ β (π’ Γ π£) β§ (π’ Γ π£) β π₯))) β§ ((π β π« π’ β§ π β π« π£) β§ (π β π
β§ π β π))) β§ (((1st βπ¦) β π β§ π β π β§ (π
βΎt π) β π΄) β§ ((2nd βπ¦) β π β§ π β π β§ (π βΎt π) β π΄))) β βπ§ β (((neiβ(π
Γt π))β{π¦}) β© π« π₯)((π
Γt π) βΎt π§) β π΄) |
90 | 89 | ex 414 |
. . . . . . . . . . . . 13
β’ ((((π
β π-Locally π΄ β§ π β π-Locally π΄) β§ ((π’ β π
β§ π£ β π) β§ (π¦ β (π’ Γ π£) β§ (π’ Γ π£) β π₯))) β§ ((π β π« π’ β§ π β π« π£) β§ (π β π
β§ π β π))) β ((((1st βπ¦) β π β§ π β π β§ (π
βΎt π) β π΄) β§ ((2nd βπ¦) β π β§ π β π β§ (π βΎt π) β π΄)) β βπ§ β (((neiβ(π
Γt π))β{π¦}) β© π« π₯)((π
Γt π) βΎt π§) β π΄)) |
91 | 90 | anassrs 469 |
. . . . . . . . . . . 12
β’
(((((π
β
π-Locally π΄ β§
π β π-Locally
π΄) β§ ((π’ β π
β§ π£ β π) β§ (π¦ β (π’ Γ π£) β§ (π’ Γ π£) β π₯))) β§ (π β π« π’ β§ π β π« π£)) β§ (π β π
β§ π β π)) β ((((1st βπ¦) β π β§ π β π β§ (π
βΎt π) β π΄) β§ ((2nd βπ¦) β π β§ π β π β§ (π βΎt π) β π΄)) β βπ§ β (((neiβ(π
Γt π))β{π¦}) β© π« π₯)((π
Γt π) βΎt π§) β π΄)) |
92 | 91 | rexlimdvva 3202 |
. . . . . . . . . . 11
β’ ((((π
β π-Locally π΄ β§ π β π-Locally π΄) β§ ((π’ β π
β§ π£ β π) β§ (π¦ β (π’ Γ π£) β§ (π’ Γ π£) β π₯))) β§ (π β π« π’ β§ π β π« π£)) β (βπ β π
βπ β π (((1st βπ¦) β π β§ π β π β§ (π
βΎt π) β π΄) β§ ((2nd βπ¦) β π β§ π β π β§ (π βΎt π) β π΄)) β βπ§ β (((neiβ(π
Γt π))β{π¦}) β© π« π₯)((π
Γt π) βΎt π§) β π΄)) |
93 | 20, 92 | biimtrrid 242 |
. . . . . . . . . 10
β’ ((((π
β π-Locally π΄ β§ π β π-Locally π΄) β§ ((π’ β π
β§ π£ β π) β§ (π¦ β (π’ Γ π£) β§ (π’ Γ π£) β π₯))) β§ (π β π« π’ β§ π β π« π£)) β ((βπ β π
((1st βπ¦) β π β§ π β π β§ (π
βΎt π) β π΄) β§ βπ β π ((2nd βπ¦) β π β§ π β π β§ (π βΎt π) β π΄)) β βπ§ β (((neiβ(π
Γt π))β{π¦}) β© π« π₯)((π
Γt π) βΎt π§) β π΄)) |
94 | 93 | rexlimdvva 3202 |
. . . . . . . . 9
β’ (((π
β π-Locally π΄ β§ π β π-Locally π΄) β§ ((π’ β π
β§ π£ β π) β§ (π¦ β (π’ Γ π£) β§ (π’ Γ π£) β π₯))) β (βπ β π« π’βπ β π« π£(βπ β π
((1st βπ¦) β π β§ π β π β§ (π
βΎt π) β π΄) β§ βπ β π ((2nd βπ¦) β π β§ π β π β§ (π βΎt π) β π΄)) β βπ§ β (((neiβ(π
Γt π))β{π¦}) β© π« π₯)((π
Γt π) βΎt π§) β π΄)) |
95 | 19, 94 | biimtrrid 242 |
. . . . . . . 8
β’ (((π
β π-Locally π΄ β§ π β π-Locally π΄) β§ ((π’ β π
β§ π£ β π) β§ (π¦ β (π’ Γ π£) β§ (π’ Γ π£) β π₯))) β ((βπ β π« π’βπ β π
((1st βπ¦) β π β§ π β π β§ (π
βΎt π) β π΄) β§ βπ β π« π£βπ β π ((2nd βπ¦) β π β§ π β π β§ (π βΎt π) β π΄)) β βπ§ β (((neiβ(π
Γt π))β{π¦}) β© π« π₯)((π
Γt π) βΎt π§) β π΄)) |
96 | 12, 18, 95 | mp2and 698 |
. . . . . . 7
β’ (((π
β π-Locally π΄ β§ π β π-Locally π΄) β§ ((π’ β π
β§ π£ β π) β§ (π¦ β (π’ Γ π£) β§ (π’ Γ π£) β π₯))) β βπ§ β (((neiβ(π
Γt π))β{π¦}) β© π« π₯)((π
Γt π) βΎt π§) β π΄) |
97 | 96 | expr 458 |
. . . . . 6
β’ (((π
β π-Locally π΄ β§ π β π-Locally π΄) β§ (π’ β π
β§ π£ β π)) β ((π¦ β (π’ Γ π£) β§ (π’ Γ π£) β π₯) β βπ§ β (((neiβ(π
Γt π))β{π¦}) β© π« π₯)((π
Γt π) βΎt π§) β π΄)) |
98 | 97 | rexlimdvva 3202 |
. . . . 5
β’ ((π
β π-Locally π΄ β§ π β π-Locally π΄) β (βπ’ β π
βπ£ β π (π¦ β (π’ Γ π£) β§ (π’ Γ π£) β π₯) β βπ§ β (((neiβ(π
Γt π))β{π¦}) β© π« π₯)((π
Γt π) βΎt π§) β π΄)) |
99 | 98 | ralimdv 3163 |
. . . 4
β’ ((π
β π-Locally π΄ β§ π β π-Locally π΄) β (βπ¦ β π₯ βπ’ β π
βπ£ β π (π¦ β (π’ Γ π£) β§ (π’ Γ π£) β π₯) β βπ¦ β π₯ βπ§ β (((neiβ(π
Γt π))β{π¦}) β© π« π₯)((π
Γt π) βΎt π§) β π΄)) |
100 | 5, 99 | sylbid 239 |
. . 3
β’ ((π
β π-Locally π΄ β§ π β π-Locally π΄) β (π₯ β (π
Γt π) β βπ¦ β π₯ βπ§ β (((neiβ(π
Γt π))β{π¦}) β© π« π₯)((π
Γt π) βΎt π§) β π΄)) |
101 | 100 | ralrimiv 3139 |
. 2
β’ ((π
β π-Locally π΄ β§ π β π-Locally π΄) β βπ₯ β (π
Γt π)βπ¦ β π₯ βπ§ β (((neiβ(π
Γt π))β{π¦}) β© π« π₯)((π
Γt π) βΎt π§) β π΄) |
102 | | isnlly 22836 |
. 2
β’ ((π
Γt π) β π-Locally π΄ β ((π
Γt π) β Top β§ βπ₯ β (π
Γt π)βπ¦ β π₯ βπ§ β (((neiβ(π
Γt π))β{π¦}) β© π« π₯)((π
Γt π) βΎt π§) β π΄)) |
103 | 4, 101, 102 | sylanbrc 584 |
1
β’ ((π
β π-Locally π΄ β§ π β π-Locally π΄) β (π
Γt π) β π-Locally π΄) |