Step | Hyp | Ref
| Expression |
1 | | dfss3 3970 |
. . . . . 6
β’ (((πΌβπ ) β© (πΌβπ‘)) β (πΌβ(π β© π‘)) β βπ₯ β ((πΌβπ ) β© (πΌβπ‘))π₯ β (πΌβ(π β© π‘))) |
2 | | ntrnei.o |
. . . . . . . . . . . . . 14
β’ π = (π β V, π β V β¦ (π β (π« π βm π) β¦ (π β π β¦ {π β π β£ π β (πβπ)}))) |
3 | | ntrnei.f |
. . . . . . . . . . . . . 14
β’ πΉ = (π« π΅ππ΅) |
4 | | ntrnei.r |
. . . . . . . . . . . . . 14
β’ (π β πΌπΉπ) |
5 | 2, 3, 4 | ntrneiiex 42817 |
. . . . . . . . . . . . 13
β’ (π β πΌ β (π« π΅ βm π« π΅)) |
6 | | elmapi 8842 |
. . . . . . . . . . . . 13
β’ (πΌ β (π« π΅ βm π«
π΅) β πΌ:π« π΅βΆπ« π΅) |
7 | 5, 6 | syl 17 |
. . . . . . . . . . . 12
β’ (π β πΌ:π« π΅βΆπ« π΅) |
8 | 7 | ffvelcdmda 7086 |
. . . . . . . . . . 11
β’ ((π β§ π β π« π΅) β (πΌβπ ) β π« π΅) |
9 | 8 | elpwid 4611 |
. . . . . . . . . 10
β’ ((π β§ π β π« π΅) β (πΌβπ ) β π΅) |
10 | | ssinss1 4237 |
. . . . . . . . . 10
β’ ((πΌβπ ) β π΅ β ((πΌβπ ) β© (πΌβπ‘)) β π΅) |
11 | 9, 10 | syl 17 |
. . . . . . . . 9
β’ ((π β§ π β π« π΅) β ((πΌβπ ) β© (πΌβπ‘)) β π΅) |
12 | 11 | adantr 481 |
. . . . . . . 8
β’ (((π β§ π β π« π΅) β§ π‘ β π« π΅) β ((πΌβπ ) β© (πΌβπ‘)) β π΅) |
13 | | ralss 4054 |
. . . . . . . 8
β’ (((πΌβπ ) β© (πΌβπ‘)) β π΅ β (βπ₯ β ((πΌβπ ) β© (πΌβπ‘))π₯ β (πΌβ(π β© π‘)) β βπ₯ β π΅ (π₯ β ((πΌβπ ) β© (πΌβπ‘)) β π₯ β (πΌβ(π β© π‘))))) |
14 | 12, 13 | syl 17 |
. . . . . . 7
β’ (((π β§ π β π« π΅) β§ π‘ β π« π΅) β (βπ₯ β ((πΌβπ ) β© (πΌβπ‘))π₯ β (πΌβ(π β© π‘)) β βπ₯ β π΅ (π₯ β ((πΌβπ ) β© (πΌβπ‘)) β π₯ β (πΌβ(π β© π‘))))) |
15 | | elin 3964 |
. . . . . . . . . 10
β’ (π₯ β ((πΌβπ ) β© (πΌβπ‘)) β (π₯ β (πΌβπ ) β§ π₯ β (πΌβπ‘))) |
16 | 4 | ad3antrrr 728 |
. . . . . . . . . . . 12
β’ ((((π β§ π β π« π΅) β§ π‘ β π« π΅) β§ π₯ β π΅) β πΌπΉπ) |
17 | | simpr 485 |
. . . . . . . . . . . 12
β’ ((((π β§ π β π« π΅) β§ π‘ β π« π΅) β§ π₯ β π΅) β π₯ β π΅) |
18 | | simpllr 774 |
. . . . . . . . . . . 12
β’ ((((π β§ π β π« π΅) β§ π‘ β π« π΅) β§ π₯ β π΅) β π β π« π΅) |
19 | 2, 3, 16, 17, 18 | ntrneiel 42822 |
. . . . . . . . . . 11
β’ ((((π β§ π β π« π΅) β§ π‘ β π« π΅) β§ π₯ β π΅) β (π₯ β (πΌβπ ) β π β (πβπ₯))) |
20 | | simplr 767 |
. . . . . . . . . . . 12
β’ ((((π β§ π β π« π΅) β§ π‘ β π« π΅) β§ π₯ β π΅) β π‘ β π« π΅) |
21 | 2, 3, 16, 17, 20 | ntrneiel 42822 |
. . . . . . . . . . 11
β’ ((((π β§ π β π« π΅) β§ π‘ β π« π΅) β§ π₯ β π΅) β (π₯ β (πΌβπ‘) β π‘ β (πβπ₯))) |
22 | 19, 21 | anbi12d 631 |
. . . . . . . . . 10
β’ ((((π β§ π β π« π΅) β§ π‘ β π« π΅) β§ π₯ β π΅) β ((π₯ β (πΌβπ ) β§ π₯ β (πΌβπ‘)) β (π β (πβπ₯) β§ π‘ β (πβπ₯)))) |
23 | 15, 22 | bitrid 282 |
. . . . . . . . 9
β’ ((((π β§ π β π« π΅) β§ π‘ β π« π΅) β§ π₯ β π΅) β (π₯ β ((πΌβπ ) β© (πΌβπ‘)) β (π β (πβπ₯) β§ π‘ β (πβπ₯)))) |
24 | 2, 3, 4 | ntrneibex 42814 |
. . . . . . . . . . . 12
β’ (π β π΅ β V) |
25 | 24 | ad3antrrr 728 |
. . . . . . . . . . 11
β’ ((((π β§ π β π« π΅) β§ π‘ β π« π΅) β§ π₯ β π΅) β π΅ β V) |
26 | 18 | elpwid 4611 |
. . . . . . . . . . . 12
β’ ((((π β§ π β π« π΅) β§ π‘ β π« π΅) β§ π₯ β π΅) β π β π΅) |
27 | | ssinss1 4237 |
. . . . . . . . . . . 12
β’ (π β π΅ β (π β© π‘) β π΅) |
28 | 26, 27 | syl 17 |
. . . . . . . . . . 11
β’ ((((π β§ π β π« π΅) β§ π‘ β π« π΅) β§ π₯ β π΅) β (π β© π‘) β π΅) |
29 | 25, 28 | sselpwd 5326 |
. . . . . . . . . 10
β’ ((((π β§ π β π« π΅) β§ π‘ β π« π΅) β§ π₯ β π΅) β (π β© π‘) β π« π΅) |
30 | 2, 3, 16, 17, 29 | ntrneiel 42822 |
. . . . . . . . 9
β’ ((((π β§ π β π« π΅) β§ π‘ β π« π΅) β§ π₯ β π΅) β (π₯ β (πΌβ(π β© π‘)) β (π β© π‘) β (πβπ₯))) |
31 | 23, 30 | imbi12d 344 |
. . . . . . . 8
β’ ((((π β§ π β π« π΅) β§ π‘ β π« π΅) β§ π₯ β π΅) β ((π₯ β ((πΌβπ ) β© (πΌβπ‘)) β π₯ β (πΌβ(π β© π‘))) β ((π β (πβπ₯) β§ π‘ β (πβπ₯)) β (π β© π‘) β (πβπ₯)))) |
32 | 31 | ralbidva 3175 |
. . . . . . 7
β’ (((π β§ π β π« π΅) β§ π‘ β π« π΅) β (βπ₯ β π΅ (π₯ β ((πΌβπ ) β© (πΌβπ‘)) β π₯ β (πΌβ(π β© π‘))) β βπ₯ β π΅ ((π β (πβπ₯) β§ π‘ β (πβπ₯)) β (π β© π‘) β (πβπ₯)))) |
33 | 14, 32 | bitrd 278 |
. . . . . 6
β’ (((π β§ π β π« π΅) β§ π‘ β π« π΅) β (βπ₯ β ((πΌβπ ) β© (πΌβπ‘))π₯ β (πΌβ(π β© π‘)) β βπ₯ β π΅ ((π β (πβπ₯) β§ π‘ β (πβπ₯)) β (π β© π‘) β (πβπ₯)))) |
34 | 1, 33 | bitrid 282 |
. . . . 5
β’ (((π β§ π β π« π΅) β§ π‘ β π« π΅) β (((πΌβπ ) β© (πΌβπ‘)) β (πΌβ(π β© π‘)) β βπ₯ β π΅ ((π β (πβπ₯) β§ π‘ β (πβπ₯)) β (π β© π‘) β (πβπ₯)))) |
35 | 34 | ralbidva 3175 |
. . . 4
β’ ((π β§ π β π« π΅) β (βπ‘ β π« π΅((πΌβπ ) β© (πΌβπ‘)) β (πΌβ(π β© π‘)) β βπ‘ β π« π΅βπ₯ β π΅ ((π β (πβπ₯) β§ π‘ β (πβπ₯)) β (π β© π‘) β (πβπ₯)))) |
36 | | ralcom 3286 |
. . . 4
β’
(βπ‘ β
π« π΅βπ₯ β π΅ ((π β (πβπ₯) β§ π‘ β (πβπ₯)) β (π β© π‘) β (πβπ₯)) β βπ₯ β π΅ βπ‘ β π« π΅((π β (πβπ₯) β§ π‘ β (πβπ₯)) β (π β© π‘) β (πβπ₯))) |
37 | 35, 36 | bitrdi 286 |
. . 3
β’ ((π β§ π β π« π΅) β (βπ‘ β π« π΅((πΌβπ ) β© (πΌβπ‘)) β (πΌβ(π β© π‘)) β βπ₯ β π΅ βπ‘ β π« π΅((π β (πβπ₯) β§ π‘ β (πβπ₯)) β (π β© π‘) β (πβπ₯)))) |
38 | 37 | ralbidva 3175 |
. 2
β’ (π β (βπ β π« π΅βπ‘ β π« π΅((πΌβπ ) β© (πΌβπ‘)) β (πΌβ(π β© π‘)) β βπ β π« π΅βπ₯ β π΅ βπ‘ β π« π΅((π β (πβπ₯) β§ π‘ β (πβπ₯)) β (π β© π‘) β (πβπ₯)))) |
39 | | ralcom 3286 |
. 2
β’
(βπ β
π« π΅βπ₯ β π΅ βπ‘ β π« π΅((π β (πβπ₯) β§ π‘ β (πβπ₯)) β (π β© π‘) β (πβπ₯)) β βπ₯ β π΅ βπ β π« π΅βπ‘ β π« π΅((π β (πβπ₯) β§ π‘ β (πβπ₯)) β (π β© π‘) β (πβπ₯))) |
40 | 38, 39 | bitrdi 286 |
1
β’ (π β (βπ β π« π΅βπ‘ β π« π΅((πΌβπ ) β© (πΌβπ‘)) β (πΌβ(π β© π‘)) β βπ₯ β π΅ βπ β π« π΅βπ‘ β π« π΅((π β (πβπ₯) β§ π‘ β (πβπ₯)) β (π β© π‘) β (πβπ₯)))) |