Step | Hyp | Ref
| Expression |
1 | | bj-charfun.1 |
. . 3
β’ (π β πΉ = (π₯ β π β¦ if(π₯ β π΄, 1o, β
))) |
2 | | fmelpw1o 14528 |
. . . 4
β’ if(π₯ β π΄, 1o, β
) β π«
1o |
3 | 2 | a1i 9 |
. . 3
β’ ((π β§ π₯ β π) β if(π₯ β π΄, 1o, β
) β π«
1o) |
4 | 1, 3 | fmpt3d 5672 |
. 2
β’ (π β πΉ:πβΆπ«
1o) |
5 | | inss1 3355 |
. . . . 5
β’ (π β© π΄) β π |
6 | 5 | a1i 9 |
. . . 4
β’ (π β (π β© π΄) β π) |
7 | | difssd 3262 |
. . . 4
β’ (π β (π β π΄) β π) |
8 | 6, 7 | unssd 3311 |
. . 3
β’ (π β ((π β© π΄) βͺ (π β π΄)) β π) |
9 | | elun 3276 |
. . . . 5
β’ (π₯ β ((π β© π΄) βͺ (π β π΄)) β (π₯ β (π β© π΄) β¨ π₯ β (π β π΄))) |
10 | | simpr 110 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (π β© π΄)) β π₯ β (π β© π΄)) |
11 | 10 | elin1d 3324 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (π β© π΄)) β π₯ β π) |
12 | 1 | adantr 276 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (π β© π΄)) β πΉ = (π₯ β π β¦ if(π₯ β π΄, 1o, β
))) |
13 | | 1oex 6424 |
. . . . . . . . . . . . 13
β’
1o β V |
14 | | 0ex 4130 |
. . . . . . . . . . . . 13
β’ β
β V |
15 | 13, 14 | ifelpwun 4483 |
. . . . . . . . . . . 12
β’ if(π₯ β π΄, 1o, β
) β π«
(1o βͺ β
) |
16 | 15 | a1i 9 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β (π β© π΄)) β§ π₯ β π) β if(π₯ β π΄, 1o, β
) β π«
(1o βͺ β
)) |
17 | 12, 16 | fvmpt2d 5602 |
. . . . . . . . . 10
β’ (((π β§ π₯ β (π β© π΄)) β§ π₯ β π) β (πΉβπ₯) = if(π₯ β π΄, 1o, β
)) |
18 | 11, 17 | mpdan 421 |
. . . . . . . . 9
β’ ((π β§ π₯ β (π β© π΄)) β (πΉβπ₯) = if(π₯ β π΄, 1o, β
)) |
19 | 10 | elin2d 3325 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (π β© π΄)) β π₯ β π΄) |
20 | 19 | iftrued 3541 |
. . . . . . . . 9
β’ ((π β§ π₯ β (π β© π΄)) β if(π₯ β π΄, 1o, β
) =
1o) |
21 | 18, 20 | eqtrd 2210 |
. . . . . . . 8
β’ ((π β§ π₯ β (π β© π΄)) β (πΉβπ₯) = 1o) |
22 | | 1lt2o 6442 |
. . . . . . . 8
β’
1o β 2o |
23 | 21, 22 | eqeltrdi 2268 |
. . . . . . 7
β’ ((π β§ π₯ β (π β© π΄)) β (πΉβπ₯) β 2o) |
24 | 23 | ex 115 |
. . . . . 6
β’ (π β (π₯ β (π β© π΄) β (πΉβπ₯) β 2o)) |
25 | | simpr 110 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (π β π΄)) β π₯ β (π β π΄)) |
26 | 25 | eldifad 3140 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (π β π΄)) β π₯ β π) |
27 | 1 | adantr 276 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (π β π΄)) β πΉ = (π₯ β π β¦ if(π₯ β π΄, 1o, β
))) |
28 | 15 | a1i 9 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β (π β π΄)) β§ π₯ β π) β if(π₯ β π΄, 1o, β
) β π«
(1o βͺ β
)) |
29 | 27, 28 | fvmpt2d 5602 |
. . . . . . . . . 10
β’ (((π β§ π₯ β (π β π΄)) β§ π₯ β π) β (πΉβπ₯) = if(π₯ β π΄, 1o, β
)) |
30 | 26, 29 | mpdan 421 |
. . . . . . . . 9
β’ ((π β§ π₯ β (π β π΄)) β (πΉβπ₯) = if(π₯ β π΄, 1o, β
)) |
31 | 25 | eldifbd 3141 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (π β π΄)) β Β¬ π₯ β π΄) |
32 | 31 | iffalsed 3544 |
. . . . . . . . 9
β’ ((π β§ π₯ β (π β π΄)) β if(π₯ β π΄, 1o, β
) =
β
) |
33 | 30, 32 | eqtrd 2210 |
. . . . . . . 8
β’ ((π β§ π₯ β (π β π΄)) β (πΉβπ₯) = β
) |
34 | | 0lt2o 6441 |
. . . . . . . 8
β’ β
β 2o |
35 | 33, 34 | eqeltrdi 2268 |
. . . . . . 7
β’ ((π β§ π₯ β (π β π΄)) β (πΉβπ₯) β 2o) |
36 | 35 | ex 115 |
. . . . . 6
β’ (π β (π₯ β (π β π΄) β (πΉβπ₯) β 2o)) |
37 | 24, 36 | jaod 717 |
. . . . 5
β’ (π β ((π₯ β (π β© π΄) β¨ π₯ β (π β π΄)) β (πΉβπ₯) β 2o)) |
38 | 9, 37 | biimtrid 152 |
. . . 4
β’ (π β (π₯ β ((π β© π΄) βͺ (π β π΄)) β (πΉβπ₯) β 2o)) |
39 | 38 | imp 124 |
. . 3
β’ ((π β§ π₯ β ((π β© π΄) βͺ (π β π΄))) β (πΉβπ₯) β 2o) |
40 | 4, 8, 39 | resflem 5680 |
. 2
β’ (π β (πΉ βΎ ((π β© π΄) βͺ (π β π΄))):((π β© π΄) βͺ (π β π΄))βΆ2o) |
41 | 21 | ralrimiva 2550 |
. . 3
β’ (π β βπ₯ β (π β© π΄)(πΉβπ₯) = 1o) |
42 | 33 | ralrimiva 2550 |
. . 3
β’ (π β βπ₯ β (π β π΄)(πΉβπ₯) = β
) |
43 | 41, 42 | jca 306 |
. 2
β’ (π β (βπ₯ β (π β© π΄)(πΉβπ₯) = 1o β§ βπ₯ β (π β π΄)(πΉβπ₯) = β
)) |
44 | 4, 40, 43 | jca31 309 |
1
β’ (π β ((πΉ:πβΆπ« 1o β§ (πΉ βΎ ((π β© π΄) βͺ (π β π΄))):((π β© π΄) βͺ (π β π΄))βΆ2o) β§
(βπ₯ β (π β© π΄)(πΉβπ₯) = 1o β§ βπ₯ β (π β π΄)(πΉβπ₯) = β
))) |