Step | Hyp | Ref
| Expression |
1 | | relopabv 5821 |
. . . . . 6
β’ Rel
{β¨π₯, π¦β© β£ (π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ) β§ ((IsoβπΆ)ββ¨π₯, π¦β©) β β
)} |
2 | 1 | a1i 11 |
. . . . 5
β’ (πΆ β Cat β Rel
{β¨π₯, π¦β© β£ (π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ) β§ ((IsoβπΆ)ββ¨π₯, π¦β©) β β
)}) |
3 | | fveq2 6891 |
. . . . . . . . 9
β’ (π = β¨π₯, π¦β© β ((IsoβπΆ)βπ) = ((IsoβπΆ)ββ¨π₯, π¦β©)) |
4 | 3 | neeq1d 3000 |
. . . . . . . 8
β’ (π = β¨π₯, π¦β© β (((IsoβπΆ)βπ) β β
β ((IsoβπΆ)ββ¨π₯, π¦β©) β β
)) |
5 | 4 | rabxp 5724 |
. . . . . . 7
β’ {π β ((BaseβπΆ) Γ (BaseβπΆ)) β£ ((IsoβπΆ)βπ) β β
} = {β¨π₯, π¦β© β£ (π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ) β§ ((IsoβπΆ)ββ¨π₯, π¦β©) β β
)} |
6 | 5 | a1i 11 |
. . . . . 6
β’ (πΆ β Cat β {π β ((BaseβπΆ) Γ (BaseβπΆ)) β£ ((IsoβπΆ)βπ) β β
} = {β¨π₯, π¦β© β£ (π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ) β§ ((IsoβπΆ)ββ¨π₯, π¦β©) β β
)}) |
7 | 6 | releqd 5778 |
. . . . 5
β’ (πΆ β Cat β (Rel {π β ((BaseβπΆ) Γ (BaseβπΆ)) β£ ((IsoβπΆ)βπ) β β
} β Rel {β¨π₯, π¦β© β£ (π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ) β§ ((IsoβπΆ)ββ¨π₯, π¦β©) β β
)})) |
8 | 2, 7 | mpbird 256 |
. . . 4
β’ (πΆ β Cat β Rel {π β ((BaseβπΆ) Γ (BaseβπΆ)) β£ ((IsoβπΆ)βπ) β β
}) |
9 | | isofn 17721 |
. . . . . 6
β’ (πΆ β Cat β
(IsoβπΆ) Fn
((BaseβπΆ) Γ
(BaseβπΆ))) |
10 | | fvex 6904 |
. . . . . . 7
β’
(BaseβπΆ)
β V |
11 | | sqxpexg 7741 |
. . . . . . 7
β’
((BaseβπΆ)
β V β ((BaseβπΆ) Γ (BaseβπΆ)) β V) |
12 | 10, 11 | mp1i 13 |
. . . . . 6
β’ (πΆ β Cat β
((BaseβπΆ) Γ
(BaseβπΆ)) β
V) |
13 | | 0ex 5307 |
. . . . . . 7
β’ β
β V |
14 | 13 | a1i 11 |
. . . . . 6
β’ (πΆ β Cat β β
β V) |
15 | | suppvalfn 8153 |
. . . . . 6
β’
(((IsoβπΆ) Fn
((BaseβπΆ) Γ
(BaseβπΆ)) β§
((BaseβπΆ) Γ
(BaseβπΆ)) β V
β§ β
β V) β ((IsoβπΆ) supp β
) = {π β ((BaseβπΆ) Γ (BaseβπΆ)) β£ ((IsoβπΆ)βπ) β β
}) |
16 | 9, 12, 14, 15 | syl3anc 1371 |
. . . . 5
β’ (πΆ β Cat β
((IsoβπΆ) supp
β
) = {π β
((BaseβπΆ) Γ
(BaseβπΆ)) β£
((IsoβπΆ)βπ) β
β
}) |
17 | 16 | releqd 5778 |
. . . 4
β’ (πΆ β Cat β (Rel
((IsoβπΆ) supp
β
) β Rel {π
β ((BaseβπΆ)
Γ (BaseβπΆ))
β£ ((IsoβπΆ)βπ) β β
})) |
18 | 8, 17 | mpbird 256 |
. . 3
β’ (πΆ β Cat β Rel
((IsoβπΆ) supp
β
)) |
19 | | cicfval 17743 |
. . . 4
β’ (πΆ β Cat β (
βπ βπΆ) = ((IsoβπΆ) supp β
)) |
20 | 19 | releqd 5778 |
. . 3
β’ (πΆ β Cat β (Rel (
βπ βπΆ) β Rel ((IsoβπΆ) supp β
))) |
21 | 18, 20 | mpbird 256 |
. 2
β’ (πΆ β Cat β Rel (
βπ βπΆ)) |
22 | | cicsym 17750 |
. 2
β’ ((πΆ β Cat β§ π₯( βπ
βπΆ)π¦) β π¦( βπ βπΆ)π₯) |
23 | | cictr 17751 |
. . 3
β’ ((πΆ β Cat β§ π₯( βπ
βπΆ)π¦ β§ π¦( βπ βπΆ)π§) β π₯( βπ βπΆ)π§) |
24 | 23 | 3expb 1120 |
. 2
β’ ((πΆ β Cat β§ (π₯( βπ
βπΆ)π¦ β§ π¦( βπ βπΆ)π§)) β π₯( βπ βπΆ)π§) |
25 | | cicref 17747 |
. . 3
β’ ((πΆ β Cat β§ π₯ β (BaseβπΆ)) β π₯( βπ βπΆ)π₯) |
26 | | ciclcl 17748 |
. . 3
β’ ((πΆ β Cat β§ π₯( βπ
βπΆ)π₯) β π₯ β (BaseβπΆ)) |
27 | 25, 26 | impbida 799 |
. 2
β’ (πΆ β Cat β (π₯ β (BaseβπΆ) β π₯( βπ βπΆ)π₯)) |
28 | 21, 22, 24, 27 | iserd 8728 |
1
β’ (πΆ β Cat β (
βπ βπΆ) Er (BaseβπΆ)) |