Metamath Proof Explorer

Theorem structfung

Description: The converse of the converse of a structure is a function. Closed form of structfun . (Contributed by AV, 12-Nov-2021)

Ref Expression
Assertion structfung 
|- ( F Struct X -> Fun `' `' F )

Proof

Step Hyp Ref Expression
1 structn0fun 
 |-  ( F Struct X -> Fun ( F \ { (/) } ) )
2 structcnvcnv 
 |-  ( F Struct X -> `' `' F = ( F \ { (/) } ) )
3 2 funeqd 
 |-  ( F Struct X -> ( Fun `' `' F <-> Fun ( F \ { (/) } ) ) )
4 1 3 mpbird 
 |-  ( F Struct X -> Fun `' `' F )