Metamath Proof Explorer


Theorem elfunsALTV5

Description: Elementhood in the class of functions. (Contributed by Peter Mazsa, 5-Sep-2021)

Ref Expression
Assertion elfunsALTV5 F FunsALTV x ran F y ran F x = y x F -1 y F -1 = F Rels

Proof

Step Hyp Ref Expression
1 elfunsALTV F FunsALTV F CnvRefRels F Rels
2 cosselcnvrefrels5 F CnvRefRels x ran F y ran F x = y x F -1 y F -1 = F Rels
3 cosselrels F Rels F Rels
4 3 biantrud F Rels x ran F y ran F x = y x F -1 y F -1 = x ran F y ran F x = y x F -1 y F -1 = F Rels
5 2 4 bitr4id F Rels F CnvRefRels x ran F y ran F x = y x F -1 y F -1 =
6 5 pm5.32ri F CnvRefRels F Rels x ran F y ran F x = y x F -1 y F -1 = F Rels
7 1 6 bitri F FunsALTV x ran F y ran F x = y x F -1 y F -1 = F Rels