Step | Hyp | Ref
| Expression |
1 | | simpl2 1190 |
. . . 4
β’ (((π½ β Top β§ πΎ β Top β§ π = π) β§ (π½ β πΎ β§ π₯ β ((neiβπ½)βπ))) β πΎ β Top) |
2 | | simprl 767 |
. . . . . 6
β’ (((π½ β Top β§ πΎ β Top β§ π = π) β§ (π½ β πΎ β§ π₯ β ((neiβπ½)βπ))) β π½ β πΎ) |
3 | | simpl1 1189 |
. . . . . . 7
β’ (((π½ β Top β§ πΎ β Top β§ π = π) β§ (π½ β πΎ β§ π₯ β ((neiβπ½)βπ))) β π½ β Top) |
4 | | simprr 769 |
. . . . . . . 8
β’ (((π½ β Top β§ πΎ β Top β§ π = π) β§ (π½ β πΎ β§ π₯ β ((neiβπ½)βπ))) β π₯ β ((neiβπ½)βπ)) |
5 | | tpnei.1 |
. . . . . . . . 9
β’ π = βͺ
π½ |
6 | 5 | neii1 22830 |
. . . . . . . 8
β’ ((π½ β Top β§ π₯ β ((neiβπ½)βπ)) β π₯ β π) |
7 | 3, 4, 6 | syl2anc 582 |
. . . . . . 7
β’ (((π½ β Top β§ πΎ β Top β§ π = π) β§ (π½ β πΎ β§ π₯ β ((neiβπ½)βπ))) β π₯ β π) |
8 | 5 | ntropn 22773 |
. . . . . . 7
β’ ((π½ β Top β§ π₯ β π) β ((intβπ½)βπ₯) β π½) |
9 | 3, 7, 8 | syl2anc 582 |
. . . . . 6
β’ (((π½ β Top β§ πΎ β Top β§ π = π) β§ (π½ β πΎ β§ π₯ β ((neiβπ½)βπ))) β ((intβπ½)βπ₯) β π½) |
10 | 2, 9 | sseldd 3982 |
. . . . 5
β’ (((π½ β Top β§ πΎ β Top β§ π = π) β§ (π½ β πΎ β§ π₯ β ((neiβπ½)βπ))) β ((intβπ½)βπ₯) β πΎ) |
11 | 5 | neiss2 22825 |
. . . . . . . 8
β’ ((π½ β Top β§ π₯ β ((neiβπ½)βπ)) β π β π) |
12 | 3, 4, 11 | syl2anc 582 |
. . . . . . 7
β’ (((π½ β Top β§ πΎ β Top β§ π = π) β§ (π½ β πΎ β§ π₯ β ((neiβπ½)βπ))) β π β π) |
13 | 5 | neiint 22828 |
. . . . . . 7
β’ ((π½ β Top β§ π β π β§ π₯ β π) β (π₯ β ((neiβπ½)βπ) β π β ((intβπ½)βπ₯))) |
14 | 3, 12, 7, 13 | syl3anc 1369 |
. . . . . 6
β’ (((π½ β Top β§ πΎ β Top β§ π = π) β§ (π½ β πΎ β§ π₯ β ((neiβπ½)βπ))) β (π₯ β ((neiβπ½)βπ) β π β ((intβπ½)βπ₯))) |
15 | 4, 14 | mpbid 231 |
. . . . 5
β’ (((π½ β Top β§ πΎ β Top β§ π = π) β§ (π½ β πΎ β§ π₯ β ((neiβπ½)βπ))) β π β ((intβπ½)βπ₯)) |
16 | | opnneiss 22842 |
. . . . 5
β’ ((πΎ β Top β§
((intβπ½)βπ₯) β πΎ β§ π β ((intβπ½)βπ₯)) β ((intβπ½)βπ₯) β ((neiβπΎ)βπ)) |
17 | 1, 10, 15, 16 | syl3anc 1369 |
. . . 4
β’ (((π½ β Top β§ πΎ β Top β§ π = π) β§ (π½ β πΎ β§ π₯ β ((neiβπ½)βπ))) β ((intβπ½)βπ₯) β ((neiβπΎ)βπ)) |
18 | 5 | ntrss2 22781 |
. . . . 5
β’ ((π½ β Top β§ π₯ β π) β ((intβπ½)βπ₯) β π₯) |
19 | 3, 7, 18 | syl2anc 582 |
. . . 4
β’ (((π½ β Top β§ πΎ β Top β§ π = π) β§ (π½ β πΎ β§ π₯ β ((neiβπ½)βπ))) β ((intβπ½)βπ₯) β π₯) |
20 | | simpl3 1191 |
. . . . 5
β’ (((π½ β Top β§ πΎ β Top β§ π = π) β§ (π½ β πΎ β§ π₯ β ((neiβπ½)βπ))) β π = π) |
21 | 7, 20 | sseqtrd 4021 |
. . . 4
β’ (((π½ β Top β§ πΎ β Top β§ π = π) β§ (π½ β πΎ β§ π₯ β ((neiβπ½)βπ))) β π₯ β π) |
22 | | topssnei.2 |
. . . . 5
β’ π = βͺ
πΎ |
23 | 22 | ssnei2 22840 |
. . . 4
β’ (((πΎ β Top β§
((intβπ½)βπ₯) β ((neiβπΎ)βπ)) β§ (((intβπ½)βπ₯) β π₯ β§ π₯ β π)) β π₯ β ((neiβπΎ)βπ)) |
24 | 1, 17, 19, 21, 23 | syl22anc 835 |
. . 3
β’ (((π½ β Top β§ πΎ β Top β§ π = π) β§ (π½ β πΎ β§ π₯ β ((neiβπ½)βπ))) β π₯ β ((neiβπΎ)βπ)) |
25 | 24 | expr 455 |
. 2
β’ (((π½ β Top β§ πΎ β Top β§ π = π) β§ π½ β πΎ) β (π₯ β ((neiβπ½)βπ) β π₯ β ((neiβπΎ)βπ))) |
26 | 25 | ssrdv 3987 |
1
β’ (((π½ β Top β§ πΎ β Top β§ π = π) β§ π½ β πΎ) β ((neiβπ½)βπ) β ((neiβπΎ)βπ)) |