Step | Hyp | Ref
| Expression |
1 | | ntrnei.o |
. . . . . . . . . . . . . 14
β’ π = (π β V, π β V β¦ (π β (π« π βm π) β¦ (π β π β¦ {π β π β£ π β (πβπ)}))) |
2 | | ntrnei.f |
. . . . . . . . . . . . . 14
β’ πΉ = (π« π΅ππ΅) |
3 | | ntrnei.r |
. . . . . . . . . . . . . 14
β’ (π β πΌπΉπ) |
4 | 1, 2, 3 | ntrneiiex 42440 |
. . . . . . . . . . . . 13
β’ (π β πΌ β (π« π΅ βm π« π΅)) |
5 | | elmapi 8793 |
. . . . . . . . . . . . 13
β’ (πΌ β (π« π΅ βm π«
π΅) β πΌ:π« π΅βΆπ« π΅) |
6 | 4, 5 | syl 17 |
. . . . . . . . . . . 12
β’ (π β πΌ:π« π΅βΆπ« π΅) |
7 | 6 | ffvelcdmda 7039 |
. . . . . . . . . . 11
β’ ((π β§ π β π« π΅) β (πΌβπ ) β π« π΅) |
8 | 7 | elpwid 4573 |
. . . . . . . . . 10
β’ ((π β§ π β π« π΅) β (πΌβπ ) β π΅) |
9 | 8 | sselda 3948 |
. . . . . . . . 9
β’ (((π β§ π β π« π΅) β§ π₯ β (πΌβπ )) β π₯ β π΅) |
10 | | biimt 361 |
. . . . . . . . 9
β’ (π₯ β π΅ β (π₯ β π β (π₯ β π΅ β π₯ β π ))) |
11 | 9, 10 | syl 17 |
. . . . . . . 8
β’ (((π β§ π β π« π΅) β§ π₯ β (πΌβπ )) β (π₯ β π β (π₯ β π΅ β π₯ β π ))) |
12 | 11 | pm5.74da 803 |
. . . . . . 7
β’ ((π β§ π β π« π΅) β ((π₯ β (πΌβπ ) β π₯ β π ) β (π₯ β (πΌβπ ) β (π₯ β π΅ β π₯ β π )))) |
13 | | bi2.04 389 |
. . . . . . 7
β’ ((π₯ β (πΌβπ ) β (π₯ β π΅ β π₯ β π )) β (π₯ β π΅ β (π₯ β (πΌβπ ) β π₯ β π ))) |
14 | 12, 13 | bitrdi 287 |
. . . . . 6
β’ ((π β§ π β π« π΅) β ((π₯ β (πΌβπ ) β π₯ β π ) β (π₯ β π΅ β (π₯ β (πΌβπ ) β π₯ β π )))) |
15 | 14 | albidv 1924 |
. . . . 5
β’ ((π β§ π β π« π΅) β (βπ₯(π₯ β (πΌβπ ) β π₯ β π ) β βπ₯(π₯ β π΅ β (π₯ β (πΌβπ ) β π₯ β π )))) |
16 | | dfss2 3934 |
. . . . 5
β’ ((πΌβπ ) β π β βπ₯(π₯ β (πΌβπ ) β π₯ β π )) |
17 | | df-ral 3062 |
. . . . 5
β’
(βπ₯ β
π΅ (π₯ β (πΌβπ ) β π₯ β π ) β βπ₯(π₯ β π΅ β (π₯ β (πΌβπ ) β π₯ β π ))) |
18 | 15, 16, 17 | 3bitr4g 314 |
. . . 4
β’ ((π β§ π β π« π΅) β ((πΌβπ ) β π β βπ₯ β π΅ (π₯ β (πΌβπ ) β π₯ β π ))) |
19 | 3 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π β π« π΅) β§ π₯ β π΅) β πΌπΉπ) |
20 | | simpr 486 |
. . . . . . 7
β’ (((π β§ π β π« π΅) β§ π₯ β π΅) β π₯ β π΅) |
21 | | simplr 768 |
. . . . . . 7
β’ (((π β§ π β π« π΅) β§ π₯ β π΅) β π β π« π΅) |
22 | 1, 2, 19, 20, 21 | ntrneiel 42445 |
. . . . . 6
β’ (((π β§ π β π« π΅) β§ π₯ β π΅) β (π₯ β (πΌβπ ) β π β (πβπ₯))) |
23 | 22 | imbi1d 342 |
. . . . 5
β’ (((π β§ π β π« π΅) β§ π₯ β π΅) β ((π₯ β (πΌβπ ) β π₯ β π ) β (π β (πβπ₯) β π₯ β π ))) |
24 | 23 | ralbidva 3169 |
. . . 4
β’ ((π β§ π β π« π΅) β (βπ₯ β π΅ (π₯ β (πΌβπ ) β π₯ β π ) β βπ₯ β π΅ (π β (πβπ₯) β π₯ β π ))) |
25 | 18, 24 | bitrd 279 |
. . 3
β’ ((π β§ π β π« π΅) β ((πΌβπ ) β π β βπ₯ β π΅ (π β (πβπ₯) β π₯ β π ))) |
26 | 25 | ralbidva 3169 |
. 2
β’ (π β (βπ β π« π΅(πΌβπ ) β π β βπ β π« π΅βπ₯ β π΅ (π β (πβπ₯) β π₯ β π ))) |
27 | | ralcom 3271 |
. 2
β’
(βπ β
π« π΅βπ₯ β π΅ (π β (πβπ₯) β π₯ β π ) β βπ₯ β π΅ βπ β π« π΅(π β (πβπ₯) β π₯ β π )) |
28 | 26, 27 | bitrdi 287 |
1
β’ (π β (βπ β π« π΅(πΌβπ ) β π β βπ₯ β π΅ βπ β π« π΅(π β (πβπ₯) β π₯ β π ))) |