Step | Hyp | Ref
| Expression |
1 | | ntrnei.o |
. . . . . . . . 9
β’ π = (π β V, π β V β¦ (π β (π« π βm π) β¦ (π β π β¦ {π β π β£ π β (πβπ)}))) |
2 | | ntrnei.f |
. . . . . . . . 9
β’ πΉ = (π« π΅ππ΅) |
3 | | ntrnei.r |
. . . . . . . . 9
β’ (π β πΌπΉπ) |
4 | 1, 2, 3 | ntrneiiex 42503 |
. . . . . . . 8
β’ (π β πΌ β (π« π΅ βm π« π΅)) |
5 | | elmapi 8809 |
. . . . . . . 8
β’ (πΌ β (π« π΅ βm π«
π΅) β πΌ:π« π΅βΆπ« π΅) |
6 | 4, 5 | syl 17 |
. . . . . . 7
β’ (π β πΌ:π« π΅βΆπ« π΅) |
7 | | 0elpw 5331 |
. . . . . . . 8
β’ β
β π« π΅ |
8 | 7 | a1i 11 |
. . . . . . 7
β’ (π β β
β π«
π΅) |
9 | 6, 8 | ffvelcdmd 7056 |
. . . . . 6
β’ (π β (πΌββ
) β π« π΅) |
10 | 9 | elpwid 4589 |
. . . . 5
β’ (π β (πΌββ
) β π΅) |
11 | | reldisj 4431 |
. . . . 5
β’ ((πΌββ
) β π΅ β (((πΌββ
) β© π΅) = β
β (πΌββ
) β (π΅ β π΅))) |
12 | 10, 11 | syl 17 |
. . . 4
β’ (π β (((πΌββ
) β© π΅) = β
β (πΌββ
) β (π΅ β π΅))) |
13 | 12 | bicomd 222 |
. . 3
β’ (π β ((πΌββ
) β (π΅ β π΅) β ((πΌββ
) β© π΅) = β
)) |
14 | | difid 4350 |
. . . . 5
β’ (π΅ β π΅) = β
|
15 | 14 | sseq2i 3991 |
. . . 4
β’ ((πΌββ
) β (π΅ β π΅) β (πΌββ
) β
β
) |
16 | | ss0b 4377 |
. . . 4
β’ ((πΌββ
) β β
β (πΌββ
) =
β
) |
17 | 15, 16 | bitri 274 |
. . 3
β’ ((πΌββ
) β (π΅ β π΅) β (πΌββ
) = β
) |
18 | | disjr 4429 |
. . 3
β’ (((πΌββ
) β© π΅) = β
β βπ₯ β π΅ Β¬ π₯ β (πΌββ
)) |
19 | 13, 17, 18 | 3bitr3g 312 |
. 2
β’ (π β ((πΌββ
) = β
β
βπ₯ β π΅ Β¬ π₯ β (πΌββ
))) |
20 | 3 | adantr 481 |
. . . . 5
β’ ((π β§ π₯ β π΅) β πΌπΉπ) |
21 | | simpr 485 |
. . . . 5
β’ ((π β§ π₯ β π΅) β π₯ β π΅) |
22 | 7 | a1i 11 |
. . . . 5
β’ ((π β§ π₯ β π΅) β β
β π« π΅) |
23 | 1, 2, 20, 21, 22 | ntrneiel 42508 |
. . . 4
β’ ((π β§ π₯ β π΅) β (π₯ β (πΌββ
) β β
β (πβπ₯))) |
24 | 23 | notbid 317 |
. . 3
β’ ((π β§ π₯ β π΅) β (Β¬ π₯ β (πΌββ
) β Β¬ β
β
(πβπ₯))) |
25 | 24 | ralbidva 3174 |
. 2
β’ (π β (βπ₯ β π΅ Β¬ π₯ β (πΌββ
) β βπ₯ β π΅ Β¬ β
β (πβπ₯))) |
26 | 19, 25 | bitrd 278 |
1
β’ (π β ((πΌββ
) = β
β
βπ₯ β π΅ Β¬ β
β (πβπ₯))) |