Step | Hyp | Ref
| Expression |
1 | | dfcleq 2726 |
. . . . 5
β’ ((πΌβπ ) = (πΌβ(πΌβπ )) β βπ₯(π₯ β (πΌβπ ) β π₯ β (πΌβ(πΌβπ )))) |
2 | | eqcom 2740 |
. . . . 5
β’ ((πΌβ(πΌβπ )) = (πΌβπ ) β (πΌβπ ) = (πΌβ(πΌβπ ))) |
3 | | ralv 3471 |
. . . . 5
β’
(βπ₯ β V
(π₯ β (πΌβπ ) β π₯ β (πΌβ(πΌβπ ))) β βπ₯(π₯ β (πΌβπ ) β π₯ β (πΌβ(πΌβπ )))) |
4 | 1, 2, 3 | 3bitr4i 303 |
. . . 4
β’ ((πΌβ(πΌβπ )) = (πΌβπ ) β βπ₯ β V (π₯ β (πΌβπ ) β π₯ β (πΌβ(πΌβπ )))) |
5 | | ssv 3972 |
. . . . . . 7
β’ π΅ β V |
6 | 5 | a1i 11 |
. . . . . 6
β’ ((π β§ π β π« π΅) β π΅ β V) |
7 | | vex 3451 |
. . . . . . . . 9
β’ π₯ β V |
8 | | eldif 3924 |
. . . . . . . . 9
β’ (π₯ β (V β π΅) β (π₯ β V β§ Β¬ π₯ β π΅)) |
9 | 7, 8 | mpbiran 708 |
. . . . . . . 8
β’ (π₯ β (V β π΅) β Β¬ π₯ β π΅) |
10 | | ntrnei.o |
. . . . . . . . . . . . . . . 16
β’ π = (π β V, π β V β¦ (π β (π« π βm π) β¦ (π β π β¦ {π β π β£ π β (πβπ)}))) |
11 | | ntrnei.f |
. . . . . . . . . . . . . . . 16
β’ πΉ = (π« π΅ππ΅) |
12 | | ntrnei.r |
. . . . . . . . . . . . . . . 16
β’ (π β πΌπΉπ) |
13 | 10, 11, 12 | ntrneiiex 42440 |
. . . . . . . . . . . . . . 15
β’ (π β πΌ β (π« π΅ βm π« π΅)) |
14 | | elmapi 8793 |
. . . . . . . . . . . . . . 15
β’ (πΌ β (π« π΅ βm π«
π΅) β πΌ:π« π΅βΆπ« π΅) |
15 | 13, 14 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β πΌ:π« π΅βΆπ« π΅) |
16 | 15 | ffvelcdmda 7039 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π« π΅) β (πΌβπ ) β π« π΅) |
17 | 16 | elpwid 4573 |
. . . . . . . . . . . 12
β’ ((π β§ π β π« π΅) β (πΌβπ ) β π΅) |
18 | 17 | sseld 3947 |
. . . . . . . . . . 11
β’ ((π β§ π β π« π΅) β (π₯ β (πΌβπ ) β π₯ β π΅)) |
19 | 18 | con3dimp 410 |
. . . . . . . . . 10
β’ (((π β§ π β π« π΅) β§ Β¬ π₯ β π΅) β Β¬ π₯ β (πΌβπ )) |
20 | 15 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π« π΅) β πΌ:π« π΅βΆπ« π΅) |
21 | 20, 16 | ffvelcdmd 7040 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π« π΅) β (πΌβ(πΌβπ )) β π« π΅) |
22 | 21 | elpwid 4573 |
. . . . . . . . . . . 12
β’ ((π β§ π β π« π΅) β (πΌβ(πΌβπ )) β π΅) |
23 | 22 | sseld 3947 |
. . . . . . . . . . 11
β’ ((π β§ π β π« π΅) β (π₯ β (πΌβ(πΌβπ )) β π₯ β π΅)) |
24 | 23 | con3dimp 410 |
. . . . . . . . . 10
β’ (((π β§ π β π« π΅) β§ Β¬ π₯ β π΅) β Β¬ π₯ β (πΌβ(πΌβπ ))) |
25 | 19, 24 | 2falsed 377 |
. . . . . . . . 9
β’ (((π β§ π β π« π΅) β§ Β¬ π₯ β π΅) β (π₯ β (πΌβπ ) β π₯ β (πΌβ(πΌβπ )))) |
26 | 25 | ex 414 |
. . . . . . . 8
β’ ((π β§ π β π« π΅) β (Β¬ π₯ β π΅ β (π₯ β (πΌβπ ) β π₯ β (πΌβ(πΌβπ ))))) |
27 | 9, 26 | biimtrid 241 |
. . . . . . 7
β’ ((π β§ π β π« π΅) β (π₯ β (V β π΅) β (π₯ β (πΌβπ ) β π₯ β (πΌβ(πΌβπ ))))) |
28 | 27 | ralrimiv 3139 |
. . . . . 6
β’ ((π β§ π β π« π΅) β βπ₯ β (V β π΅)(π₯ β (πΌβπ ) β π₯ β (πΌβ(πΌβπ )))) |
29 | 6, 28 | raldifeq 4455 |
. . . . 5
β’ ((π β§ π β π« π΅) β (βπ₯ β π΅ (π₯ β (πΌβπ ) β π₯ β (πΌβ(πΌβπ ))) β βπ₯ β V (π₯ β (πΌβπ ) β π₯ β (πΌβ(πΌβπ ))))) |
30 | 12 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β π« π΅) β πΌπΉπ) |
31 | 30 | adantr 482 |
. . . . . . . 8
β’ (((π β§ π β π« π΅) β§ π₯ β π΅) β πΌπΉπ) |
32 | | simpr 486 |
. . . . . . . 8
β’ (((π β§ π β π« π΅) β§ π₯ β π΅) β π₯ β π΅) |
33 | | simplr 768 |
. . . . . . . 8
β’ (((π β§ π β π« π΅) β§ π₯ β π΅) β π β π« π΅) |
34 | 10, 11, 31, 32, 33 | ntrneiel 42445 |
. . . . . . 7
β’ (((π β§ π β π« π΅) β§ π₯ β π΅) β (π₯ β (πΌβπ ) β π β (πβπ₯))) |
35 | 16 | adantr 482 |
. . . . . . . 8
β’ (((π β§ π β π« π΅) β§ π₯ β π΅) β (πΌβπ ) β π« π΅) |
36 | 10, 11, 31, 32, 35 | ntrneiel 42445 |
. . . . . . 7
β’ (((π β§ π β π« π΅) β§ π₯ β π΅) β (π₯ β (πΌβ(πΌβπ )) β (πΌβπ ) β (πβπ₯))) |
37 | 34, 36 | bibi12d 346 |
. . . . . 6
β’ (((π β§ π β π« π΅) β§ π₯ β π΅) β ((π₯ β (πΌβπ ) β π₯ β (πΌβ(πΌβπ ))) β (π β (πβπ₯) β (πΌβπ ) β (πβπ₯)))) |
38 | 37 | ralbidva 3169 |
. . . . 5
β’ ((π β§ π β π« π΅) β (βπ₯ β π΅ (π₯ β (πΌβπ ) β π₯ β (πΌβ(πΌβπ ))) β βπ₯ β π΅ (π β (πβπ₯) β (πΌβπ ) β (πβπ₯)))) |
39 | 29, 38 | bitr3d 281 |
. . . 4
β’ ((π β§ π β π« π΅) β (βπ₯ β V (π₯ β (πΌβπ ) β π₯ β (πΌβ(πΌβπ ))) β βπ₯ β π΅ (π β (πβπ₯) β (πΌβπ ) β (πβπ₯)))) |
40 | 4, 39 | bitrid 283 |
. . 3
β’ ((π β§ π β π« π΅) β ((πΌβ(πΌβπ )) = (πΌβπ ) β βπ₯ β π΅ (π β (πβπ₯) β (πΌβπ ) β (πβπ₯)))) |
41 | 40 | ralbidva 3169 |
. 2
β’ (π β (βπ β π« π΅(πΌβ(πΌβπ )) = (πΌβπ ) β βπ β π« π΅βπ₯ β π΅ (π β (πβπ₯) β (πΌβπ ) β (πβπ₯)))) |
42 | | ralcom 3271 |
. 2
β’
(βπ β
π« π΅βπ₯ β π΅ (π β (πβπ₯) β (πΌβπ ) β (πβπ₯)) β βπ₯ β π΅ βπ β π« π΅(π β (πβπ₯) β (πΌβπ ) β (πβπ₯))) |
43 | 41, 42 | bitrdi 287 |
1
β’ (π β (βπ β π« π΅(πΌβ(πΌβπ )) = (πΌβπ ) β βπ₯ β π΅ βπ β π« π΅(π β (πβπ₯) β (πΌβπ ) β (πβπ₯)))) |