Step | Hyp | Ref
| Expression |
1 | | relxp 5695 |
. . . . 5
β’ Rel
(π Γ π) |
2 | | utoptop.1 |
. . . . . . . . . . 11
β’ π½ = (unifTopβπ) |
3 | | utoptop 23739 |
. . . . . . . . . . 11
β’ (π β (UnifOnβπ) β (unifTopβπ) β Top) |
4 | 2, 3 | eqeltrid 2838 |
. . . . . . . . . 10
β’ (π β (UnifOnβπ) β π½ β Top) |
5 | | txtop 23073 |
. . . . . . . . . 10
β’ ((π½ β Top β§ π½ β Top) β (π½ Γt π½) β Top) |
6 | 4, 4, 5 | syl2anc 585 |
. . . . . . . . 9
β’ (π β (UnifOnβπ) β (π½ Γt π½) β Top) |
7 | 6 | ad3antrrr 729 |
. . . . . . . 8
β’ ((((π β (UnifOnβπ) β§ π β (π Γ π)) β§ (π β π β§ β‘π = π)) β§ π§ β ((clsβ(π½ Γt π½))βπ)) β (π½ Γt π½) β Top) |
8 | | simpllr 775 |
. . . . . . . . 9
β’ ((((π β (UnifOnβπ) β§ π β (π Γ π)) β§ (π β π β§ β‘π = π)) β§ π§ β ((clsβ(π½ Γt π½))βπ)) β π β (π Γ π)) |
9 | | utoptopon 23741 |
. . . . . . . . . . . . . 14
β’ (π β (UnifOnβπ) β (unifTopβπ) β (TopOnβπ)) |
10 | 2, 9 | eqeltrid 2838 |
. . . . . . . . . . . . 13
β’ (π β (UnifOnβπ) β π½ β (TopOnβπ)) |
11 | | toponuni 22416 |
. . . . . . . . . . . . 13
β’ (π½ β (TopOnβπ) β π = βͺ π½) |
12 | 10, 11 | syl 17 |
. . . . . . . . . . . 12
β’ (π β (UnifOnβπ) β π = βͺ π½) |
13 | 12 | sqxpeqd 5709 |
. . . . . . . . . . 11
β’ (π β (UnifOnβπ) β (π Γ π) = (βͺ π½ Γ βͺ π½)) |
14 | | eqid 2733 |
. . . . . . . . . . . . 13
β’ βͺ π½ =
βͺ π½ |
15 | 14, 14 | txuni 23096 |
. . . . . . . . . . . 12
β’ ((π½ β Top β§ π½ β Top) β (βͺ π½
Γ βͺ π½) = βͺ (π½ Γt π½)) |
16 | 4, 4, 15 | syl2anc 585 |
. . . . . . . . . . 11
β’ (π β (UnifOnβπ) β (βͺ π½
Γ βͺ π½) = βͺ (π½ Γt π½)) |
17 | 13, 16 | eqtrd 2773 |
. . . . . . . . . 10
β’ (π β (UnifOnβπ) β (π Γ π) = βͺ (π½ Γt π½)) |
18 | 17 | ad3antrrr 729 |
. . . . . . . . 9
β’ ((((π β (UnifOnβπ) β§ π β (π Γ π)) β§ (π β π β§ β‘π = π)) β§ π§ β ((clsβ(π½ Γt π½))βπ)) β (π Γ π) = βͺ (π½ Γt π½)) |
19 | 8, 18 | sseqtrd 4023 |
. . . . . . . 8
β’ ((((π β (UnifOnβπ) β§ π β (π Γ π)) β§ (π β π β§ β‘π = π)) β§ π§ β ((clsβ(π½ Γt π½))βπ)) β π β βͺ (π½ Γt π½)) |
20 | | eqid 2733 |
. . . . . . . . 9
β’ βͺ (π½
Γt π½) =
βͺ (π½ Γt π½) |
21 | 20 | clsss3 22563 |
. . . . . . . 8
β’ (((π½ Γt π½) β Top β§ π β βͺ (π½
Γt π½))
β ((clsβ(π½
Γt π½))βπ) β βͺ
(π½ Γt
π½)) |
22 | 7, 19, 21 | syl2anc 585 |
. . . . . . 7
β’ ((((π β (UnifOnβπ) β§ π β (π Γ π)) β§ (π β π β§ β‘π = π)) β§ π§ β ((clsβ(π½ Γt π½))βπ)) β ((clsβ(π½ Γt π½))βπ) β βͺ
(π½ Γt
π½)) |
23 | 22, 18 | sseqtrrd 4024 |
. . . . . 6
β’ ((((π β (UnifOnβπ) β§ π β (π Γ π)) β§ (π β π β§ β‘π = π)) β§ π§ β ((clsβ(π½ Γt π½))βπ)) β ((clsβ(π½ Γt π½))βπ) β (π Γ π)) |
24 | | simpr 486 |
. . . . . 6
β’ ((((π β (UnifOnβπ) β§ π β (π Γ π)) β§ (π β π β§ β‘π = π)) β§ π§ β ((clsβ(π½ Γt π½))βπ)) β π§ β ((clsβ(π½ Γt π½))βπ)) |
25 | 23, 24 | sseldd 3984 |
. . . . 5
β’ ((((π β (UnifOnβπ) β§ π β (π Γ π)) β§ (π β π β§ β‘π = π)) β§ π§ β ((clsβ(π½ Γt π½))βπ)) β π§ β (π Γ π)) |
26 | | 1st2nd 8025 |
. . . . 5
β’ ((Rel
(π Γ π) β§ π§ β (π Γ π)) β π§ = β¨(1st βπ§), (2nd βπ§)β©) |
27 | 1, 25, 26 | sylancr 588 |
. . . 4
β’ ((((π β (UnifOnβπ) β§ π β (π Γ π)) β§ (π β π β§ β‘π = π)) β§ π§ β ((clsβ(π½ Γt π½))βπ)) β π§ = β¨(1st βπ§), (2nd βπ§)β©) |
28 | | simp-4l 782 |
. . . . . . . . . 10
β’
(((((π β
(UnifOnβπ) β§
π β (π Γ π)) β§ (π β π β§ β‘π = π)) β§ π§ β ((clsβ(π½ Γt π½))βπ)) β§ π β (((π β {(1st βπ§)}) Γ (π β {(2nd βπ§)})) β© π)) β π β (UnifOnβπ)) |
29 | | simpr1l 1231 |
. . . . . . . . . . 11
β’ (((π β (UnifOnβπ) β§ π β (π Γ π)) β§ ((π β π β§ β‘π = π) β§ π§ β ((clsβ(π½ Γt π½))βπ) β§ π β (((π β {(1st βπ§)}) Γ (π β {(2nd βπ§)})) β© π))) β π β π) |
30 | 29 | 3anassrs 1361 |
. . . . . . . . . 10
β’
(((((π β
(UnifOnβπ) β§
π β (π Γ π)) β§ (π β π β§ β‘π = π)) β§ π§ β ((clsβ(π½ Γt π½))βπ)) β§ π β (((π β {(1st βπ§)}) Γ (π β {(2nd βπ§)})) β© π)) β π β π) |
31 | | ustrel 23716 |
. . . . . . . . . 10
β’ ((π β (UnifOnβπ) β§ π β π) β Rel π) |
32 | 28, 30, 31 | syl2anc 585 |
. . . . . . . . 9
β’
(((((π β
(UnifOnβπ) β§
π β (π Γ π)) β§ (π β π β§ β‘π = π)) β§ π§ β ((clsβ(π½ Γt π½))βπ)) β§ π β (((π β {(1st βπ§)}) Γ (π β {(2nd βπ§)})) β© π)) β Rel π) |
33 | | simpr 486 |
. . . . . . . . . . . 12
β’
(((((π β
(UnifOnβπ) β§
π β (π Γ π)) β§ (π β π β§ β‘π = π)) β§ π§ β ((clsβ(π½ Γt π½))βπ)) β§ π β (((π β {(1st βπ§)}) Γ (π β {(2nd βπ§)})) β© π)) β π β (((π β {(1st βπ§)}) Γ (π β {(2nd βπ§)})) β© π)) |
34 | | elin 3965 |
. . . . . . . . . . . 12
β’ (π β (((π β {(1st βπ§)}) Γ (π β {(2nd βπ§)})) β© π) β (π β ((π β {(1st βπ§)}) Γ (π β {(2nd βπ§)})) β§ π β π)) |
35 | 33, 34 | sylib 217 |
. . . . . . . . . . 11
β’
(((((π β
(UnifOnβπ) β§
π β (π Γ π)) β§ (π β π β§ β‘π = π)) β§ π§ β ((clsβ(π½ Γt π½))βπ)) β§ π β (((π β {(1st βπ§)}) Γ (π β {(2nd βπ§)})) β© π)) β (π β ((π β {(1st βπ§)}) Γ (π β {(2nd βπ§)})) β§ π β π)) |
36 | 35 | simpld 496 |
. . . . . . . . . 10
β’
(((((π β
(UnifOnβπ) β§
π β (π Γ π)) β§ (π β π β§ β‘π = π)) β§ π§ β ((clsβ(π½ Γt π½))βπ)) β§ π β (((π β {(1st βπ§)}) Γ (π β {(2nd βπ§)})) β© π)) β π β ((π β {(1st βπ§)}) Γ (π β {(2nd βπ§)}))) |
37 | | xp1st 8007 |
. . . . . . . . . 10
β’ (π β ((π β {(1st βπ§)}) Γ (π β {(2nd βπ§)})) β (1st
βπ) β (π β {(1st
βπ§)})) |
38 | 36, 37 | syl 17 |
. . . . . . . . 9
β’
(((((π β
(UnifOnβπ) β§
π β (π Γ π)) β§ (π β π β§ β‘π = π)) β§ π§ β ((clsβ(π½ Γt π½))βπ)) β§ π β (((π β {(1st βπ§)}) Γ (π β {(2nd βπ§)})) β© π)) β (1st βπ) β (π β {(1st βπ§)})) |
39 | | elrelimasn 6085 |
. . . . . . . . . 10
β’ (Rel
π β ((1st
βπ) β (π β {(1st
βπ§)}) β
(1st βπ§)π(1st βπ))) |
40 | 39 | biimpa 478 |
. . . . . . . . 9
β’ ((Rel
π β§ (1st
βπ) β (π β {(1st
βπ§)})) β
(1st βπ§)π(1st βπ)) |
41 | 32, 38, 40 | syl2anc 585 |
. . . . . . . 8
β’
(((((π β
(UnifOnβπ) β§
π β (π Γ π)) β§ (π β π β§ β‘π = π)) β§ π§ β ((clsβ(π½ Γt π½))βπ)) β§ π β (((π β {(1st βπ§)}) Γ (π β {(2nd βπ§)})) β© π)) β (1st βπ§)π(1st βπ)) |
42 | | simp-4r 783 |
. . . . . . . . . . 11
β’
(((((π β
(UnifOnβπ) β§
π β (π Γ π)) β§ (π β π β§ β‘π = π)) β§ π§ β ((clsβ(π½ Γt π½))βπ)) β§ π β (((π β {(1st βπ§)}) Γ (π β {(2nd βπ§)})) β© π)) β π β (π Γ π)) |
43 | | xpss 5693 |
. . . . . . . . . . 11
β’ (π Γ π) β (V Γ V) |
44 | 42, 43 | sstrdi 3995 |
. . . . . . . . . 10
β’
(((((π β
(UnifOnβπ) β§
π β (π Γ π)) β§ (π β π β§ β‘π = π)) β§ π§ β ((clsβ(π½ Γt π½))βπ)) β§ π β (((π β {(1st βπ§)}) Γ (π β {(2nd βπ§)})) β© π)) β π β (V Γ V)) |
45 | | df-rel 5684 |
. . . . . . . . . 10
β’ (Rel
π β π β (V Γ V)) |
46 | 44, 45 | sylibr 233 |
. . . . . . . . 9
β’
(((((π β
(UnifOnβπ) β§
π β (π Γ π)) β§ (π β π β§ β‘π = π)) β§ π§ β ((clsβ(π½ Γt π½))βπ)) β§ π β (((π β {(1st βπ§)}) Γ (π β {(2nd βπ§)})) β© π)) β Rel π) |
47 | 35 | simprd 497 |
. . . . . . . . 9
β’
(((((π β
(UnifOnβπ) β§
π β (π Γ π)) β§ (π β π β§ β‘π = π)) β§ π§ β ((clsβ(π½ Γt π½))βπ)) β§ π β (((π β {(1st βπ§)}) Γ (π β {(2nd βπ§)})) β© π)) β π β π) |
48 | | 1st2ndbr 8028 |
. . . . . . . . 9
β’ ((Rel
π β§ π β π) β (1st βπ)π(2nd βπ)) |
49 | 46, 47, 48 | syl2anc 585 |
. . . . . . . 8
β’
(((((π β
(UnifOnβπ) β§
π β (π Γ π)) β§ (π β π β§ β‘π = π)) β§ π§ β ((clsβ(π½ Γt π½))βπ)) β§ π β (((π β {(1st βπ§)}) Γ (π β {(2nd βπ§)})) β© π)) β (1st βπ)π(2nd βπ)) |
50 | | xp2nd 8008 |
. . . . . . . . . . 11
β’ (π β ((π β {(1st βπ§)}) Γ (π β {(2nd βπ§)})) β (2nd
βπ) β (π β {(2nd
βπ§)})) |
51 | 36, 50 | syl 17 |
. . . . . . . . . 10
β’
(((((π β
(UnifOnβπ) β§
π β (π Γ π)) β§ (π β π β§ β‘π = π)) β§ π§ β ((clsβ(π½ Γt π½))βπ)) β§ π β (((π β {(1st βπ§)}) Γ (π β {(2nd βπ§)})) β© π)) β (2nd βπ) β (π β {(2nd βπ§)})) |
52 | | elrelimasn 6085 |
. . . . . . . . . . 11
β’ (Rel
π β ((2nd
βπ) β (π β {(2nd
βπ§)}) β
(2nd βπ§)π(2nd βπ))) |
53 | 52 | biimpa 478 |
. . . . . . . . . 10
β’ ((Rel
π β§ (2nd
βπ) β (π β {(2nd
βπ§)})) β
(2nd βπ§)π(2nd βπ)) |
54 | 32, 51, 53 | syl2anc 585 |
. . . . . . . . 9
β’
(((((π β
(UnifOnβπ) β§
π β (π Γ π)) β§ (π β π β§ β‘π = π)) β§ π§ β ((clsβ(π½ Γt π½))βπ)) β§ π β (((π β {(1st βπ§)}) Γ (π β {(2nd βπ§)})) β© π)) β (2nd βπ§)π(2nd βπ)) |
55 | | simpr1r 1232 |
. . . . . . . . . . 11
β’ (((π β (UnifOnβπ) β§ π β (π Γ π)) β§ ((π β π β§ β‘π = π) β§ π§ β ((clsβ(π½ Γt π½))βπ) β§ π β (((π β {(1st βπ§)}) Γ (π β {(2nd βπ§)})) β© π))) β β‘π = π) |
56 | 55 | 3anassrs 1361 |
. . . . . . . . . 10
β’
(((((π β
(UnifOnβπ) β§
π β (π Γ π)) β§ (π β π β§ β‘π = π)) β§ π§ β ((clsβ(π½ Γt π½))βπ)) β§ π β (((π β {(1st βπ§)}) Γ (π β {(2nd βπ§)})) β© π)) β β‘π = π) |
57 | | breq 5151 |
. . . . . . . . . . 11
β’ (β‘π = π β ((2nd βπ)β‘π(2nd βπ§) β (2nd βπ)π(2nd βπ§))) |
58 | | fvex 6905 |
. . . . . . . . . . . 12
β’
(2nd βπ) β V |
59 | | fvex 6905 |
. . . . . . . . . . . 12
β’
(2nd βπ§) β V |
60 | 58, 59 | brcnv 5883 |
. . . . . . . . . . 11
β’
((2nd βπ)β‘π(2nd βπ§) β (2nd βπ§)π(2nd βπ)) |
61 | 57, 60 | bitr3di 286 |
. . . . . . . . . 10
β’ (β‘π = π β ((2nd βπ)π(2nd βπ§) β (2nd βπ§)π(2nd βπ))) |
62 | 56, 61 | syl 17 |
. . . . . . . . 9
β’
(((((π β
(UnifOnβπ) β§
π β (π Γ π)) β§ (π β π β§ β‘π = π)) β§ π§ β ((clsβ(π½ Γt π½))βπ)) β§ π β (((π β {(1st βπ§)}) Γ (π β {(2nd βπ§)})) β© π)) β ((2nd βπ)π(2nd βπ§) β (2nd βπ§)π(2nd βπ))) |
63 | 54, 62 | mpbird 257 |
. . . . . . . 8
β’
(((((π β
(UnifOnβπ) β§
π β (π Γ π)) β§ (π β π β§ β‘π = π)) β§ π§ β ((clsβ(π½ Γt π½))βπ)) β§ π β (((π β {(1st βπ§)}) Γ (π β {(2nd βπ§)})) β© π)) β (2nd βπ)π(2nd βπ§)) |
64 | | fvex 6905 |
. . . . . . . . . 10
β’
(1st βπ§) β V |
65 | | fvex 6905 |
. . . . . . . . . 10
β’
(1st βπ) β V |
66 | | brcogw 5869 |
. . . . . . . . . . 11
β’
((((1st βπ§) β V β§ (2nd βπ) β V β§ (1st
βπ) β V) β§
((1st βπ§)π(1st βπ) β§ (1st βπ)π(2nd βπ))) β (1st βπ§)(π β π)(2nd βπ)) |
67 | 66 | ex 414 |
. . . . . . . . . 10
β’
(((1st βπ§) β V β§ (2nd βπ) β V β§ (1st
βπ) β V) β
(((1st βπ§)π(1st βπ) β§ (1st βπ)π(2nd βπ)) β (1st βπ§)(π β π)(2nd βπ))) |
68 | 64, 58, 65, 67 | mp3an 1462 |
. . . . . . . . 9
β’
(((1st βπ§)π(1st βπ) β§ (1st βπ)π(2nd βπ)) β (1st βπ§)(π β π)(2nd βπ)) |
69 | | brcogw 5869 |
. . . . . . . . . . 11
β’
((((1st βπ§) β V β§ (2nd βπ§) β V β§ (2nd
βπ) β V) β§
((1st βπ§)(π β π)(2nd βπ) β§ (2nd βπ)π(2nd βπ§))) β (1st βπ§)(π β (π β π))(2nd βπ§)) |
70 | 69 | ex 414 |
. . . . . . . . . 10
β’
(((1st βπ§) β V β§ (2nd βπ§) β V β§ (2nd
βπ) β V) β
(((1st βπ§)(π β π)(2nd βπ) β§ (2nd βπ)π(2nd βπ§)) β (1st βπ§)(π β (π β π))(2nd βπ§))) |
71 | 64, 59, 58, 70 | mp3an 1462 |
. . . . . . . . 9
β’
(((1st βπ§)(π β π)(2nd βπ) β§ (2nd βπ)π(2nd βπ§)) β (1st βπ§)(π β (π β π))(2nd βπ§)) |
72 | 68, 71 | sylan 581 |
. . . . . . . 8
β’
((((1st βπ§)π(1st βπ) β§ (1st βπ)π(2nd βπ)) β§ (2nd βπ)π(2nd βπ§)) β (1st βπ§)(π β (π β π))(2nd βπ§)) |
73 | 41, 49, 63, 72 | syl21anc 837 |
. . . . . . 7
β’
(((((π β
(UnifOnβπ) β§
π β (π Γ π)) β§ (π β π β§ β‘π = π)) β§ π§ β ((clsβ(π½ Γt π½))βπ)) β§ π β (((π β {(1st βπ§)}) Γ (π β {(2nd βπ§)})) β© π)) β (1st βπ§)(π β (π β π))(2nd βπ§)) |
74 | 73 | ralrimiva 3147 |
. . . . . 6
β’ ((((π β (UnifOnβπ) β§ π β (π Γ π)) β§ (π β π β§ β‘π = π)) β§ π§ β ((clsβ(π½ Γt π½))βπ)) β βπ β (((π β {(1st βπ§)}) Γ (π β {(2nd βπ§)})) β© π)(1st βπ§)(π β (π β π))(2nd βπ§)) |
75 | | simplll 774 |
. . . . . . . . 9
β’ ((((π β (UnifOnβπ) β§ π β (π Γ π)) β§ (π β π β§ β‘π = π)) β§ π§ β ((clsβ(π½ Γt π½))βπ)) β π β (UnifOnβπ)) |
76 | | simplrl 776 |
. . . . . . . . 9
β’ ((((π β (UnifOnβπ) β§ π β (π Γ π)) β§ (π β π β§ β‘π = π)) β§ π§ β ((clsβ(π½ Γt π½))βπ)) β π β π) |
77 | 4 | 3ad2ant1 1134 |
. . . . . . . . . . 11
β’ ((π β (UnifOnβπ) β§ π β π β§ π§ β (π Γ π)) β π½ β Top) |
78 | | xp1st 8007 |
. . . . . . . . . . . 12
β’ (π§ β (π Γ π) β (1st βπ§) β π) |
79 | 2 | utopsnnei 23754 |
. . . . . . . . . . . 12
β’ ((π β (UnifOnβπ) β§ π β π β§ (1st βπ§) β π) β (π β {(1st βπ§)}) β ((neiβπ½)β{(1st
βπ§)})) |
80 | 78, 79 | syl3an3 1166 |
. . . . . . . . . . 11
β’ ((π β (UnifOnβπ) β§ π β π β§ π§ β (π Γ π)) β (π β {(1st βπ§)}) β ((neiβπ½)β{(1st
βπ§)})) |
81 | | xp2nd 8008 |
. . . . . . . . . . . 12
β’ (π§ β (π Γ π) β (2nd βπ§) β π) |
82 | 2 | utopsnnei 23754 |
. . . . . . . . . . . 12
β’ ((π β (UnifOnβπ) β§ π β π β§ (2nd βπ§) β π) β (π β {(2nd βπ§)}) β ((neiβπ½)β{(2nd
βπ§)})) |
83 | 81, 82 | syl3an3 1166 |
. . . . . . . . . . 11
β’ ((π β (UnifOnβπ) β§ π β π β§ π§ β (π Γ π)) β (π β {(2nd βπ§)}) β ((neiβπ½)β{(2nd
βπ§)})) |
84 | 14, 14 | neitx 23111 |
. . . . . . . . . . 11
β’ (((π½ β Top β§ π½ β Top) β§ ((π β {(1st
βπ§)}) β
((neiβπ½)β{(1st βπ§)}) β§ (π β {(2nd βπ§)}) β ((neiβπ½)β{(2nd
βπ§)}))) β
((π β
{(1st βπ§)}) Γ (π β {(2nd βπ§)})) β ((neiβ(π½ Γt π½))β({(1st
βπ§)} Γ
{(2nd βπ§)}))) |
85 | 77, 77, 80, 83, 84 | syl22anc 838 |
. . . . . . . . . 10
β’ ((π β (UnifOnβπ) β§ π β π β§ π§ β (π Γ π)) β ((π β {(1st βπ§)}) Γ (π β {(2nd βπ§)})) β ((neiβ(π½ Γt π½))β({(1st
βπ§)} Γ
{(2nd βπ§)}))) |
86 | | 1st2nd2 8014 |
. . . . . . . . . . . . . 14
β’ (π§ β (π Γ π) β π§ = β¨(1st βπ§), (2nd βπ§)β©) |
87 | 86 | sneqd 4641 |
. . . . . . . . . . . . 13
β’ (π§ β (π Γ π) β {π§} = {β¨(1st βπ§), (2nd βπ§)β©}) |
88 | 64, 59 | xpsn 7139 |
. . . . . . . . . . . . 13
β’
({(1st βπ§)} Γ {(2nd βπ§)}) = {β¨(1st
βπ§), (2nd
βπ§)β©} |
89 | 87, 88 | eqtr4di 2791 |
. . . . . . . . . . . 12
β’ (π§ β (π Γ π) β {π§} = ({(1st βπ§)} Γ {(2nd
βπ§)})) |
90 | 89 | fveq2d 6896 |
. . . . . . . . . . 11
β’ (π§ β (π Γ π) β ((neiβ(π½ Γt π½))β{π§}) = ((neiβ(π½ Γt π½))β({(1st βπ§)} Γ {(2nd
βπ§)}))) |
91 | 90 | 3ad2ant3 1136 |
. . . . . . . . . 10
β’ ((π β (UnifOnβπ) β§ π β π β§ π§ β (π Γ π)) β ((neiβ(π½ Γt π½))β{π§}) = ((neiβ(π½ Γt π½))β({(1st βπ§)} Γ {(2nd
βπ§)}))) |
92 | 85, 91 | eleqtrrd 2837 |
. . . . . . . . 9
β’ ((π β (UnifOnβπ) β§ π β π β§ π§ β (π Γ π)) β ((π β {(1st βπ§)}) Γ (π β {(2nd βπ§)})) β ((neiβ(π½ Γt π½))β{π§})) |
93 | 75, 76, 25, 92 | syl3anc 1372 |
. . . . . . . 8
β’ ((((π β (UnifOnβπ) β§ π β (π Γ π)) β§ (π β π β§ β‘π = π)) β§ π§ β ((clsβ(π½ Γt π½))βπ)) β ((π β {(1st βπ§)}) Γ (π β {(2nd βπ§)})) β ((neiβ(π½ Γt π½))β{π§})) |
94 | 20 | neindisj 22621 |
. . . . . . . 8
β’ ((((π½ Γt π½) β Top β§ π β βͺ (π½
Γt π½))
β§ (π§ β
((clsβ(π½
Γt π½))βπ) β§ ((π β {(1st βπ§)}) Γ (π β {(2nd βπ§)})) β ((neiβ(π½ Γt π½))β{π§}))) β (((π β {(1st βπ§)}) Γ (π β {(2nd βπ§)})) β© π) β β
) |
95 | 7, 19, 24, 93, 94 | syl22anc 838 |
. . . . . . 7
β’ ((((π β (UnifOnβπ) β§ π β (π Γ π)) β§ (π β π β§ β‘π = π)) β§ π§ β ((clsβ(π½ Γt π½))βπ)) β (((π β {(1st βπ§)}) Γ (π β {(2nd βπ§)})) β© π) β β
) |
96 | | r19.3rzv 4499 |
. . . . . . 7
β’ ((((π β {(1st
βπ§)}) Γ (π β {(2nd
βπ§)})) β© π) β β
β
((1st βπ§)(π β (π β π))(2nd βπ§) β βπ β (((π β {(1st βπ§)}) Γ (π β {(2nd βπ§)})) β© π)(1st βπ§)(π β (π β π))(2nd βπ§))) |
97 | 95, 96 | syl 17 |
. . . . . 6
β’ ((((π β (UnifOnβπ) β§ π β (π Γ π)) β§ (π β π β§ β‘π = π)) β§ π§ β ((clsβ(π½ Γt π½))βπ)) β ((1st βπ§)(π β (π β π))(2nd βπ§) β βπ β (((π β {(1st βπ§)}) Γ (π β {(2nd βπ§)})) β© π)(1st βπ§)(π β (π β π))(2nd βπ§))) |
98 | 74, 97 | mpbird 257 |
. . . . 5
β’ ((((π β (UnifOnβπ) β§ π β (π Γ π)) β§ (π β π β§ β‘π = π)) β§ π§ β ((clsβ(π½ Γt π½))βπ)) β (1st βπ§)(π β (π β π))(2nd βπ§)) |
99 | | df-br 5150 |
. . . . 5
β’
((1st βπ§)(π β (π β π))(2nd βπ§) β β¨(1st βπ§), (2nd βπ§)β© β (π β (π β π))) |
100 | 98, 99 | sylib 217 |
. . . 4
β’ ((((π β (UnifOnβπ) β§ π β (π Γ π)) β§ (π β π β§ β‘π = π)) β§ π§ β ((clsβ(π½ Γt π½))βπ)) β β¨(1st βπ§), (2nd βπ§)β© β (π β (π β π))) |
101 | 27, 100 | eqeltrd 2834 |
. . 3
β’ ((((π β (UnifOnβπ) β§ π β (π Γ π)) β§ (π β π β§ β‘π = π)) β§ π§ β ((clsβ(π½ Γt π½))βπ)) β π§ β (π β (π β π))) |
102 | 101 | ex 414 |
. 2
β’ (((π β (UnifOnβπ) β§ π β (π Γ π)) β§ (π β π β§ β‘π = π)) β (π§ β ((clsβ(π½ Γt π½))βπ) β π§ β (π β (π β π)))) |
103 | 102 | ssrdv 3989 |
1
β’ (((π β (UnifOnβπ) β§ π β (π Γ π)) β§ (π β π β§ β‘π = π)) β ((clsβ(π½ Γt π½))βπ) β (π β (π β π))) |