Step | Hyp | Ref
| Expression |
1 | | dfss2 3934 |
. . . . . . . 8
β’ ((πΌβπ ) β (πΌβπ‘) β βπ₯(π₯ β (πΌβπ ) β π₯ β (πΌβπ‘))) |
2 | 1 | imbi2i 336 |
. . . . . . 7
β’ ((π β π‘ β (πΌβπ ) β (πΌβπ‘)) β (π β π‘ β βπ₯(π₯ β (πΌβπ ) β π₯ β (πΌβπ‘)))) |
3 | | 19.21v 1943 |
. . . . . . 7
β’
(βπ₯(π β π‘ β (π₯ β (πΌβπ ) β π₯ β (πΌβπ‘))) β (π β π‘ β βπ₯(π₯ β (πΌβπ ) β π₯ β (πΌβπ‘)))) |
4 | 2, 3 | bitr4i 278 |
. . . . . 6
β’ ((π β π‘ β (πΌβπ ) β (πΌβπ‘)) β βπ₯(π β π‘ β (π₯ β (πΌβπ ) β π₯ β (πΌβπ‘)))) |
5 | | ax-1 6 |
. . . . . . . . . 10
β’ ((π β π‘ β (π₯ β (πΌβπ ) β π₯ β (πΌβπ‘))) β (π₯ β π΅ β (π β π‘ β (π₯ β (πΌβπ ) β π₯ β (πΌβπ‘))))) |
6 | | simpll 766 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β π« π΅) β§ π‘ β π« π΅) β π) |
7 | | ntrnei.o |
. . . . . . . . . . . . . . . . . . . 20
β’ π = (π β V, π β V β¦ (π β (π« π βm π) β¦ (π β π β¦ {π β π β£ π β (πβπ)}))) |
8 | | ntrnei.f |
. . . . . . . . . . . . . . . . . . . 20
β’ πΉ = (π« π΅ππ΅) |
9 | | ntrnei.r |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β πΌπΉπ) |
10 | 7, 8, 9 | ntrneiiex 42440 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β πΌ β (π« π΅ βm π« π΅)) |
11 | | elmapi 8793 |
. . . . . . . . . . . . . . . . . . 19
β’ (πΌ β (π« π΅ βm π«
π΅) β πΌ:π« π΅βΆπ« π΅) |
12 | 6, 10, 11 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β π« π΅) β§ π‘ β π« π΅) β πΌ:π« π΅βΆπ« π΅) |
13 | | simplr 768 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β π« π΅) β§ π‘ β π« π΅) β π β π« π΅) |
14 | 12, 13 | ffvelcdmd 7040 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β π« π΅) β§ π‘ β π« π΅) β (πΌβπ ) β π« π΅) |
15 | 14 | elpwid 4573 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β π« π΅) β§ π‘ β π« π΅) β (πΌβπ ) β π΅) |
16 | 15 | sselda 3948 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π β π« π΅) β§ π‘ β π« π΅) β§ π₯ β (πΌβπ )) β π₯ β π΅) |
17 | 16 | pm2.24d 151 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β π« π΅) β§ π‘ β π« π΅) β§ π₯ β (πΌβπ )) β (Β¬ π₯ β π΅ β π₯ β (πΌβπ‘))) |
18 | 17 | ex 414 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π« π΅) β§ π‘ β π« π΅) β (π₯ β (πΌβπ ) β (Β¬ π₯ β π΅ β π₯ β (πΌβπ‘)))) |
19 | 18 | com23 86 |
. . . . . . . . . . . 12
β’ (((π β§ π β π« π΅) β§ π‘ β π« π΅) β (Β¬ π₯ β π΅ β (π₯ β (πΌβπ ) β π₯ β (πΌβπ‘)))) |
20 | 19 | a1dd 50 |
. . . . . . . . . . 11
β’ (((π β§ π β π« π΅) β§ π‘ β π« π΅) β (Β¬ π₯ β π΅ β (π β π‘ β (π₯ β (πΌβπ ) β π₯ β (πΌβπ‘))))) |
21 | | idd 24 |
. . . . . . . . . . 11
β’ (((π β§ π β π« π΅) β§ π‘ β π« π΅) β ((π β π‘ β (π₯ β (πΌβπ ) β π₯ β (πΌβπ‘))) β (π β π‘ β (π₯ β (πΌβπ ) β π₯ β (πΌβπ‘))))) |
22 | 20, 21 | jad 187 |
. . . . . . . . . 10
β’ (((π β§ π β π« π΅) β§ π‘ β π« π΅) β ((π₯ β π΅ β (π β π‘ β (π₯ β (πΌβπ ) β π₯ β (πΌβπ‘)))) β (π β π‘ β (π₯ β (πΌβπ ) β π₯ β (πΌβπ‘))))) |
23 | 5, 22 | impbid2 225 |
. . . . . . . . 9
β’ (((π β§ π β π« π΅) β§ π‘ β π« π΅) β ((π β π‘ β (π₯ β (πΌβπ ) β π₯ β (πΌβπ‘))) β (π₯ β π΅ β (π β π‘ β (π₯ β (πΌβπ ) β π₯ β (πΌβπ‘)))))) |
24 | 23 | albidv 1924 |
. . . . . . . 8
β’ (((π β§ π β π« π΅) β§ π‘ β π« π΅) β (βπ₯(π β π‘ β (π₯ β (πΌβπ ) β π₯ β (πΌβπ‘))) β βπ₯(π₯ β π΅ β (π β π‘ β (π₯ β (πΌβπ ) β π₯ β (πΌβπ‘)))))) |
25 | | df-ral 3062 |
. . . . . . . 8
β’
(βπ₯ β
π΅ (π β π‘ β (π₯ β (πΌβπ ) β π₯ β (πΌβπ‘))) β βπ₯(π₯ β π΅ β (π β π‘ β (π₯ β (πΌβπ ) β π₯ β (πΌβπ‘))))) |
26 | 24, 25 | bitr4di 289 |
. . . . . . 7
β’ (((π β§ π β π« π΅) β§ π‘ β π« π΅) β (βπ₯(π β π‘ β (π₯ β (πΌβπ ) β π₯ β (πΌβπ‘))) β βπ₯ β π΅ (π β π‘ β (π₯ β (πΌβπ ) β π₯ β (πΌβπ‘))))) |
27 | 9 | ad3antrrr 729 |
. . . . . . . . . . . 12
β’ ((((π β§ π β π« π΅) β§ π‘ β π« π΅) β§ π₯ β π΅) β πΌπΉπ) |
28 | | simpr 486 |
. . . . . . . . . . . 12
β’ ((((π β§ π β π« π΅) β§ π‘ β π« π΅) β§ π₯ β π΅) β π₯ β π΅) |
29 | | simpllr 775 |
. . . . . . . . . . . 12
β’ ((((π β§ π β π« π΅) β§ π‘ β π« π΅) β§ π₯ β π΅) β π β π« π΅) |
30 | 7, 8, 27, 28, 29 | ntrneiel 42445 |
. . . . . . . . . . 11
β’ ((((π β§ π β π« π΅) β§ π‘ β π« π΅) β§ π₯ β π΅) β (π₯ β (πΌβπ ) β π β (πβπ₯))) |
31 | | simplr 768 |
. . . . . . . . . . . 12
β’ ((((π β§ π β π« π΅) β§ π‘ β π« π΅) β§ π₯ β π΅) β π‘ β π« π΅) |
32 | 7, 8, 27, 28, 31 | ntrneiel 42445 |
. . . . . . . . . . 11
β’ ((((π β§ π β π« π΅) β§ π‘ β π« π΅) β§ π₯ β π΅) β (π₯ β (πΌβπ‘) β π‘ β (πβπ₯))) |
33 | 30, 32 | imbi12d 345 |
. . . . . . . . . 10
β’ ((((π β§ π β π« π΅) β§ π‘ β π« π΅) β§ π₯ β π΅) β ((π₯ β (πΌβπ ) β π₯ β (πΌβπ‘)) β (π β (πβπ₯) β π‘ β (πβπ₯)))) |
34 | 33 | imbi2d 341 |
. . . . . . . . 9
β’ ((((π β§ π β π« π΅) β§ π‘ β π« π΅) β§ π₯ β π΅) β ((π β π‘ β (π₯ β (πΌβπ ) β π₯ β (πΌβπ‘))) β (π β π‘ β (π β (πβπ₯) β π‘ β (πβπ₯))))) |
35 | | impexp 452 |
. . . . . . . . . 10
β’ (((π β π‘ β§ π β (πβπ₯)) β π‘ β (πβπ₯)) β (π β π‘ β (π β (πβπ₯) β π‘ β (πβπ₯)))) |
36 | | ancomst 466 |
. . . . . . . . . 10
β’ (((π β π‘ β§ π β (πβπ₯)) β π‘ β (πβπ₯)) β ((π β (πβπ₯) β§ π β π‘) β π‘ β (πβπ₯))) |
37 | 35, 36 | bitr3i 277 |
. . . . . . . . 9
β’ ((π β π‘ β (π β (πβπ₯) β π‘ β (πβπ₯))) β ((π β (πβπ₯) β§ π β π‘) β π‘ β (πβπ₯))) |
38 | 34, 37 | bitrdi 287 |
. . . . . . . 8
β’ ((((π β§ π β π« π΅) β§ π‘ β π« π΅) β§ π₯ β π΅) β ((π β π‘ β (π₯ β (πΌβπ ) β π₯ β (πΌβπ‘))) β ((π β (πβπ₯) β§ π β π‘) β π‘ β (πβπ₯)))) |
39 | 38 | ralbidva 3169 |
. . . . . . 7
β’ (((π β§ π β π« π΅) β§ π‘ β π« π΅) β (βπ₯ β π΅ (π β π‘ β (π₯ β (πΌβπ ) β π₯ β (πΌβπ‘))) β βπ₯ β π΅ ((π β (πβπ₯) β§ π β π‘) β π‘ β (πβπ₯)))) |
40 | 26, 39 | bitrd 279 |
. . . . . 6
β’ (((π β§ π β π« π΅) β§ π‘ β π« π΅) β (βπ₯(π β π‘ β (π₯ β (πΌβπ ) β π₯ β (πΌβπ‘))) β βπ₯ β π΅ ((π β (πβπ₯) β§ π β π‘) β π‘ β (πβπ₯)))) |
41 | 4, 40 | bitrid 283 |
. . . . 5
β’ (((π β§ π β π« π΅) β§ π‘ β π« π΅) β ((π β π‘ β (πΌβπ ) β (πΌβπ‘)) β βπ₯ β π΅ ((π β (πβπ₯) β§ π β π‘) β π‘ β (πβπ₯)))) |
42 | 41 | ralbidva 3169 |
. . . 4
β’ ((π β§ π β π« π΅) β (βπ‘ β π« π΅(π β π‘ β (πΌβπ ) β (πΌβπ‘)) β βπ‘ β π« π΅βπ₯ β π΅ ((π β (πβπ₯) β§ π β π‘) β π‘ β (πβπ₯)))) |
43 | | ralcom 3271 |
. . . 4
β’
(βπ‘ β
π« π΅βπ₯ β π΅ ((π β (πβπ₯) β§ π β π‘) β π‘ β (πβπ₯)) β βπ₯ β π΅ βπ‘ β π« π΅((π β (πβπ₯) β§ π β π‘) β π‘ β (πβπ₯))) |
44 | 42, 43 | bitrdi 287 |
. . 3
β’ ((π β§ π β π« π΅) β (βπ‘ β π« π΅(π β π‘ β (πΌβπ ) β (πΌβπ‘)) β βπ₯ β π΅ βπ‘ β π« π΅((π β (πβπ₯) β§ π β π‘) β π‘ β (πβπ₯)))) |
45 | 44 | ralbidva 3169 |
. 2
β’ (π β (βπ β π« π΅βπ‘ β π« π΅(π β π‘ β (πΌβπ ) β (πΌβπ‘)) β βπ β π« π΅βπ₯ β π΅ βπ‘ β π« π΅((π β (πβπ₯) β§ π β π‘) β π‘ β (πβπ₯)))) |
46 | | ralcom 3271 |
. 2
β’
(βπ β
π« π΅βπ₯ β π΅ βπ‘ β π« π΅((π β (πβπ₯) β§ π β π‘) β π‘ β (πβπ₯)) β βπ₯ β π΅ βπ β π« π΅βπ‘ β π« π΅((π β (πβπ₯) β§ π β π‘) β π‘ β (πβπ₯))) |
47 | 45, 46 | bitrdi 287 |
1
β’ (π β (βπ β π« π΅βπ‘ β π« π΅(π β π‘ β (πΌβπ ) β (πΌβπ‘)) β βπ₯ β π΅ βπ β π« π΅βπ‘ β π« π΅((π β (πβπ₯) β§ π β π‘) β π‘ β (πβπ₯)))) |