Step | Hyp | Ref
| Expression |
1 | | pwidg 4585 |
. . . . 5
β’ (π΅ β π β π΅ β π« π΅) |
2 | 1 | ad2antrr 725 |
. . . 4
β’ (((π΅ β π β§ πΌ β (π« π΅ βm π« π΅)) β§ ((πΌβπ΅) = π΅ β§ βπ β π« π΅βπ‘ β π« π΅((π β© π‘) = β
β ((πΌβπ ) β© (πΌβπ‘)) = β
))) β π΅ β π« π΅) |
3 | | 0elpw 5316 |
. . . . 5
β’ β
β π« π΅ |
4 | 3 | a1i 11 |
. . . 4
β’ (((π΅ β π β§ πΌ β (π« π΅ βm π« π΅)) β§ ((πΌβπ΅) = π΅ β§ βπ β π« π΅βπ‘ β π« π΅((π β© π‘) = β
β ((πΌβπ ) β© (πΌβπ‘)) = β
))) β β
β
π« π΅) |
5 | | simprr 772 |
. . . 4
β’ (((π΅ β π β§ πΌ β (π« π΅ βm π« π΅)) β§ ((πΌβπ΅) = π΅ β§ βπ β π« π΅βπ‘ β π« π΅((π β© π‘) = β
β ((πΌβπ ) β© (πΌβπ‘)) = β
))) β βπ β π« π΅βπ‘ β π« π΅((π β© π‘) = β
β ((πΌβπ ) β© (πΌβπ‘)) = β
)) |
6 | | ineq1 4170 |
. . . . . . 7
β’ (π = π΅ β (π β© π‘) = (π΅ β© π‘)) |
7 | 6 | eqeq1d 2739 |
. . . . . 6
β’ (π = π΅ β ((π β© π‘) = β
β (π΅ β© π‘) = β
)) |
8 | | fveq2 6847 |
. . . . . . . 8
β’ (π = π΅ β (πΌβπ ) = (πΌβπ΅)) |
9 | 8 | ineq1d 4176 |
. . . . . . 7
β’ (π = π΅ β ((πΌβπ ) β© (πΌβπ‘)) = ((πΌβπ΅) β© (πΌβπ‘))) |
10 | 9 | eqeq1d 2739 |
. . . . . 6
β’ (π = π΅ β (((πΌβπ ) β© (πΌβπ‘)) = β
β ((πΌβπ΅) β© (πΌβπ‘)) = β
)) |
11 | 7, 10 | imbi12d 345 |
. . . . 5
β’ (π = π΅ β (((π β© π‘) = β
β ((πΌβπ ) β© (πΌβπ‘)) = β
) β ((π΅ β© π‘) = β
β ((πΌβπ΅) β© (πΌβπ‘)) = β
))) |
12 | | ineq2 4171 |
. . . . . . . 8
β’ (π‘ = β
β (π΅ β© π‘) = (π΅ β© β
)) |
13 | 12 | eqeq1d 2739 |
. . . . . . 7
β’ (π‘ = β
β ((π΅ β© π‘) = β
β (π΅ β© β
) = β
)) |
14 | | fveq2 6847 |
. . . . . . . . 9
β’ (π‘ = β
β (πΌβπ‘) = (πΌββ
)) |
15 | 14 | ineq2d 4177 |
. . . . . . . 8
β’ (π‘ = β
β ((πΌβπ΅) β© (πΌβπ‘)) = ((πΌβπ΅) β© (πΌββ
))) |
16 | 15 | eqeq1d 2739 |
. . . . . . 7
β’ (π‘ = β
β (((πΌβπ΅) β© (πΌβπ‘)) = β
β ((πΌβπ΅) β© (πΌββ
)) =
β
)) |
17 | 13, 16 | imbi12d 345 |
. . . . . 6
β’ (π‘ = β
β (((π΅ β© π‘) = β
β ((πΌβπ΅) β© (πΌβπ‘)) = β
) β ((π΅ β© β
) = β
β ((πΌβπ΅) β© (πΌββ
)) =
β
))) |
18 | | in0 4356 |
. . . . . . 7
β’ (π΅ β© β
) =
β
|
19 | | pm5.5 362 |
. . . . . . 7
β’ ((π΅ β© β
) = β
β
(((π΅ β© β
) =
β
β ((πΌβπ΅) β© (πΌββ
)) = β
) β ((πΌβπ΅) β© (πΌββ
)) =
β
)) |
20 | 18, 19 | mp1i 13 |
. . . . . 6
β’ (π‘ = β
β (((π΅ β© β
) = β
β
((πΌβπ΅) β© (πΌββ
)) = β
) β ((πΌβπ΅) β© (πΌββ
)) =
β
)) |
21 | 17, 20 | bitrd 279 |
. . . . 5
β’ (π‘ = β
β (((π΅ β© π‘) = β
β ((πΌβπ΅) β© (πΌβπ‘)) = β
) β ((πΌβπ΅) β© (πΌββ
)) =
β
)) |
22 | 11, 21 | rspc2va 3594 |
. . . 4
β’ (((π΅ β π« π΅ β§ β
β π«
π΅) β§ βπ β π« π΅βπ‘ β π« π΅((π β© π‘) = β
β ((πΌβπ ) β© (πΌβπ‘)) = β
)) β ((πΌβπ΅) β© (πΌββ
)) = β
) |
23 | 2, 4, 5, 22 | syl21anc 837 |
. . 3
β’ (((π΅ β π β§ πΌ β (π« π΅ βm π« π΅)) β§ ((πΌβπ΅) = π΅ β§ βπ β π« π΅βπ‘ β π« π΅((π β© π‘) = β
β ((πΌβπ ) β© (πΌβπ‘)) = β
))) β ((πΌβπ΅) β© (πΌββ
)) = β
) |
24 | 23 | ex 414 |
. 2
β’ ((π΅ β π β§ πΌ β (π« π΅ βm π« π΅)) β (((πΌβπ΅) = π΅ β§ βπ β π« π΅βπ‘ β π« π΅((π β© π‘) = β
β ((πΌβπ ) β© (πΌβπ‘)) = β
)) β ((πΌβπ΅) β© (πΌββ
)) =
β
)) |
25 | | elmapi 8794 |
. . . . . 6
β’ (πΌ β (π« π΅ βm π«
π΅) β πΌ:π« π΅βΆπ« π΅) |
26 | 25 | adantl 483 |
. . . . 5
β’ ((π΅ β π β§ πΌ β (π« π΅ βm π« π΅)) β πΌ:π« π΅βΆπ« π΅) |
27 | 3 | a1i 11 |
. . . . 5
β’ ((π΅ β π β§ πΌ β (π« π΅ βm π« π΅)) β β
β
π« π΅) |
28 | 26, 27 | ffvelcdmd 7041 |
. . . 4
β’ ((π΅ β π β§ πΌ β (π« π΅ βm π« π΅)) β (πΌββ
) β π« π΅) |
29 | 28 | elpwid 4574 |
. . 3
β’ ((π΅ β π β§ πΌ β (π« π΅ βm π« π΅)) β (πΌββ
) β π΅) |
30 | | simpl 484 |
. . 3
β’ (((πΌβπ΅) = π΅ β§ βπ β π« π΅βπ‘ β π« π΅((π β© π‘) = β
β ((πΌβπ ) β© (πΌβπ‘)) = β
)) β (πΌβπ΅) = π΅) |
31 | | ineq1 4170 |
. . . . . . . 8
β’ ((πΌβπ΅) = π΅ β ((πΌβπ΅) β© (πΌββ
)) = (π΅ β© (πΌββ
))) |
32 | | incom 4166 |
. . . . . . . 8
β’ (π΅ β© (πΌββ
)) = ((πΌββ
) β© π΅) |
33 | 31, 32 | eqtrdi 2793 |
. . . . . . 7
β’ ((πΌβπ΅) = π΅ β ((πΌβπ΅) β© (πΌββ
)) = ((πΌββ
) β© π΅)) |
34 | 33 | eqeq1d 2739 |
. . . . . 6
β’ ((πΌβπ΅) = π΅ β (((πΌβπ΅) β© (πΌββ
)) = β
β ((πΌββ
) β© π΅) = β
)) |
35 | 34 | biimpd 228 |
. . . . 5
β’ ((πΌβπ΅) = π΅ β (((πΌβπ΅) β© (πΌββ
)) = β
β ((πΌββ
) β© π΅) = β
)) |
36 | | reldisj 4416 |
. . . . . . 7
β’ ((πΌββ
) β π΅ β (((πΌββ
) β© π΅) = β
β (πΌββ
) β (π΅ β π΅))) |
37 | 36 | biimpd 228 |
. . . . . 6
β’ ((πΌββ
) β π΅ β (((πΌββ
) β© π΅) = β
β (πΌββ
) β (π΅ β π΅))) |
38 | | difid 4335 |
. . . . . . . 8
β’ (π΅ β π΅) = β
|
39 | 38 | sseq2i 3978 |
. . . . . . 7
β’ ((πΌββ
) β (π΅ β π΅) β (πΌββ
) β
β
) |
40 | | ss0 4363 |
. . . . . . 7
β’ ((πΌββ
) β β
β (πΌββ
) =
β
) |
41 | 39, 40 | sylbi 216 |
. . . . . 6
β’ ((πΌββ
) β (π΅ β π΅) β (πΌββ
) = β
) |
42 | 37, 41 | syl6com 37 |
. . . . 5
β’ (((πΌββ
) β© π΅) = β
β ((πΌββ
) β π΅ β (πΌββ
) = β
)) |
43 | 35, 42 | syl6com 37 |
. . . 4
β’ (((πΌβπ΅) β© (πΌββ
)) = β
β ((πΌβπ΅) = π΅ β ((πΌββ
) β π΅ β (πΌββ
) =
β
))) |
44 | 43 | com13 88 |
. . 3
β’ ((πΌββ
) β π΅ β ((πΌβπ΅) = π΅ β (((πΌβπ΅) β© (πΌββ
)) = β
β (πΌββ
) =
β
))) |
45 | 29, 30, 44 | syl2im 40 |
. 2
β’ ((π΅ β π β§ πΌ β (π« π΅ βm π« π΅)) β (((πΌβπ΅) = π΅ β§ βπ β π« π΅βπ‘ β π« π΅((π β© π‘) = β
β ((πΌβπ ) β© (πΌβπ‘)) = β
)) β (((πΌβπ΅) β© (πΌββ
)) = β
β (πΌββ
) =
β
))) |
46 | 24, 45 | mpdd 43 |
1
β’ ((π΅ β π β§ πΌ β (π« π΅ βm π« π΅)) β (((πΌβπ΅) = π΅ β§ βπ β π« π΅βπ‘ β π« π΅((π β© π‘) = β
β ((πΌβπ ) β© (πΌβπ‘)) = β
)) β (πΌββ
) = β
)) |