Step | Hyp | Ref
| Expression |
1 | | bj-charfundc.1 |
. . 3
β’ (π β πΉ = (π₯ β π β¦ if(π₯ β π΄, 1o, β
))) |
2 | 1 | bj-charfun 14119 |
. 2
β’ (π β ((πΉ:πβΆπ« 1o β§ (πΉ βΎ ((π β© π΄) βͺ (π β π΄))):((π β© π΄) βͺ (π β π΄))βΆ2o) β§
(βπ₯ β (π β© π΄)(πΉβπ₯) = 1o β§ βπ₯ β (π β π΄)(πΉβπ₯) = β
))) |
3 | | difin 3370 |
. . . . . . . . . . . 12
β’ (π β (π β© π΄)) = (π β π΄) |
4 | 3 | eqcomi 2179 |
. . . . . . . . . . 11
β’ (π β π΄) = (π β (π β© π΄)) |
5 | 4 | a1i 9 |
. . . . . . . . . 10
β’ (π β (π β π΄) = (π β (π β© π΄))) |
6 | 5 | uneq2d 3287 |
. . . . . . . . 9
β’ (π β ((π β© π΄) βͺ (π β π΄)) = ((π β© π΄) βͺ (π β (π β© π΄)))) |
7 | | inss1 3353 |
. . . . . . . . . . 11
β’ (π β© π΄) β π |
8 | 7 | a1i 9 |
. . . . . . . . . 10
β’ (π β (π β© π΄) β π) |
9 | | bj-charfundc.dc |
. . . . . . . . . . 11
β’ (π β βπ₯ β π DECID π₯ β π΄) |
10 | | elin 3316 |
. . . . . . . . . . . . . 14
β’ (π₯ β (π β© π΄) β (π₯ β π β§ π₯ β π΄)) |
11 | 10 | baibr 920 |
. . . . . . . . . . . . 13
β’ (π₯ β π β (π₯ β π΄ β π₯ β (π β© π΄))) |
12 | 11 | dcbid 838 |
. . . . . . . . . . . 12
β’ (π₯ β π β (DECID π₯ β π΄ β DECID π₯ β (π β© π΄))) |
13 | 12 | ralbiia 2489 |
. . . . . . . . . . 11
β’
(βπ₯ β
π DECID
π₯ β π΄ β βπ₯ β π DECID π₯ β (π β© π΄)) |
14 | 9, 13 | sylib 122 |
. . . . . . . . . 10
β’ (π β βπ₯ β π DECID π₯ β (π β© π΄)) |
15 | | undifdcss 6912 |
. . . . . . . . . 10
β’ (π = ((π β© π΄) βͺ (π β (π β© π΄))) β ((π β© π΄) β π β§ βπ₯ β π DECID π₯ β (π β© π΄))) |
16 | 8, 14, 15 | sylanbrc 417 |
. . . . . . . . 9
β’ (π β π = ((π β© π΄) βͺ (π β (π β© π΄)))) |
17 | 6, 16 | eqtr4d 2211 |
. . . . . . . 8
β’ (π β ((π β© π΄) βͺ (π β π΄)) = π) |
18 | 17 | reseq2d 4900 |
. . . . . . 7
β’ (π β (πΉ βΎ ((π β© π΄) βͺ (π β π΄))) = (πΉ βΎ π)) |
19 | | ssidd 3174 |
. . . . . . . . 9
β’ (π β π β π) |
20 | 19 | resmptd 4951 |
. . . . . . . 8
β’ (π β ((π₯ β π β¦ if(π₯ β π΄, 1o, β
)) βΎ π) = (π₯ β π β¦ if(π₯ β π΄, 1o, β
))) |
21 | 1 | reseq1d 4899 |
. . . . . . . 8
β’ (π β (πΉ βΎ π) = ((π₯ β π β¦ if(π₯ β π΄, 1o, β
)) βΎ π)) |
22 | 20, 21, 1 | 3eqtr4d 2218 |
. . . . . . 7
β’ (π β (πΉ βΎ π) = πΉ) |
23 | 18, 22 | eqtrd 2208 |
. . . . . 6
β’ (π β (πΉ βΎ ((π β© π΄) βͺ (π β π΄))) = πΉ) |
24 | 23, 17 | feq12d 5347 |
. . . . 5
β’ (π β ((πΉ βΎ ((π β© π΄) βͺ (π β π΄))):((π β© π΄) βͺ (π β π΄))βΆ2o β πΉ:πβΆ2o)) |
25 | 24 | biimpd 144 |
. . . 4
β’ (π β ((πΉ βΎ ((π β© π΄) βͺ (π β π΄))):((π β© π΄) βͺ (π β π΄))βΆ2o β πΉ:πβΆ2o)) |
26 | 25 | adantld 278 |
. . 3
β’ (π β ((πΉ:πβΆπ« 1o β§ (πΉ βΎ ((π β© π΄) βͺ (π β π΄))):((π β© π΄) βͺ (π β π΄))βΆ2o) β πΉ:πβΆ2o)) |
27 | 26 | anim1d 336 |
. 2
β’ (π β (((πΉ:πβΆπ« 1o β§ (πΉ βΎ ((π β© π΄) βͺ (π β π΄))):((π β© π΄) βͺ (π β π΄))βΆ2o) β§
(βπ₯ β (π β© π΄)(πΉβπ₯) = 1o β§ βπ₯ β (π β π΄)(πΉβπ₯) = β
)) β (πΉ:πβΆ2o β§ (βπ₯ β (π β© π΄)(πΉβπ₯) = 1o β§ βπ₯ β (π β π΄)(πΉβπ₯) = β
)))) |
28 | 2, 27 | mpd 13 |
1
β’ (π β (πΉ:πβΆ2o β§ (βπ₯ β (π β© π΄)(πΉβπ₯) = 1o β§ βπ₯ β (π β π΄)(πΉβπ₯) = β
))) |