Metamath Proof Explorer

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 F ↔ Fun ⁡ F

Proof

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