Theorem funALTVfun

Description: Our definition of the function predicate df-funALTV (based on a more general, converse reflexive, relation) and the original definition of function in set.mm df-fun , are always the same and interchangeable. (Contributed by Peter Mazsa, 27-Jul-2021)

	Ref	Expression
Assertion	funALTVfun	⊢ ( FunALTV 𝐹 ↔ Fun 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		cnvrefrelcoss2	⊢ ( CnvRefRel ≀ 𝐹 ↔ ≀ 𝐹 ⊆ I )
2		dfcoss3	⊢ ≀ 𝐹 = ( 𝐹 ∘ ◡ 𝐹 )
3	2	sseq1i	⊢ ( ≀ 𝐹 ⊆ I ↔ ( 𝐹 ∘ ◡ 𝐹 ) ⊆ I )
4	1 3	bitri	⊢ ( CnvRefRel ≀ 𝐹 ↔ ( 𝐹 ∘ ◡ 𝐹 ) ⊆ I )
5	4	anbi2ci	⊢ ( ( CnvRefRel ≀ 𝐹 ∧ Rel 𝐹 ) ↔ ( Rel 𝐹 ∧ ( 𝐹 ∘ ◡ 𝐹 ) ⊆ I ) )
6		df-funALTV	⊢ ( FunALTV 𝐹 ↔ ( CnvRefRel ≀ 𝐹 ∧ Rel 𝐹 ) )
7		df-fun	⊢ ( Fun 𝐹 ↔ ( Rel 𝐹 ∧ ( 𝐹 ∘ ◡ 𝐹 ) ⊆ I ) )
8	5 6 7	3bitr4i	⊢ ( FunALTV 𝐹 ↔ Fun 𝐹 )