Step | Hyp | Ref
| Expression |
1 | | ntrnei.o |
. . . . 5
β’ π = (π β V, π β V β¦ (π β (π« π βm π) β¦ (π β π β¦ {π β π β£ π β (πβπ)}))) |
2 | | ntrnei.f |
. . . . 5
β’ πΉ = (π« π΅ππ΅) |
3 | | ntrnei.r |
. . . . . 6
β’ (π β πΌπΉπ) |
4 | 3 | adantr 481 |
. . . . 5
β’ ((π β§ π β π« π΅) β πΌπΉπ) |
5 | | ntrnei.x |
. . . . . 6
β’ (π β π β π΅) |
6 | 5 | adantr 481 |
. . . . 5
β’ ((π β§ π β π« π΅) β π β π΅) |
7 | | simpr 485 |
. . . . 5
β’ ((π β§ π β π« π΅) β π β π« π΅) |
8 | 1, 2, 4, 6, 7 | ntrneiel 42508 |
. . . 4
β’ ((π β§ π β π« π΅) β (π β (πΌβπ ) β π β (πβπ))) |
9 | 8 | notbid 317 |
. . 3
β’ ((π β§ π β π« π΅) β (Β¬ π β (πΌβπ ) β Β¬ π β (πβπ))) |
10 | 9 | rexbidva 3175 |
. 2
β’ (π β (βπ β π« π΅ Β¬ π β (πΌβπ ) β βπ β π« π΅ Β¬ π β (πβπ))) |
11 | 1, 2, 3 | ntrneinex 42504 |
. . . . . . 7
β’ (π β π β (π« π« π΅ βm π΅)) |
12 | | elmapi 8809 |
. . . . . . 7
β’ (π β (π« π«
π΅ βm π΅) β π:π΅βΆπ« π« π΅) |
13 | 11, 12 | syl 17 |
. . . . . 6
β’ (π β π:π΅βΆπ« π« π΅) |
14 | 13, 5 | ffvelcdmd 7056 |
. . . . 5
β’ (π β (πβπ) β π« π« π΅) |
15 | 14 | elpwid 4589 |
. . . 4
β’ (π β (πβπ) β π« π΅) |
16 | | biortn 936 |
. . . 4
β’ ((πβπ) β π« π΅ β (Β¬ π« π΅ β (πβπ) β (Β¬ (πβπ) β π« π΅ β¨ Β¬ π« π΅ β (πβπ)))) |
17 | 15, 16 | syl 17 |
. . 3
β’ (π β (Β¬ π« π΅ β (πβπ) β (Β¬ (πβπ) β π« π΅ β¨ Β¬ π« π΅ β (πβπ)))) |
18 | | df-rex 3070 |
. . . 4
β’
(βπ β
π« π΅ Β¬ π β (πβπ) β βπ (π β π« π΅ β§ Β¬ π β (πβπ))) |
19 | | nss 4026 |
. . . 4
β’ (Β¬
π« π΅ β (πβπ) β βπ (π β π« π΅ β§ Β¬ π β (πβπ))) |
20 | 18, 19 | bitr4i 277 |
. . 3
β’
(βπ β
π« π΅ Β¬ π β (πβπ) β Β¬ π« π΅ β (πβπ)) |
21 | | df-ne 2940 |
. . . 4
β’ ((πβπ) β π« π΅ β Β¬ (πβπ) = π« π΅) |
22 | | ianor 980 |
. . . . 5
β’ (Β¬
((πβπ) β π« π΅ β§ π« π΅ β (πβπ)) β (Β¬ (πβπ) β π« π΅ β¨ Β¬ π« π΅ β (πβπ))) |
23 | | eqss 3977 |
. . . . 5
β’ ((πβπ) = π« π΅ β ((πβπ) β π« π΅ β§ π« π΅ β (πβπ))) |
24 | 22, 23 | xchnxbir 332 |
. . . 4
β’ (Β¬
(πβπ) = π« π΅ β (Β¬ (πβπ) β π« π΅ β¨ Β¬ π« π΅ β (πβπ))) |
25 | 21, 24 | bitri 274 |
. . 3
β’ ((πβπ) β π« π΅ β (Β¬ (πβπ) β π« π΅ β¨ Β¬ π« π΅ β (πβπ))) |
26 | 17, 20, 25 | 3bitr4g 313 |
. 2
β’ (π β (βπ β π« π΅ Β¬ π β (πβπ) β (πβπ) β π« π΅)) |
27 | 10, 26 | bitrd 278 |
1
β’ (π β (βπ β π« π΅ Β¬ π β (πΌβπ ) β (πβπ) β π« π΅)) |