Step | Hyp | Ref
| Expression |
1 | | dfss3 3936 |
. . . . . 6
β’ ((πΌβ(π βͺ π‘)) β ((πΌβπ ) βͺ (πΌβπ‘)) β βπ₯ β (πΌβ(π βͺ π‘))π₯ β ((πΌβπ ) βͺ (πΌβπ‘))) |
2 | | ntrnei.o |
. . . . . . . . . . . . 13
β’ π = (π β V, π β V β¦ (π β (π« π βm π) β¦ (π β π β¦ {π β π β£ π β (πβπ)}))) |
3 | | ntrnei.f |
. . . . . . . . . . . . 13
β’ πΉ = (π« π΅ππ΅) |
4 | | ntrnei.r |
. . . . . . . . . . . . 13
β’ (π β πΌπΉπ) |
5 | 2, 3, 4 | ntrneiiex 42440 |
. . . . . . . . . . . 12
β’ (π β πΌ β (π« π΅ βm π« π΅)) |
6 | 5 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π β π« π΅) β§ π‘ β π« π΅) β πΌ β (π« π΅ βm π« π΅)) |
7 | | elmapi 8793 |
. . . . . . . . . . 11
β’ (πΌ β (π« π΅ βm π«
π΅) β πΌ:π« π΅βΆπ« π΅) |
8 | 6, 7 | syl 17 |
. . . . . . . . . 10
β’ (((π β§ π β π« π΅) β§ π‘ β π« π΅) β πΌ:π« π΅βΆπ« π΅) |
9 | 2, 3, 4 | ntrneibex 42437 |
. . . . . . . . . . . 12
β’ (π β π΅ β V) |
10 | 9 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π β π« π΅) β§ π‘ β π« π΅) β π΅ β V) |
11 | | simplr 768 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π« π΅) β§ π‘ β π« π΅) β π β π« π΅) |
12 | 11 | elpwid 4573 |
. . . . . . . . . . . 12
β’ (((π β§ π β π« π΅) β§ π‘ β π« π΅) β π β π΅) |
13 | | simpr 486 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π« π΅) β§ π‘ β π« π΅) β π‘ β π« π΅) |
14 | 13 | elpwid 4573 |
. . . . . . . . . . . 12
β’ (((π β§ π β π« π΅) β§ π‘ β π« π΅) β π‘ β π΅) |
15 | 12, 14 | unssd 4150 |
. . . . . . . . . . 11
β’ (((π β§ π β π« π΅) β§ π‘ β π« π΅) β (π βͺ π‘) β π΅) |
16 | 10, 15 | sselpwd 5287 |
. . . . . . . . . 10
β’ (((π β§ π β π« π΅) β§ π‘ β π« π΅) β (π βͺ π‘) β π« π΅) |
17 | 8, 16 | ffvelcdmd 7040 |
. . . . . . . . 9
β’ (((π β§ π β π« π΅) β§ π‘ β π« π΅) β (πΌβ(π βͺ π‘)) β π« π΅) |
18 | 17 | elpwid 4573 |
. . . . . . . 8
β’ (((π β§ π β π« π΅) β§ π‘ β π« π΅) β (πΌβ(π βͺ π‘)) β π΅) |
19 | | ralss 4018 |
. . . . . . . 8
β’ ((πΌβ(π βͺ π‘)) β π΅ β (βπ₯ β (πΌβ(π βͺ π‘))π₯ β ((πΌβπ ) βͺ (πΌβπ‘)) β βπ₯ β π΅ (π₯ β (πΌβ(π βͺ π‘)) β π₯ β ((πΌβπ ) βͺ (πΌβπ‘))))) |
20 | 18, 19 | syl 17 |
. . . . . . 7
β’ (((π β§ π β π« π΅) β§ π‘ β π« π΅) β (βπ₯ β (πΌβ(π βͺ π‘))π₯ β ((πΌβπ ) βͺ (πΌβπ‘)) β βπ₯ β π΅ (π₯ β (πΌβ(π βͺ π‘)) β π₯ β ((πΌβπ ) βͺ (πΌβπ‘))))) |
21 | 4 | ad3antrrr 729 |
. . . . . . . . . 10
β’ ((((π β§ π β π« π΅) β§ π‘ β π« π΅) β§ π₯ β π΅) β πΌπΉπ) |
22 | | simpr 486 |
. . . . . . . . . 10
β’ ((((π β§ π β π« π΅) β§ π‘ β π« π΅) β§ π₯ β π΅) β π₯ β π΅) |
23 | 9 | ad3antrrr 729 |
. . . . . . . . . . 11
β’ ((((π β§ π β π« π΅) β§ π‘ β π« π΅) β§ π₯ β π΅) β π΅ β V) |
24 | | simpllr 775 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β π« π΅) β§ π‘ β π« π΅) β§ π₯ β π΅) β π β π« π΅) |
25 | 24 | elpwid 4573 |
. . . . . . . . . . . 12
β’ ((((π β§ π β π« π΅) β§ π‘ β π« π΅) β§ π₯ β π΅) β π β π΅) |
26 | | simplr 768 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β π« π΅) β§ π‘ β π« π΅) β§ π₯ β π΅) β π‘ β π« π΅) |
27 | 26 | elpwid 4573 |
. . . . . . . . . . . 12
β’ ((((π β§ π β π« π΅) β§ π‘ β π« π΅) β§ π₯ β π΅) β π‘ β π΅) |
28 | 25, 27 | unssd 4150 |
. . . . . . . . . . 11
β’ ((((π β§ π β π« π΅) β§ π‘ β π« π΅) β§ π₯ β π΅) β (π βͺ π‘) β π΅) |
29 | 23, 28 | sselpwd 5287 |
. . . . . . . . . 10
β’ ((((π β§ π β π« π΅) β§ π‘ β π« π΅) β§ π₯ β π΅) β (π βͺ π‘) β π« π΅) |
30 | 2, 3, 21, 22, 29 | ntrneiel 42445 |
. . . . . . . . 9
β’ ((((π β§ π β π« π΅) β§ π‘ β π« π΅) β§ π₯ β π΅) β (π₯ β (πΌβ(π βͺ π‘)) β (π βͺ π‘) β (πβπ₯))) |
31 | | elun 4112 |
. . . . . . . . . 10
β’ (π₯ β ((πΌβπ ) βͺ (πΌβπ‘)) β (π₯ β (πΌβπ ) β¨ π₯ β (πΌβπ‘))) |
32 | 2, 3, 21, 22, 24 | ntrneiel 42445 |
. . . . . . . . . . 11
β’ ((((π β§ π β π« π΅) β§ π‘ β π« π΅) β§ π₯ β π΅) β (π₯ β (πΌβπ ) β π β (πβπ₯))) |
33 | 2, 3, 21, 22, 26 | ntrneiel 42445 |
. . . . . . . . . . 11
β’ ((((π β§ π β π« π΅) β§ π‘ β π« π΅) β§ π₯ β π΅) β (π₯ β (πΌβπ‘) β π‘ β (πβπ₯))) |
34 | 32, 33 | orbi12d 918 |
. . . . . . . . . 10
β’ ((((π β§ π β π« π΅) β§ π‘ β π« π΅) β§ π₯ β π΅) β ((π₯ β (πΌβπ ) β¨ π₯ β (πΌβπ‘)) β (π β (πβπ₯) β¨ π‘ β (πβπ₯)))) |
35 | 31, 34 | bitrid 283 |
. . . . . . . . 9
β’ ((((π β§ π β π« π΅) β§ π‘ β π« π΅) β§ π₯ β π΅) β (π₯ β ((πΌβπ ) βͺ (πΌβπ‘)) β (π β (πβπ₯) β¨ π‘ β (πβπ₯)))) |
36 | 30, 35 | imbi12d 345 |
. . . . . . . 8
β’ ((((π β§ π β π« π΅) β§ π‘ β π« π΅) β§ π₯ β π΅) β ((π₯ β (πΌβ(π βͺ π‘)) β π₯ β ((πΌβπ ) βͺ (πΌβπ‘))) β ((π βͺ π‘) β (πβπ₯) β (π β (πβπ₯) β¨ π‘ β (πβπ₯))))) |
37 | 36 | ralbidva 3169 |
. . . . . . 7
β’ (((π β§ π β π« π΅) β§ π‘ β π« π΅) β (βπ₯ β π΅ (π₯ β (πΌβ(π βͺ π‘)) β π₯ β ((πΌβπ ) βͺ (πΌβπ‘))) β βπ₯ β π΅ ((π βͺ π‘) β (πβπ₯) β (π β (πβπ₯) β¨ π‘ β (πβπ₯))))) |
38 | 20, 37 | bitrd 279 |
. . . . . 6
β’ (((π β§ π β π« π΅) β§ π‘ β π« π΅) β (βπ₯ β (πΌβ(π βͺ π‘))π₯ β ((πΌβπ ) βͺ (πΌβπ‘)) β βπ₯ β π΅ ((π βͺ π‘) β (πβπ₯) β (π β (πβπ₯) β¨ π‘ β (πβπ₯))))) |
39 | 1, 38 | bitrid 283 |
. . . . 5
β’ (((π β§ π β π« π΅) β§ π‘ β π« π΅) β ((πΌβ(π βͺ π‘)) β ((πΌβπ ) βͺ (πΌβπ‘)) β βπ₯ β π΅ ((π βͺ π‘) β (πβπ₯) β (π β (πβπ₯) β¨ π‘ β (πβπ₯))))) |
40 | 39 | ralbidva 3169 |
. . . 4
β’ ((π β§ π β π« π΅) β (βπ‘ β π« π΅(πΌβ(π βͺ π‘)) β ((πΌβπ ) βͺ (πΌβπ‘)) β βπ‘ β π« π΅βπ₯ β π΅ ((π βͺ π‘) β (πβπ₯) β (π β (πβπ₯) β¨ π‘ β (πβπ₯))))) |
41 | | ralcom 3271 |
. . . 4
β’
(βπ‘ β
π« π΅βπ₯ β π΅ ((π βͺ π‘) β (πβπ₯) β (π β (πβπ₯) β¨ π‘ β (πβπ₯))) β βπ₯ β π΅ βπ‘ β π« π΅((π βͺ π‘) β (πβπ₯) β (π β (πβπ₯) β¨ π‘ β (πβπ₯)))) |
42 | 40, 41 | bitrdi 287 |
. . 3
β’ ((π β§ π β π« π΅) β (βπ‘ β π« π΅(πΌβ(π βͺ π‘)) β ((πΌβπ ) βͺ (πΌβπ‘)) β βπ₯ β π΅ βπ‘ β π« π΅((π βͺ π‘) β (πβπ₯) β (π β (πβπ₯) β¨ π‘ β (πβπ₯))))) |
43 | 42 | ralbidva 3169 |
. 2
β’ (π β (βπ β π« π΅βπ‘ β π« π΅(πΌβ(π βͺ π‘)) β ((πΌβπ ) βͺ (πΌβπ‘)) β βπ β π« π΅βπ₯ β π΅ βπ‘ β π« π΅((π βͺ π‘) β (πβπ₯) β (π β (πβπ₯) β¨ π‘ β (πβπ₯))))) |
44 | | ralcom 3271 |
. 2
β’
(βπ β
π« π΅βπ₯ β π΅ βπ‘ β π« π΅((π βͺ π‘) β (πβπ₯) β (π β (πβπ₯) β¨ π‘ β (πβπ₯))) β βπ₯ β π΅ βπ β π« π΅βπ‘ β π« π΅((π βͺ π‘) β (πβπ₯) β (π β (πβπ₯) β¨ π‘ β (πβπ₯)))) |
45 | 43, 44 | bitrdi 287 |
1
β’ (π β (βπ β π« π΅βπ‘ β π« π΅(πΌβ(π βͺ π‘)) β ((πΌβπ ) βͺ (πΌβπ‘)) β βπ₯ β π΅ βπ β π« π΅βπ‘ β π« π΅((π βͺ π‘) β (πβπ₯) β (π β (πβπ₯) β¨ π‘ β (πβπ₯))))) |