Step | Hyp | Ref
| Expression |
1 | | relopabv 5822 |
. . . 4
β’ Rel
{β¨π, π β© β£ (π = (π β(β©π β ((LTrnβπΎ)βπ)(πβ((ocβπΎ)βπ)) = π)) β§ π β ((TEndoβπΎ)βπ))} |
2 | | eqid 2733 |
. . . . . . . . . 10
β’
(leβπΎ) =
(leβπΎ) |
3 | | eqid 2733 |
. . . . . . . . . 10
β’
(AtomsβπΎ) =
(AtomsβπΎ) |
4 | | dicvalrel.h |
. . . . . . . . . 10
β’ π» = (LHypβπΎ) |
5 | | dicvalrel.i |
. . . . . . . . . 10
β’ πΌ = ((DIsoCβπΎ)βπ) |
6 | 2, 3, 4, 5 | dicdmN 40055 |
. . . . . . . . 9
β’ ((πΎ β π β§ π β π») β dom πΌ = {π β (AtomsβπΎ) β£ Β¬ π(leβπΎ)π}) |
7 | 6 | eleq2d 2820 |
. . . . . . . 8
β’ ((πΎ β π β§ π β π») β (π β dom πΌ β π β {π β (AtomsβπΎ) β£ Β¬ π(leβπΎ)π})) |
8 | | breq1 5152 |
. . . . . . . . . 10
β’ (π = π β (π(leβπΎ)π β π(leβπΎ)π)) |
9 | 8 | notbid 318 |
. . . . . . . . 9
β’ (π = π β (Β¬ π(leβπΎ)π β Β¬ π(leβπΎ)π)) |
10 | 9 | elrab 3684 |
. . . . . . . 8
β’ (π β {π β (AtomsβπΎ) β£ Β¬ π(leβπΎ)π} β (π β (AtomsβπΎ) β§ Β¬ π(leβπΎ)π)) |
11 | 7, 10 | bitrdi 287 |
. . . . . . 7
β’ ((πΎ β π β§ π β π») β (π β dom πΌ β (π β (AtomsβπΎ) β§ Β¬ π(leβπΎ)π))) |
12 | 11 | biimpa 478 |
. . . . . 6
β’ (((πΎ β π β§ π β π») β§ π β dom πΌ) β (π β (AtomsβπΎ) β§ Β¬ π(leβπΎ)π)) |
13 | | eqid 2733 |
. . . . . . 7
β’
((ocβπΎ)βπ) = ((ocβπΎ)βπ) |
14 | | eqid 2733 |
. . . . . . 7
β’
((LTrnβπΎ)βπ) = ((LTrnβπΎ)βπ) |
15 | | eqid 2733 |
. . . . . . 7
β’
((TEndoβπΎ)βπ) = ((TEndoβπΎ)βπ) |
16 | 2, 3, 4, 13, 14, 15, 5 | dicval 40047 |
. . . . . 6
β’ (((πΎ β π β§ π β π») β§ (π β (AtomsβπΎ) β§ Β¬ π(leβπΎ)π)) β (πΌβπ) = {β¨π, π β© β£ (π = (π β(β©π β ((LTrnβπΎ)βπ)(πβ((ocβπΎ)βπ)) = π)) β§ π β ((TEndoβπΎ)βπ))}) |
17 | 12, 16 | syldan 592 |
. . . . 5
β’ (((πΎ β π β§ π β π») β§ π β dom πΌ) β (πΌβπ) = {β¨π, π β© β£ (π = (π β(β©π β ((LTrnβπΎ)βπ)(πβ((ocβπΎ)βπ)) = π)) β§ π β ((TEndoβπΎ)βπ))}) |
18 | 17 | releqd 5779 |
. . . 4
β’ (((πΎ β π β§ π β π») β§ π β dom πΌ) β (Rel (πΌβπ) β Rel {β¨π, π β© β£ (π = (π β(β©π β ((LTrnβπΎ)βπ)(πβ((ocβπΎ)βπ)) = π)) β§ π β ((TEndoβπΎ)βπ))})) |
19 | 1, 18 | mpbiri 258 |
. . 3
β’ (((πΎ β π β§ π β π») β§ π β dom πΌ) β Rel (πΌβπ)) |
20 | 19 | ex 414 |
. 2
β’ ((πΎ β π β§ π β π») β (π β dom πΌ β Rel (πΌβπ))) |
21 | | rel0 5800 |
. . 3
β’ Rel
β
|
22 | | ndmfv 6927 |
. . . 4
β’ (Β¬
π β dom πΌ β (πΌβπ) = β
) |
23 | 22 | releqd 5779 |
. . 3
β’ (Β¬
π β dom πΌ β (Rel (πΌβπ) β Rel β
)) |
24 | 21, 23 | mpbiri 258 |
. 2
β’ (Β¬
π β dom πΌ β Rel (πΌβπ)) |
25 | 20, 24 | pm2.61d1 180 |
1
β’ ((πΎ β π β§ π β π») β Rel (πΌβπ)) |