Step | Hyp | Ref
| Expression |
1 | | dfss3 3936 |
. . . . . 6
β’ (((πΌβπ ) β© (πΌβπ‘)) β (πΌβ(π β© π‘)) β βπ₯ β ((πΌβπ ) β© (πΌβπ‘))π₯ β (πΌβ(π β© π‘))) |
2 | | ntrnei.o |
. . . . . . . . . . . . . 14
β’ π = (π β V, π β V β¦ (π β (π« π βm π) β¦ (π β π β¦ {π β π β£ π β (πβπ)}))) |
3 | | ntrnei.f |
. . . . . . . . . . . . . 14
β’ πΉ = (π« π΅ππ΅) |
4 | | ntrnei.r |
. . . . . . . . . . . . . 14
β’ (π β πΌπΉπ) |
5 | 2, 3, 4 | ntrneiiex 42440 |
. . . . . . . . . . . . 13
β’ (π β πΌ β (π« π΅ βm π« π΅)) |
6 | | elmapi 8793 |
. . . . . . . . . . . . 13
β’ (πΌ β (π« π΅ βm π«
π΅) β πΌ:π« π΅βΆπ« π΅) |
7 | 5, 6 | syl 17 |
. . . . . . . . . . . 12
β’ (π β πΌ:π« π΅βΆπ« π΅) |
8 | 7 | ffvelcdmda 7039 |
. . . . . . . . . . 11
β’ ((π β§ π β π« π΅) β (πΌβπ ) β π« π΅) |
9 | 8 | elpwid 4573 |
. . . . . . . . . 10
β’ ((π β§ π β π« π΅) β (πΌβπ ) β π΅) |
10 | | ssinss1 4201 |
. . . . . . . . . 10
β’ ((πΌβπ ) β π΅ β ((πΌβπ ) β© (πΌβπ‘)) β π΅) |
11 | 9, 10 | syl 17 |
. . . . . . . . 9
β’ ((π β§ π β π« π΅) β ((πΌβπ ) β© (πΌβπ‘)) β π΅) |
12 | 11 | adantr 482 |
. . . . . . . 8
β’ (((π β§ π β π« π΅) β§ π‘ β π« π΅) β ((πΌβπ ) β© (πΌβπ‘)) β π΅) |
13 | | ralss 4018 |
. . . . . . . 8
β’ (((πΌβπ ) β© (πΌβπ‘)) β π΅ β (βπ₯ β ((πΌβπ ) β© (πΌβπ‘))π₯ β (πΌβ(π β© π‘)) β βπ₯ β π΅ (π₯ β ((πΌβπ ) β© (πΌβπ‘)) β π₯ β (πΌβ(π β© π‘))))) |
14 | 12, 13 | syl 17 |
. . . . . . 7
β’ (((π β§ π β π« π΅) β§ π‘ β π« π΅) β (βπ₯ β ((πΌβπ ) β© (πΌβπ‘))π₯ β (πΌβ(π β© π‘)) β βπ₯ β π΅ (π₯ β ((πΌβπ ) β© (πΌβπ‘)) β π₯ β (πΌβ(π β© π‘))))) |
15 | | elin 3930 |
. . . . . . . . . 10
β’ (π₯ β ((πΌβπ ) β© (πΌβπ‘)) β (π₯ β (πΌβπ ) β§ π₯ β (πΌβπ‘))) |
16 | 4 | ad3antrrr 729 |
. . . . . . . . . . . 12
β’ ((((π β§ π β π« π΅) β§ π‘ β π« π΅) β§ π₯ β π΅) β πΌπΉπ) |
17 | | simpr 486 |
. . . . . . . . . . . 12
β’ ((((π β§ π β π« π΅) β§ π‘ β π« π΅) β§ π₯ β π΅) β π₯ β π΅) |
18 | | simpllr 775 |
. . . . . . . . . . . 12
β’ ((((π β§ π β π« π΅) β§ π‘ β π« π΅) β§ π₯ β π΅) β π β π« π΅) |
19 | 2, 3, 16, 17, 18 | ntrneiel 42445 |
. . . . . . . . . . 11
β’ ((((π β§ π β π« π΅) β§ π‘ β π« π΅) β§ π₯ β π΅) β (π₯ β (πΌβπ ) β π β (πβπ₯))) |
20 | | simplr 768 |
. . . . . . . . . . . 12
β’ ((((π β§ π β π« π΅) β§ π‘ β π« π΅) β§ π₯ β π΅) β π‘ β π« π΅) |
21 | 2, 3, 16, 17, 20 | ntrneiel 42445 |
. . . . . . . . . . 11
β’ ((((π β§ π β π« π΅) β§ π‘ β π« π΅) β§ π₯ β π΅) β (π₯ β (πΌβπ‘) β π‘ β (πβπ₯))) |
22 | 19, 21 | anbi12d 632 |
. . . . . . . . . 10
β’ ((((π β§ π β π« π΅) β§ π‘ β π« π΅) β§ π₯ β π΅) β ((π₯ β (πΌβπ ) β§ π₯ β (πΌβπ‘)) β (π β (πβπ₯) β§ π‘ β (πβπ₯)))) |
23 | 15, 22 | bitrid 283 |
. . . . . . . . 9
β’ ((((π β§ π β π« π΅) β§ π‘ β π« π΅) β§ π₯ β π΅) β (π₯ β ((πΌβπ ) β© (πΌβπ‘)) β (π β (πβπ₯) β§ π‘ β (πβπ₯)))) |
24 | 2, 3, 4 | ntrneibex 42437 |
. . . . . . . . . . . 12
β’ (π β π΅ β V) |
25 | 24 | ad3antrrr 729 |
. . . . . . . . . . 11
β’ ((((π β§ π β π« π΅) β§ π‘ β π« π΅) β§ π₯ β π΅) β π΅ β V) |
26 | 18 | elpwid 4573 |
. . . . . . . . . . . 12
β’ ((((π β§ π β π« π΅) β§ π‘ β π« π΅) β§ π₯ β π΅) β π β π΅) |
27 | | ssinss1 4201 |
. . . . . . . . . . . 12
β’ (π β π΅ β (π β© π‘) β π΅) |
28 | 26, 27 | syl 17 |
. . . . . . . . . . 11
β’ ((((π β§ π β π« π΅) β§ π‘ β π« π΅) β§ π₯ β π΅) β (π β© π‘) β π΅) |
29 | 25, 28 | sselpwd 5287 |
. . . . . . . . . 10
β’ ((((π β§ π β π« π΅) β§ π‘ β π« π΅) β§ π₯ β π΅) β (π β© π‘) β π« π΅) |
30 | 2, 3, 16, 17, 29 | ntrneiel 42445 |
. . . . . . . . 9
β’ ((((π β§ π β π« π΅) β§ π‘ β π« π΅) β§ π₯ β π΅) β (π₯ β (πΌβ(π β© π‘)) β (π β© π‘) β (πβπ₯))) |
31 | 23, 30 | imbi12d 345 |
. . . . . . . 8
β’ ((((π β§ π β π« π΅) β§ π‘ β π« π΅) β§ π₯ β π΅) β ((π₯ β ((πΌβπ ) β© (πΌβπ‘)) β π₯ β (πΌβ(π β© π‘))) β ((π β (πβπ₯) β§ π‘ β (πβπ₯)) β (π β© π‘) β (πβπ₯)))) |
32 | 31 | ralbidva 3169 |
. . . . . . 7
β’ (((π β§ π β π« π΅) β§ π‘ β π« π΅) β (βπ₯ β π΅ (π₯ β ((πΌβπ ) β© (πΌβπ‘)) β π₯ β (πΌβ(π β© π‘))) β βπ₯ β π΅ ((π β (πβπ₯) β§ π‘ β (πβπ₯)) β (π β© π‘) β (πβπ₯)))) |
33 | 14, 32 | bitrd 279 |
. . . . . 6
β’ (((π β§ π β π« π΅) β§ π‘ β π« π΅) β (βπ₯ β ((πΌβπ ) β© (πΌβπ‘))π₯ β (πΌβ(π β© π‘)) β βπ₯ β π΅ ((π β (πβπ₯) β§ π‘ β (πβπ₯)) β (π β© π‘) β (πβπ₯)))) |
34 | 1, 33 | bitrid 283 |
. . . . 5
β’ (((π β§ π β π« π΅) β§ π‘ β π« π΅) β (((πΌβπ ) β© (πΌβπ‘)) β (πΌβ(π β© π‘)) β βπ₯ β π΅ ((π β (πβπ₯) β§ π‘ β (πβπ₯)) β (π β© π‘) β (πβπ₯)))) |
35 | 34 | ralbidva 3169 |
. . . 4
β’ ((π β§ π β π« π΅) β (βπ‘ β π« π΅((πΌβπ ) β© (πΌβπ‘)) β (πΌβ(π β© π‘)) β βπ‘ β π« π΅βπ₯ β π΅ ((π β (πβπ₯) β§ π‘ β (πβπ₯)) β (π β© π‘) β (πβπ₯)))) |
36 | | ralcom 3271 |
. . . 4
β’
(βπ‘ β
π« π΅βπ₯ β π΅ ((π β (πβπ₯) β§ π‘ β (πβπ₯)) β (π β© π‘) β (πβπ₯)) β βπ₯ β π΅ βπ‘ β π« π΅((π β (πβπ₯) β§ π‘ β (πβπ₯)) β (π β© π‘) β (πβπ₯))) |
37 | 35, 36 | bitrdi 287 |
. . 3
β’ ((π β§ π β π« π΅) β (βπ‘ β π« π΅((πΌβπ ) β© (πΌβπ‘)) β (πΌβ(π β© π‘)) β βπ₯ β π΅ βπ‘ β π« π΅((π β (πβπ₯) β§ π‘ β (πβπ₯)) β (π β© π‘) β (πβπ₯)))) |
38 | 37 | ralbidva 3169 |
. 2
β’ (π β (βπ β π« π΅βπ‘ β π« π΅((πΌβπ ) β© (πΌβπ‘)) β (πΌβ(π β© π‘)) β βπ β π« π΅βπ₯ β π΅ βπ‘ β π« π΅((π β (πβπ₯) β§ π‘ β (πβπ₯)) β (π β© π‘) β (πβπ₯)))) |
39 | | ralcom 3271 |
. 2
β’
(βπ β
π« π΅βπ₯ β π΅ βπ‘ β π« π΅((π β (πβπ₯) β§ π‘ β (πβπ₯)) β (π β© π‘) β (πβπ₯)) β βπ₯ β π΅ βπ β π« π΅βπ‘ β π« π΅((π β (πβπ₯) β§ π‘ β (πβπ₯)) β (π β© π‘) β (πβπ₯))) |
40 | 38, 39 | bitrdi 287 |
1
β’ (π β (βπ β π« π΅βπ‘ β π« π΅((πΌβπ ) β© (πΌβπ‘)) β (πΌβ(π β© π‘)) β βπ₯ β π΅ βπ β π« π΅βπ‘ β π« π΅((π β (πβπ₯) β§ π‘ β (πβπ₯)) β (π β© π‘) β (πβπ₯)))) |