Step | Hyp | Ref
| Expression |
1 | | con34b 316 |
. . . . . . 7
β’ (((π₯ β (πΌβπ ) β§ π₯ β (πΌβπ‘)) β (π β© π‘) β β
) β (Β¬ (π β© π‘) β β
β Β¬ (π₯ β (πΌβπ ) β§ π₯ β (πΌβπ‘)))) |
2 | 1 | albii 1822 |
. . . . . 6
β’
(βπ₯((π₯ β (πΌβπ ) β§ π₯ β (πΌβπ‘)) β (π β© π‘) β β
) β βπ₯(Β¬ (π β© π‘) β β
β Β¬ (π₯ β (πΌβπ ) β§ π₯ β (πΌβπ‘)))) |
3 | | 19.21v 1943 |
. . . . . 6
β’
(βπ₯(Β¬
(π β© π‘) β β
β Β¬ (π₯ β (πΌβπ ) β§ π₯ β (πΌβπ‘))) β (Β¬ (π β© π‘) β β
β βπ₯ Β¬ (π₯ β (πΌβπ ) β§ π₯ β (πΌβπ‘)))) |
4 | | nne 2948 |
. . . . . . 7
β’ (Β¬
(π β© π‘) β β
β (π β© π‘) = β
) |
5 | | elin 3931 |
. . . . . . . . . . 11
β’ (π₯ β ((πΌβπ ) β© (πΌβπ‘)) β (π₯ β (πΌβπ ) β§ π₯ β (πΌβπ‘))) |
6 | 5 | imbi1i 350 |
. . . . . . . . . 10
β’ ((π₯ β ((πΌβπ ) β© (πΌβπ‘)) β π₯ β β
) β ((π₯ β (πΌβπ ) β§ π₯ β (πΌβπ‘)) β π₯ β β
)) |
7 | | noel 4295 |
. . . . . . . . . . 11
β’ Β¬
π₯ β
β
|
8 | | imnot 366 |
. . . . . . . . . . 11
β’ (Β¬
π₯ β β
β
(((π₯ β (πΌβπ ) β§ π₯ β (πΌβπ‘)) β π₯ β β
) β Β¬ (π₯ β (πΌβπ ) β§ π₯ β (πΌβπ‘)))) |
9 | 7, 8 | ax-mp 5 |
. . . . . . . . . 10
β’ (((π₯ β (πΌβπ ) β§ π₯ β (πΌβπ‘)) β π₯ β β
) β Β¬ (π₯ β (πΌβπ ) β§ π₯ β (πΌβπ‘))) |
10 | 6, 9 | bitr2i 276 |
. . . . . . . . 9
β’ (Β¬
(π₯ β (πΌβπ ) β§ π₯ β (πΌβπ‘)) β (π₯ β ((πΌβπ ) β© (πΌβπ‘)) β π₯ β β
)) |
11 | 10 | albii 1822 |
. . . . . . . 8
β’
(βπ₯ Β¬
(π₯ β (πΌβπ ) β§ π₯ β (πΌβπ‘)) β βπ₯(π₯ β ((πΌβπ ) β© (πΌβπ‘)) β π₯ β β
)) |
12 | | dfss2 3935 |
. . . . . . . 8
β’ (((πΌβπ ) β© (πΌβπ‘)) β β
β βπ₯(π₯ β ((πΌβπ ) β© (πΌβπ‘)) β π₯ β β
)) |
13 | | ss0b 4362 |
. . . . . . . 8
β’ (((πΌβπ ) β© (πΌβπ‘)) β β
β ((πΌβπ ) β© (πΌβπ‘)) = β
) |
14 | 11, 12, 13 | 3bitr2i 299 |
. . . . . . 7
β’
(βπ₯ Β¬
(π₯ β (πΌβπ ) β§ π₯ β (πΌβπ‘)) β ((πΌβπ ) β© (πΌβπ‘)) = β
) |
15 | 4, 14 | imbi12i 351 |
. . . . . 6
β’ ((Β¬
(π β© π‘) β β
β βπ₯ Β¬ (π₯ β (πΌβπ ) β§ π₯ β (πΌβπ‘))) β ((π β© π‘) = β
β ((πΌβπ ) β© (πΌβπ‘)) = β
)) |
16 | 2, 3, 15 | 3bitrri 298 |
. . . . 5
β’ (((π β© π‘) = β
β ((πΌβπ ) β© (πΌβπ‘)) = β
) β βπ₯((π₯ β (πΌβπ ) β§ π₯ β (πΌβπ‘)) β (π β© π‘) β β
)) |
17 | | ntrnei.o |
. . . . . . . . . . . . . . . . . . 19
β’ π = (π β V, π β V β¦ (π β (π« π βm π) β¦ (π β π β¦ {π β π β£ π β (πβπ)}))) |
18 | | ntrnei.f |
. . . . . . . . . . . . . . . . . . 19
β’ πΉ = (π« π΅ππ΅) |
19 | | ntrnei.r |
. . . . . . . . . . . . . . . . . . 19
β’ (π β πΌπΉπ) |
20 | 17, 18, 19 | ntrneiiex 42422 |
. . . . . . . . . . . . . . . . . 18
β’ (π β πΌ β (π« π΅ βm π« π΅)) |
21 | | elmapi 8794 |
. . . . . . . . . . . . . . . . . 18
β’ (πΌ β (π« π΅ βm π«
π΅) β πΌ:π« π΅βΆπ« π΅) |
22 | 20, 21 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (π β πΌ:π« π΅βΆπ« π΅) |
23 | 22 | ffvelcdmda 7040 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β π« π΅) β (πΌβπ ) β π« π΅) |
24 | 23 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β π« π΅) β§ π‘ β π« π΅) β (πΌβπ ) β π« π΅) |
25 | 24 | elpwid 4574 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β π« π΅) β§ π‘ β π« π΅) β (πΌβπ ) β π΅) |
26 | 25 | sseld 3948 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π« π΅) β§ π‘ β π« π΅) β (π₯ β (πΌβπ ) β π₯ β π΅)) |
27 | 26 | adantrd 493 |
. . . . . . . . . . . 12
β’ (((π β§ π β π« π΅) β§ π‘ β π« π΅) β ((π₯ β (πΌβπ ) β§ π₯ β (πΌβπ‘)) β π₯ β π΅)) |
28 | 27 | imp 408 |
. . . . . . . . . . 11
β’ ((((π β§ π β π« π΅) β§ π‘ β π« π΅) β§ (π₯ β (πΌβπ ) β§ π₯ β (πΌβπ‘))) β π₯ β π΅) |
29 | | biimt 361 |
. . . . . . . . . . 11
β’ (π₯ β π΅ β ((π β© π‘) β β
β (π₯ β π΅ β (π β© π‘) β β
))) |
30 | 28, 29 | syl 17 |
. . . . . . . . . 10
β’ ((((π β§ π β π« π΅) β§ π‘ β π« π΅) β§ (π₯ β (πΌβπ ) β§ π₯ β (πΌβπ‘))) β ((π β© π‘) β β
β (π₯ β π΅ β (π β© π‘) β β
))) |
31 | 30 | pm5.74da 803 |
. . . . . . . . 9
β’ (((π β§ π β π« π΅) β§ π‘ β π« π΅) β (((π₯ β (πΌβπ ) β§ π₯ β (πΌβπ‘)) β (π β© π‘) β β
) β ((π₯ β (πΌβπ ) β§ π₯ β (πΌβπ‘)) β (π₯ β π΅ β (π β© π‘) β β
)))) |
32 | | bi2.04 389 |
. . . . . . . . 9
β’ (((π₯ β (πΌβπ ) β§ π₯ β (πΌβπ‘)) β (π₯ β π΅ β (π β© π‘) β β
)) β (π₯ β π΅ β ((π₯ β (πΌβπ ) β§ π₯ β (πΌβπ‘)) β (π β© π‘) β β
))) |
33 | 31, 32 | bitrdi 287 |
. . . . . . . 8
β’ (((π β§ π β π« π΅) β§ π‘ β π« π΅) β (((π₯ β (πΌβπ ) β§ π₯ β (πΌβπ‘)) β (π β© π‘) β β
) β (π₯ β π΅ β ((π₯ β (πΌβπ ) β§ π₯ β (πΌβπ‘)) β (π β© π‘) β β
)))) |
34 | 33 | albidv 1924 |
. . . . . . 7
β’ (((π β§ π β π« π΅) β§ π‘ β π« π΅) β (βπ₯((π₯ β (πΌβπ ) β§ π₯ β (πΌβπ‘)) β (π β© π‘) β β
) β βπ₯(π₯ β π΅ β ((π₯ β (πΌβπ ) β§ π₯ β (πΌβπ‘)) β (π β© π‘) β β
)))) |
35 | | df-ral 3066 |
. . . . . . 7
β’
(βπ₯ β
π΅ ((π₯ β (πΌβπ ) β§ π₯ β (πΌβπ‘)) β (π β© π‘) β β
) β βπ₯(π₯ β π΅ β ((π₯ β (πΌβπ ) β§ π₯ β (πΌβπ‘)) β (π β© π‘) β β
))) |
36 | 34, 35 | bitr4di 289 |
. . . . . 6
β’ (((π β§ π β π« π΅) β§ π‘ β π« π΅) β (βπ₯((π₯ β (πΌβπ ) β§ π₯ β (πΌβπ‘)) β (π β© π‘) β β
) β βπ₯ β π΅ ((π₯ β (πΌβπ ) β§ π₯ β (πΌβπ‘)) β (π β© π‘) β β
))) |
37 | 19 | ad3antrrr 729 |
. . . . . . . . . 10
β’ ((((π β§ π β π« π΅) β§ π‘ β π« π΅) β§ π₯ β π΅) β πΌπΉπ) |
38 | | simpr 486 |
. . . . . . . . . 10
β’ ((((π β§ π β π« π΅) β§ π‘ β π« π΅) β§ π₯ β π΅) β π₯ β π΅) |
39 | | simpllr 775 |
. . . . . . . . . 10
β’ ((((π β§ π β π« π΅) β§ π‘ β π« π΅) β§ π₯ β π΅) β π β π« π΅) |
40 | 17, 18, 37, 38, 39 | ntrneiel 42427 |
. . . . . . . . 9
β’ ((((π β§ π β π« π΅) β§ π‘ β π« π΅) β§ π₯ β π΅) β (π₯ β (πΌβπ ) β π β (πβπ₯))) |
41 | | simplr 768 |
. . . . . . . . . 10
β’ ((((π β§ π β π« π΅) β§ π‘ β π« π΅) β§ π₯ β π΅) β π‘ β π« π΅) |
42 | 17, 18, 37, 38, 41 | ntrneiel 42427 |
. . . . . . . . 9
β’ ((((π β§ π β π« π΅) β§ π‘ β π« π΅) β§ π₯ β π΅) β (π₯ β (πΌβπ‘) β π‘ β (πβπ₯))) |
43 | 40, 42 | anbi12d 632 |
. . . . . . . 8
β’ ((((π β§ π β π« π΅) β§ π‘ β π« π΅) β§ π₯ β π΅) β ((π₯ β (πΌβπ ) β§ π₯ β (πΌβπ‘)) β (π β (πβπ₯) β§ π‘ β (πβπ₯)))) |
44 | 43 | imbi1d 342 |
. . . . . . 7
β’ ((((π β§ π β π« π΅) β§ π‘ β π« π΅) β§ π₯ β π΅) β (((π₯ β (πΌβπ ) β§ π₯ β (πΌβπ‘)) β (π β© π‘) β β
) β ((π β (πβπ₯) β§ π‘ β (πβπ₯)) β (π β© π‘) β β
))) |
45 | 44 | ralbidva 3173 |
. . . . . 6
β’ (((π β§ π β π« π΅) β§ π‘ β π« π΅) β (βπ₯ β π΅ ((π₯ β (πΌβπ ) β§ π₯ β (πΌβπ‘)) β (π β© π‘) β β
) β βπ₯ β π΅ ((π β (πβπ₯) β§ π‘ β (πβπ₯)) β (π β© π‘) β β
))) |
46 | 36, 45 | bitrd 279 |
. . . . 5
β’ (((π β§ π β π« π΅) β§ π‘ β π« π΅) β (βπ₯((π₯ β (πΌβπ ) β§ π₯ β (πΌβπ‘)) β (π β© π‘) β β
) β βπ₯ β π΅ ((π β (πβπ₯) β§ π‘ β (πβπ₯)) β (π β© π‘) β β
))) |
47 | 16, 46 | bitrid 283 |
. . . 4
β’ (((π β§ π β π« π΅) β§ π‘ β π« π΅) β (((π β© π‘) = β
β ((πΌβπ ) β© (πΌβπ‘)) = β
) β βπ₯ β π΅ ((π β (πβπ₯) β§ π‘ β (πβπ₯)) β (π β© π‘) β β
))) |
48 | 47 | ralbidva 3173 |
. . 3
β’ ((π β§ π β π« π΅) β (βπ‘ β π« π΅((π β© π‘) = β
β ((πΌβπ ) β© (πΌβπ‘)) = β
) β βπ‘ β π« π΅βπ₯ β π΅ ((π β (πβπ₯) β§ π‘ β (πβπ₯)) β (π β© π‘) β β
))) |
49 | 48 | ralbidva 3173 |
. 2
β’ (π β (βπ β π« π΅βπ‘ β π« π΅((π β© π‘) = β
β ((πΌβπ ) β© (πΌβπ‘)) = β
) β βπ β π« π΅βπ‘ β π« π΅βπ₯ β π΅ ((π β (πβπ₯) β§ π‘ β (πβπ₯)) β (π β© π‘) β β
))) |
50 | | ralrot3 3279 |
. 2
β’
(βπ β
π« π΅βπ‘ β π« π΅βπ₯ β π΅ ((π β (πβπ₯) β§ π‘ β (πβπ₯)) β (π β© π‘) β β
) β βπ₯ β π΅ βπ β π« π΅βπ‘ β π« π΅((π β (πβπ₯) β§ π‘ β (πβπ₯)) β (π β© π‘) β β
)) |
51 | 49, 50 | bitrdi 287 |
1
β’ (π β (βπ β π« π΅βπ‘ β π« π΅((π β© π‘) = β
β ((πΌβπ ) β© (πΌβπ‘)) = β
) β βπ₯ β π΅ βπ β π« π΅βπ‘ β π« π΅((π β (πβπ₯) β§ π‘ β (πβπ₯)) β (π β© π‘) β β
))) |