Step | Hyp | Ref
| Expression |
1 | | islptre.1 |
. . . . . 6
β’ π½ = (topGenβran
(,)) |
2 | | retopon 24130 |
. . . . . 6
β’
(topGenβran (,)) β (TopOnββ) |
3 | 1, 2 | eqeltri 2834 |
. . . . 5
β’ π½ β
(TopOnββ) |
4 | 3 | topontopi 22267 |
. . . 4
β’ π½ β Top |
5 | 4 | a1i 11 |
. . 3
β’ (π β π½ β Top) |
6 | | islptre.2 |
. . 3
β’ (π β π΄ β β) |
7 | | islptre.3 |
. . 3
β’ (π β π΅ β β) |
8 | 3 | toponunii 22268 |
. . . 4
β’ β =
βͺ π½ |
9 | 8 | islp2 22499 |
. . 3
β’ ((π½ β Top β§ π΄ β β β§ π΅ β β) β (π΅ β ((limPtβπ½)βπ΄) β βπ β ((neiβπ½)β{π΅})(π β© (π΄ β {π΅})) β β
)) |
10 | 5, 6, 7, 9 | syl3anc 1372 |
. 2
β’ (π β (π΅ β ((limPtβπ½)βπ΄) β βπ β ((neiβπ½)β{π΅})(π β© (π΄ β {π΅})) β β
)) |
11 | | simp1r 1199 |
. . . . . 6
β’ (((π β§ βπ β ((neiβπ½)β{π΅})(π β© (π΄ β {π΅})) β β
) β§ (π β β* β§ π β β*)
β§ π΅ β (π(,)π)) β βπ β ((neiβπ½)β{π΅})(π β© (π΄ β {π΅})) β β
) |
12 | | iooretop 24132 |
. . . . . . . . . . . 12
β’ (π(,)π) β (topGenβran
(,)) |
13 | 12, 1 | eleqtrri 2837 |
. . . . . . . . . . 11
β’ (π(,)π) β π½ |
14 | 13 | a1i 11 |
. . . . . . . . . 10
β’ (((π β β*
β§ π β
β*) β§ π΅ β (π(,)π)) β (π(,)π) β π½) |
15 | | snssi 4769 |
. . . . . . . . . . 11
β’ (π΅ β (π(,)π) β {π΅} β (π(,)π)) |
16 | 15 | adantl 483 |
. . . . . . . . . 10
β’ (((π β β*
β§ π β
β*) β§ π΅ β (π(,)π)) β {π΅} β (π(,)π)) |
17 | | ssidd 3968 |
. . . . . . . . . 10
β’ (((π β β*
β§ π β
β*) β§ π΅ β (π(,)π)) β (π(,)π) β (π(,)π)) |
18 | | sseq2 3971 |
. . . . . . . . . . . 12
β’ (π£ = (π(,)π) β ({π΅} β π£ β {π΅} β (π(,)π))) |
19 | | sseq1 3970 |
. . . . . . . . . . . 12
β’ (π£ = (π(,)π) β (π£ β (π(,)π) β (π(,)π) β (π(,)π))) |
20 | 18, 19 | anbi12d 632 |
. . . . . . . . . . 11
β’ (π£ = (π(,)π) β (({π΅} β π£ β§ π£ β (π(,)π)) β ({π΅} β (π(,)π) β§ (π(,)π) β (π(,)π)))) |
21 | 20 | rspcev 3582 |
. . . . . . . . . 10
β’ (((π(,)π) β π½ β§ ({π΅} β (π(,)π) β§ (π(,)π) β (π(,)π))) β βπ£ β π½ ({π΅} β π£ β§ π£ β (π(,)π))) |
22 | 14, 16, 17, 21 | syl12anc 836 |
. . . . . . . . 9
β’ (((π β β*
β§ π β
β*) β§ π΅ β (π(,)π)) β βπ£ β π½ ({π΅} β π£ β§ π£ β (π(,)π))) |
23 | | ioossre 13326 |
. . . . . . . . 9
β’ (π(,)π) β β |
24 | 22, 23 | jctil 521 |
. . . . . . . 8
β’ (((π β β*
β§ π β
β*) β§ π΅ β (π(,)π)) β ((π(,)π) β β β§ βπ£ β π½ ({π΅} β π£ β§ π£ β (π(,)π)))) |
25 | | elioore 13295 |
. . . . . . . . . . 11
β’ (π΅ β (π(,)π) β π΅ β β) |
26 | 25 | snssd 4770 |
. . . . . . . . . 10
β’ (π΅ β (π(,)π) β {π΅} β β) |
27 | 26 | adantl 483 |
. . . . . . . . 9
β’ (((π β β*
β§ π β
β*) β§ π΅ β (π(,)π)) β {π΅} β β) |
28 | 8 | isnei 22457 |
. . . . . . . . 9
β’ ((π½ β Top β§ {π΅} β β) β
((π(,)π) β ((neiβπ½)β{π΅}) β ((π(,)π) β β β§ βπ£ β π½ ({π΅} β π£ β§ π£ β (π(,)π))))) |
29 | 4, 27, 28 | sylancr 588 |
. . . . . . . 8
β’ (((π β β*
β§ π β
β*) β§ π΅ β (π(,)π)) β ((π(,)π) β ((neiβπ½)β{π΅}) β ((π(,)π) β β β§ βπ£ β π½ ({π΅} β π£ β§ π£ β (π(,)π))))) |
30 | 24, 29 | mpbird 257 |
. . . . . . 7
β’ (((π β β*
β§ π β
β*) β§ π΅ β (π(,)π)) β (π(,)π) β ((neiβπ½)β{π΅})) |
31 | 30 | 3adant1 1131 |
. . . . . 6
β’ (((π β§ βπ β ((neiβπ½)β{π΅})(π β© (π΄ β {π΅})) β β
) β§ (π β β* β§ π β β*)
β§ π΅ β (π(,)π)) β (π(,)π) β ((neiβπ½)β{π΅})) |
32 | | ineq1 4166 |
. . . . . . . 8
β’ (π = (π(,)π) β (π β© (π΄ β {π΅})) = ((π(,)π) β© (π΄ β {π΅}))) |
33 | 32 | neeq1d 3004 |
. . . . . . 7
β’ (π = (π(,)π) β ((π β© (π΄ β {π΅})) β β
β ((π(,)π) β© (π΄ β {π΅})) β β
)) |
34 | 33 | rspccva 3581 |
. . . . . 6
β’
((βπ β
((neiβπ½)β{π΅})(π β© (π΄ β {π΅})) β β
β§ (π(,)π) β ((neiβπ½)β{π΅})) β ((π(,)π) β© (π΄ β {π΅})) β β
) |
35 | 11, 31, 34 | syl2anc 585 |
. . . . 5
β’ (((π β§ βπ β ((neiβπ½)β{π΅})(π β© (π΄ β {π΅})) β β
) β§ (π β β* β§ π β β*)
β§ π΅ β (π(,)π)) β ((π(,)π) β© (π΄ β {π΅})) β β
) |
36 | 35 | 3exp 1120 |
. . . 4
β’ ((π β§ βπ β ((neiβπ½)β{π΅})(π β© (π΄ β {π΅})) β β
) β ((π β β*
β§ π β
β*) β (π΅ β (π(,)π) β ((π(,)π) β© (π΄ β {π΅})) β β
))) |
37 | 36 | ralrimivv 3196 |
. . 3
β’ ((π β§ βπ β ((neiβπ½)β{π΅})(π β© (π΄ β {π΅})) β β
) β βπ β β*
βπ β
β* (π΅
β (π(,)π) β ((π(,)π) β© (π΄ β {π΅})) β β
)) |
38 | 7 | snssd 4770 |
. . . . . . . . 9
β’ (π β {π΅} β β) |
39 | 8 | isnei 22457 |
. . . . . . . . 9
β’ ((π½ β Top β§ {π΅} β β) β (π β ((neiβπ½)β{π΅}) β (π β β β§ βπ£ β π½ ({π΅} β π£ β§ π£ β π)))) |
40 | 4, 38, 39 | sylancr 588 |
. . . . . . . 8
β’ (π β (π β ((neiβπ½)β{π΅}) β (π β β β§ βπ£ β π½ ({π΅} β π£ β§ π£ β π)))) |
41 | 40 | simplbda 501 |
. . . . . . 7
β’ ((π β§ π β ((neiβπ½)β{π΅})) β βπ£ β π½ ({π΅} β π£ β§ π£ β π)) |
42 | 1 | eleq2i 2830 |
. . . . . . . . . . . . . . 15
β’ (π£ β π½ β π£ β (topGenβran
(,))) |
43 | 42 | biimpi 215 |
. . . . . . . . . . . . . 14
β’ (π£ β π½ β π£ β (topGenβran
(,))) |
44 | 43 | 3ad2ant2 1135 |
. . . . . . . . . . . . 13
β’ ((π β§ π£ β π½ β§ ({π΅} β π£ β§ π£ β π)) β π£ β (topGenβran
(,))) |
45 | | simp1 1137 |
. . . . . . . . . . . . . 14
β’ ((π β§ π£ β π½ β§ ({π΅} β π£ β§ π£ β π)) β π) |
46 | | simp3l 1202 |
. . . . . . . . . . . . . 14
β’ ((π β§ π£ β π½ β§ ({π΅} β π£ β§ π£ β π)) β {π΅} β π£) |
47 | | simpr 486 |
. . . . . . . . . . . . . . 15
β’ ((π β§ {π΅} β π£) β {π΅} β π£) |
48 | 7 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ {π΅} β π£) β π΅ β β) |
49 | | snssg 4745 |
. . . . . . . . . . . . . . . 16
β’ (π΅ β β β (π΅ β π£ β {π΅} β π£)) |
50 | 48, 49 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((π β§ {π΅} β π£) β (π΅ β π£ β {π΅} β π£)) |
51 | 47, 50 | mpbird 257 |
. . . . . . . . . . . . . 14
β’ ((π β§ {π΅} β π£) β π΅ β π£) |
52 | 45, 46, 51 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((π β§ π£ β π½ β§ ({π΅} β π£ β§ π£ β π)) β π΅ β π£) |
53 | 44, 52 | jca 513 |
. . . . . . . . . . . 12
β’ ((π β§ π£ β π½ β§ ({π΅} β π£ β§ π£ β π)) β (π£ β (topGenβran (,)) β§ π΅ β π£)) |
54 | | tg2 22318 |
. . . . . . . . . . . 12
β’ ((π£ β (topGenβran (,))
β§ π΅ β π£) β βπ’ β ran (,)(π΅ β π’ β§ π’ β π£)) |
55 | | ioof 13365 |
. . . . . . . . . . . . . . . . 17
β’
(,):(β* Γ β*)βΆπ«
β |
56 | | ffn 6669 |
. . . . . . . . . . . . . . . . 17
β’
((,):(β* Γ β*)βΆπ«
β β (,) Fn (β* Γ
β*)) |
57 | | ovelrn 7531 |
. . . . . . . . . . . . . . . . 17
β’ ((,) Fn
(β* Γ β*) β (π’ β ran (,) β βπ β β*
βπ β
β* π’ =
(π(,)π))) |
58 | 55, 56, 57 | mp2b 10 |
. . . . . . . . . . . . . . . 16
β’ (π’ β ran (,) β
βπ β
β* βπ β β* π’ = (π(,)π)) |
59 | 58 | biimpi 215 |
. . . . . . . . . . . . . . 15
β’ (π’ β ran (,) β
βπ β
β* βπ β β* π’ = (π(,)π)) |
60 | 59 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π’ β ran (,) β§ (π΅ β π’ β§ π’ β π£)) β βπ β β* βπ β β*
π’ = (π(,)π)) |
61 | | simpll 766 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π΅ β π’ β§ π’ β π£) β§ π’ = (π(,)π)) β π΅ β π’) |
62 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π΅ β π’ β§ π’ β π£) β§ π’ = (π(,)π)) β π’ = (π(,)π)) |
63 | 61, 62 | eleqtrd 2840 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π΅ β π’ β§ π’ β π£) β§ π’ = (π(,)π)) β π΅ β (π(,)π)) |
64 | | simplr 768 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π΅ β π’ β§ π’ β π£) β§ π’ = (π(,)π)) β π’ β π£) |
65 | 62, 64 | eqsstrrd 3984 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π΅ β π’ β§ π’ β π£) β§ π’ = (π(,)π)) β (π(,)π) β π£) |
66 | 63, 65 | jca 513 |
. . . . . . . . . . . . . . . . . 18
β’ (((π΅ β π’ β§ π’ β π£) β§ π’ = (π(,)π)) β (π΅ β (π(,)π) β§ (π(,)π) β π£)) |
67 | 66 | ex 414 |
. . . . . . . . . . . . . . . . 17
β’ ((π΅ β π’ β§ π’ β π£) β (π’ = (π(,)π) β (π΅ β (π(,)π) β§ (π(,)π) β π£))) |
68 | 67 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ ((π’ β ran (,) β§ (π΅ β π’ β§ π’ β π£)) β (π’ = (π(,)π) β (π΅ β (π(,)π) β§ (π(,)π) β π£))) |
69 | 68 | reximdv 3168 |
. . . . . . . . . . . . . . 15
β’ ((π’ β ran (,) β§ (π΅ β π’ β§ π’ β π£)) β (βπ β β* π’ = (π(,)π) β βπ β β* (π΅ β (π(,)π) β§ (π(,)π) β π£))) |
70 | 69 | reximdv 3168 |
. . . . . . . . . . . . . 14
β’ ((π’ β ran (,) β§ (π΅ β π’ β§ π’ β π£)) β (βπ β β* βπ β β*
π’ = (π(,)π) β βπ β β* βπ β β*
(π΅ β (π(,)π) β§ (π(,)π) β π£))) |
71 | 60, 70 | mpd 15 |
. . . . . . . . . . . . 13
β’ ((π’ β ran (,) β§ (π΅ β π’ β§ π’ β π£)) β βπ β β* βπ β β*
(π΅ β (π(,)π) β§ (π(,)π) β π£)) |
72 | 71 | rexlimiva 3145 |
. . . . . . . . . . . 12
β’
(βπ’ β ran
(,)(π΅ β π’ β§ π’ β π£) β βπ β β* βπ β β*
(π΅ β (π(,)π) β§ (π(,)π) β π£)) |
73 | 53, 54, 72 | 3syl 18 |
. . . . . . . . . . 11
β’ ((π β§ π£ β π½ β§ ({π΅} β π£ β§ π£ β π)) β βπ β β* βπ β β*
(π΅ β (π(,)π) β§ (π(,)π) β π£)) |
74 | | simpl3r 1230 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π£ β π½ β§ ({π΅} β π£ β§ π£ β π)) β§ π β β*) β π£ β π) |
75 | 74 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π£ β π½ β§ ({π΅} β π£ β§ π£ β π)) β§ π β β*) β§ π β β*)
β π£ β π) |
76 | | sstr 3953 |
. . . . . . . . . . . . . . . 16
β’ (((π(,)π) β π£ β§ π£ β π) β (π(,)π) β π) |
77 | 76 | expcom 415 |
. . . . . . . . . . . . . . 15
β’ (π£ β π β ((π(,)π) β π£ β (π(,)π) β π)) |
78 | 75, 77 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π£ β π½ β§ ({π΅} β π£ β§ π£ β π)) β§ π β β*) β§ π β β*)
β ((π(,)π) β π£ β (π(,)π) β π)) |
79 | 78 | anim2d 613 |
. . . . . . . . . . . . 13
β’ ((((π β§ π£ β π½ β§ ({π΅} β π£ β§ π£ β π)) β§ π β β*) β§ π β β*)
β ((π΅ β (π(,)π) β§ (π(,)π) β π£) β (π΅ β (π(,)π) β§ (π(,)π) β π))) |
80 | 79 | reximdva 3166 |
. . . . . . . . . . . 12
β’ (((π β§ π£ β π½ β§ ({π΅} β π£ β§ π£ β π)) β§ π β β*) β
(βπ β
β* (π΅
β (π(,)π) β§ (π(,)π) β π£) β βπ β β* (π΅ β (π(,)π) β§ (π(,)π) β π))) |
81 | 80 | reximdva 3166 |
. . . . . . . . . . 11
β’ ((π β§ π£ β π½ β§ ({π΅} β π£ β§ π£ β π)) β (βπ β β* βπ β β*
(π΅ β (π(,)π) β§ (π(,)π) β π£) β βπ β β* βπ β β*
(π΅ β (π(,)π) β§ (π(,)π) β π))) |
82 | 73, 81 | mpd 15 |
. . . . . . . . . 10
β’ ((π β§ π£ β π½ β§ ({π΅} β π£ β§ π£ β π)) β βπ β β* βπ β β*
(π΅ β (π(,)π) β§ (π(,)π) β π)) |
83 | 82 | 3exp 1120 |
. . . . . . . . 9
β’ (π β (π£ β π½ β (({π΅} β π£ β§ π£ β π) β βπ β β* βπ β β*
(π΅ β (π(,)π) β§ (π(,)π) β π)))) |
84 | 83 | rexlimdv 3151 |
. . . . . . . 8
β’ (π β (βπ£ β π½ ({π΅} β π£ β§ π£ β π) β βπ β β* βπ β β*
(π΅ β (π(,)π) β§ (π(,)π) β π))) |
85 | 84 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β ((neiβπ½)β{π΅})) β (βπ£ β π½ ({π΅} β π£ β§ π£ β π) β βπ β β* βπ β β*
(π΅ β (π(,)π) β§ (π(,)π) β π))) |
86 | 41, 85 | mpd 15 |
. . . . . 6
β’ ((π β§ π β ((neiβπ½)β{π΅})) β βπ β β* βπ β β*
(π΅ β (π(,)π) β§ (π(,)π) β π)) |
87 | 86 | adantlr 714 |
. . . . 5
β’ (((π β§ βπ β β* βπ β β*
(π΅ β (π(,)π) β ((π(,)π) β© (π΄ β {π΅})) β β
)) β§ π β ((neiβπ½)β{π΅})) β βπ β β* βπ β β*
(π΅ β (π(,)π) β§ (π(,)π) β π)) |
88 | | nfv 1918 |
. . . . . . . 8
β’
β²ππ |
89 | | nfra1 3268 |
. . . . . . . 8
β’
β²πβπ β β* βπ β β*
(π΅ β (π(,)π) β ((π(,)π) β© (π΄ β {π΅})) β β
) |
90 | 88, 89 | nfan 1903 |
. . . . . . 7
β’
β²π(π β§ βπ β β* βπ β β*
(π΅ β (π(,)π) β ((π(,)π) β© (π΄ β {π΅})) β β
)) |
91 | | nfv 1918 |
. . . . . . 7
β’
β²π π β ((neiβπ½)β{π΅}) |
92 | 90, 91 | nfan 1903 |
. . . . . 6
β’
β²π((π β§ βπ β β* βπ β β*
(π΅ β (π(,)π) β ((π(,)π) β© (π΄ β {π΅})) β β
)) β§ π β ((neiβπ½)β{π΅})) |
93 | | nfv 1918 |
. . . . . 6
β’
β²π(π β© (π΄ β {π΅})) β β
|
94 | | nfv 1918 |
. . . . . . . . . . 11
β’
β²ππ |
95 | | nfra2w 3283 |
. . . . . . . . . . 11
β’
β²πβπ β β* βπ β β*
(π΅ β (π(,)π) β ((π(,)π) β© (π΄ β {π΅})) β β
) |
96 | 94, 95 | nfan 1903 |
. . . . . . . . . 10
β’
β²π(π β§ βπ β β* βπ β β*
(π΅ β (π(,)π) β ((π(,)π) β© (π΄ β {π΅})) β β
)) |
97 | | nfv 1918 |
. . . . . . . . . 10
β’
β²π π β ((neiβπ½)β{π΅}) |
98 | 96, 97 | nfan 1903 |
. . . . . . . . 9
β’
β²π((π β§ βπ β β* βπ β β*
(π΅ β (π(,)π) β ((π(,)π) β© (π΄ β {π΅})) β β
)) β§ π β ((neiβπ½)β{π΅})) |
99 | | nfv 1918 |
. . . . . . . . 9
β’
β²π π β
β* |
100 | 98, 99 | nfan 1903 |
. . . . . . . 8
β’
β²π(((π β§ βπ β β* βπ β β*
(π΅ β (π(,)π) β ((π(,)π) β© (π΄ β {π΅})) β β
)) β§ π β ((neiβπ½)β{π΅})) β§ π β β*) |
101 | | nfv 1918 |
. . . . . . . 8
β’
β²π(π β© (π΄ β {π΅})) β β
|
102 | | inss1 4189 |
. . . . . . . . . . . 12
β’ ((π(,)π) β© (π΄ β {π΅})) β (π(,)π) |
103 | | simp3r 1203 |
. . . . . . . . . . . 12
β’
(((((π β§
βπ β
β* βπ β β* (π΅ β (π(,)π) β ((π(,)π) β© (π΄ β {π΅})) β β
)) β§ π β ((neiβπ½)β{π΅})) β§ π β β*) β§ π β β*
β§ (π΅ β (π(,)π) β§ (π(,)π) β π)) β (π(,)π) β π) |
104 | 102, 103 | sstrid 3956 |
. . . . . . . . . . 11
β’
(((((π β§
βπ β
β* βπ β β* (π΅ β (π(,)π) β ((π(,)π) β© (π΄ β {π΅})) β β
)) β§ π β ((neiβπ½)β{π΅})) β§ π β β*) β§ π β β*
β§ (π΅ β (π(,)π) β§ (π(,)π) β π)) β ((π(,)π) β© (π΄ β {π΅})) β π) |
105 | | inss2 4190 |
. . . . . . . . . . . 12
β’ ((π(,)π) β© (π΄ β {π΅})) β (π΄ β {π΅}) |
106 | 105 | a1i 11 |
. . . . . . . . . . 11
β’
(((((π β§
βπ β
β* βπ β β* (π΅ β (π(,)π) β ((π(,)π) β© (π΄ β {π΅})) β β
)) β§ π β ((neiβπ½)β{π΅})) β§ π β β*) β§ π β β*
β§ (π΅ β (π(,)π) β§ (π(,)π) β π)) β ((π(,)π) β© (π΄ β {π΅})) β (π΄ β {π΅})) |
107 | 104, 106 | ssind 4193 |
. . . . . . . . . 10
β’
(((((π β§
βπ β
β* βπ β β* (π΅ β (π(,)π) β ((π(,)π) β© (π΄ β {π΅})) β β
)) β§ π β ((neiβπ½)β{π΅})) β§ π β β*) β§ π β β*
β§ (π΅ β (π(,)π) β§ (π(,)π) β π)) β ((π(,)π) β© (π΄ β {π΅})) β (π β© (π΄ β {π΅}))) |
108 | | simpllr 775 |
. . . . . . . . . . . 12
β’ ((((π β§ βπ β β* βπ β β*
(π΅ β (π(,)π) β ((π(,)π) β© (π΄ β {π΅})) β β
)) β§ π β ((neiβπ½)β{π΅})) β§ π β β*) β
βπ β
β* βπ β β* (π΅ β (π(,)π) β ((π(,)π) β© (π΄ β {π΅})) β β
)) |
109 | 108 | 3ad2ant1 1134 |
. . . . . . . . . . 11
β’
(((((π β§
βπ β
β* βπ β β* (π΅ β (π(,)π) β ((π(,)π) β© (π΄ β {π΅})) β β
)) β§ π β ((neiβπ½)β{π΅})) β§ π β β*) β§ π β β*
β§ (π΅ β (π(,)π) β§ (π(,)π) β π)) β βπ β β* βπ β β*
(π΅ β (π(,)π) β ((π(,)π) β© (π΄ β {π΅})) β β
)) |
110 | | simp1r 1199 |
. . . . . . . . . . . 12
β’
(((((π β§
βπ β
β* βπ β β* (π΅ β (π(,)π) β ((π(,)π) β© (π΄ β {π΅})) β β
)) β§ π β ((neiβπ½)β{π΅})) β§ π β β*) β§ π β β*
β§ (π΅ β (π(,)π) β§ (π(,)π) β π)) β π β β*) |
111 | | simp2 1138 |
. . . . . . . . . . . 12
β’
(((((π β§
βπ β
β* βπ β β* (π΅ β (π(,)π) β ((π(,)π) β© (π΄ β {π΅})) β β
)) β§ π β ((neiβπ½)β{π΅})) β§ π β β*) β§ π β β*
β§ (π΅ β (π(,)π) β§ (π(,)π) β π)) β π β β*) |
112 | 110, 111 | jca 513 |
. . . . . . . . . . 11
β’
(((((π β§
βπ β
β* βπ β β* (π΅ β (π(,)π) β ((π(,)π) β© (π΄ β {π΅})) β β
)) β§ π β ((neiβπ½)β{π΅})) β§ π β β*) β§ π β β*
β§ (π΅ β (π(,)π) β§ (π(,)π) β π)) β (π β β* β§ π β
β*)) |
113 | | simp3l 1202 |
. . . . . . . . . . 11
β’
(((((π β§
βπ β
β* βπ β β* (π΅ β (π(,)π) β ((π(,)π) β© (π΄ β {π΅})) β β
)) β§ π β ((neiβπ½)β{π΅})) β§ π β β*) β§ π β β*
β§ (π΅ β (π(,)π) β§ (π(,)π) β π)) β π΅ β (π(,)π)) |
114 | | rsp2 3261 |
. . . . . . . . . . 11
β’
(βπ β
β* βπ β β* (π΅ β (π(,)π) β ((π(,)π) β© (π΄ β {π΅})) β β
) β ((π β β*
β§ π β
β*) β (π΅ β (π(,)π) β ((π(,)π) β© (π΄ β {π΅})) β β
))) |
115 | 109, 112,
113, 114 | syl3c 66 |
. . . . . . . . . 10
β’
(((((π β§
βπ β
β* βπ β β* (π΅ β (π(,)π) β ((π(,)π) β© (π΄ β {π΅})) β β
)) β§ π β ((neiβπ½)β{π΅})) β§ π β β*) β§ π β β*
β§ (π΅ β (π(,)π) β§ (π(,)π) β π)) β ((π(,)π) β© (π΄ β {π΅})) β β
) |
116 | | ssn0 4361 |
. . . . . . . . . 10
β’ ((((π(,)π) β© (π΄ β {π΅})) β (π β© (π΄ β {π΅})) β§ ((π(,)π) β© (π΄ β {π΅})) β β
) β (π β© (π΄ β {π΅})) β β
) |
117 | 107, 115,
116 | syl2anc 585 |
. . . . . . . . 9
β’
(((((π β§
βπ β
β* βπ β β* (π΅ β (π(,)π) β ((π(,)π) β© (π΄ β {π΅})) β β
)) β§ π β ((neiβπ½)β{π΅})) β§ π β β*) β§ π β β*
β§ (π΅ β (π(,)π) β§ (π(,)π) β π)) β (π β© (π΄ β {π΅})) β β
) |
118 | 117 | 3exp 1120 |
. . . . . . . 8
β’ ((((π β§ βπ β β* βπ β β*
(π΅ β (π(,)π) β ((π(,)π) β© (π΄ β {π΅})) β β
)) β§ π β ((neiβπ½)β{π΅})) β§ π β β*) β (π β β*
β ((π΅ β (π(,)π) β§ (π(,)π) β π) β (π β© (π΄ β {π΅})) β β
))) |
119 | 100, 101,
118 | rexlimd 3250 |
. . . . . . 7
β’ ((((π β§ βπ β β* βπ β β*
(π΅ β (π(,)π) β ((π(,)π) β© (π΄ β {π΅})) β β
)) β§ π β ((neiβπ½)β{π΅})) β§ π β β*) β
(βπ β
β* (π΅
β (π(,)π) β§ (π(,)π) β π) β (π β© (π΄ β {π΅})) β β
)) |
120 | 119 | ex 414 |
. . . . . 6
β’ (((π β§ βπ β β* βπ β β*
(π΅ β (π(,)π) β ((π(,)π) β© (π΄ β {π΅})) β β
)) β§ π β ((neiβπ½)β{π΅})) β (π β β* β
(βπ β
β* (π΅
β (π(,)π) β§ (π(,)π) β π) β (π β© (π΄ β {π΅})) β β
))) |
121 | 92, 93, 120 | rexlimd 3250 |
. . . . 5
β’ (((π β§ βπ β β* βπ β β*
(π΅ β (π(,)π) β ((π(,)π) β© (π΄ β {π΅})) β β
)) β§ π β ((neiβπ½)β{π΅})) β (βπ β β* βπ β β*
(π΅ β (π(,)π) β§ (π(,)π) β π) β (π β© (π΄ β {π΅})) β β
)) |
122 | 87, 121 | mpd 15 |
. . . 4
β’ (((π β§ βπ β β* βπ β β*
(π΅ β (π(,)π) β ((π(,)π) β© (π΄ β {π΅})) β β
)) β§ π β ((neiβπ½)β{π΅})) β (π β© (π΄ β {π΅})) β β
) |
123 | 122 | ralrimiva 3144 |
. . 3
β’ ((π β§ βπ β β* βπ β β*
(π΅ β (π(,)π) β ((π(,)π) β© (π΄ β {π΅})) β β
)) β βπ β ((neiβπ½)β{π΅})(π β© (π΄ β {π΅})) β β
) |
124 | 37, 123 | impbida 800 |
. 2
β’ (π β (βπ β ((neiβπ½)β{π΅})(π β© (π΄ β {π΅})) β β
β βπ β β*
βπ β
β* (π΅
β (π(,)π) β ((π(,)π) β© (π΄ β {π΅})) β β
))) |
125 | 10, 124 | bitrd 279 |
1
β’ (π β (π΅ β ((limPtβπ½)βπ΄) β βπ β β* βπ β β*
(π΅ β (π(,)π) β ((π(,)π) β© (π΄ β {π΅})) β β
))) |