Step | Hyp | Ref
| Expression |
1 | | relxp 5695 |
. . 3
β’ Rel
((((DIsoAβπΎ)βπ)βπ) Γ {(β β ((LTrnβπΎ)βπ) β¦ ( I βΎ (BaseβπΎ)))}) |
2 | | dibcl.h |
. . . . . . . 8
β’ π» = (LHypβπΎ) |
3 | | eqid 2733 |
. . . . . . . 8
β’
((DIsoAβπΎ)βπ) = ((DIsoAβπΎ)βπ) |
4 | | dibcl.i |
. . . . . . . 8
β’ πΌ = ((DIsoBβπΎ)βπ) |
5 | 2, 3, 4 | dibdiadm 40026 |
. . . . . . 7
β’ ((πΎ β π β§ π β π») β dom πΌ = dom ((DIsoAβπΎ)βπ)) |
6 | 5 | eleq2d 2820 |
. . . . . 6
β’ ((πΎ β π β§ π β π») β (π β dom πΌ β π β dom ((DIsoAβπΎ)βπ))) |
7 | 6 | biimpa 478 |
. . . . 5
β’ (((πΎ β π β§ π β π») β§ π β dom πΌ) β π β dom ((DIsoAβπΎ)βπ)) |
8 | | eqid 2733 |
. . . . . 6
β’
(BaseβπΎ) =
(BaseβπΎ) |
9 | | eqid 2733 |
. . . . . 6
β’
((LTrnβπΎ)βπ) = ((LTrnβπΎ)βπ) |
10 | | eqid 2733 |
. . . . . 6
β’ (β β ((LTrnβπΎ)βπ) β¦ ( I βΎ (BaseβπΎ))) = (β β ((LTrnβπΎ)βπ) β¦ ( I βΎ (BaseβπΎ))) |
11 | 8, 2, 9, 10, 3, 4 | dibval 40013 |
. . . . 5
β’ (((πΎ β π β§ π β π») β§ π β dom ((DIsoAβπΎ)βπ)) β (πΌβπ) = ((((DIsoAβπΎ)βπ)βπ) Γ {(β β ((LTrnβπΎ)βπ) β¦ ( I βΎ (BaseβπΎ)))})) |
12 | 7, 11 | syldan 592 |
. . . 4
β’ (((πΎ β π β§ π β π») β§ π β dom πΌ) β (πΌβπ) = ((((DIsoAβπΎ)βπ)βπ) Γ {(β β ((LTrnβπΎ)βπ) β¦ ( I βΎ (BaseβπΎ)))})) |
13 | 12 | releqd 5779 |
. . 3
β’ (((πΎ β π β§ π β π») β§ π β dom πΌ) β (Rel (πΌβπ) β Rel ((((DIsoAβπΎ)βπ)βπ) Γ {(β β ((LTrnβπΎ)βπ) β¦ ( I βΎ (BaseβπΎ)))}))) |
14 | 1, 13 | mpbiri 258 |
. 2
β’ (((πΎ β π β§ π β π») β§ π β dom πΌ) β Rel (πΌβπ)) |
15 | | rel0 5800 |
. . . 4
β’ Rel
β
|
16 | | ndmfv 6927 |
. . . . 5
β’ (Β¬
π β dom πΌ β (πΌβπ) = β
) |
17 | 16 | releqd 5779 |
. . . 4
β’ (Β¬
π β dom πΌ β (Rel (πΌβπ) β Rel β
)) |
18 | 15, 17 | mpbiri 258 |
. . 3
β’ (Β¬
π β dom πΌ β Rel (πΌβπ)) |
19 | 18 | adantl 483 |
. 2
β’ (((πΎ β π β§ π β π») β§ Β¬ π β dom πΌ) β Rel (πΌβπ)) |
20 | 14, 19 | pm2.61dan 812 |
1
β’ ((πΎ β π β§ π β π») β Rel (πΌβπ)) |