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	⊢ ( 𝐹 Struct 𝑋 → Fun ◡ ◡ 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		structn0fun	⊢ ( 𝐹 Struct 𝑋 → Fun ( 𝐹 ∖ { ∅ } ) )
2		structcnvcnv	⊢ ( 𝐹 Struct 𝑋 → ◡ ◡ 𝐹 = ( 𝐹 ∖ { ∅ } ) )
3	2	funeqd	⊢ ( 𝐹 Struct 𝑋 → ( Fun ◡ ◡ 𝐹 ↔ Fun ( 𝐹 ∖ { ∅ } ) ) )
4	1 3	mpbird	⊢ ( 𝐹 Struct 𝑋 → Fun ◡ ◡ 𝐹 )