Description: Define the function relation predicate, i.e., the function predicate. This definition of the function predicate (based on a more general, converse reflexive, relation) and the original definition of function in set.mm df-fun , are always the same, that is ( FunALTV F <-> Fun F ) , see funALTVfun .
The element of the class of functions and the function predicate are the same, that is ( F e. FunsALTV <-> FunALTV F ) when F is a set, see elfunsALTVfunALTV . Alternate definitions are dffunALTV2 , ... , dffunALTV5 . (Contributed by Peter Mazsa, 17-Jul-2021)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-funALTV | ⊢ ( FunALTV 𝐹 ↔ ( CnvRefRel ≀ 𝐹 ∧ Rel 𝐹 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cF | ⊢ 𝐹 | |
| 1 | 0 | wfunALTV | ⊢ FunALTV 𝐹 |
| 2 | 0 | ccoss | ⊢ ≀ 𝐹 |
| 3 | 2 | wcnvrefrel | ⊢ CnvRefRel ≀ 𝐹 |
| 4 | 0 | wrel | ⊢ Rel 𝐹 |
| 5 | 3 4 | wa | ⊢ ( CnvRefRel ≀ 𝐹 ∧ Rel 𝐹 ) |
| 6 | 1 5 | wb | ⊢ ( FunALTV 𝐹 ↔ ( CnvRefRel ≀ 𝐹 ∧ Rel 𝐹 ) ) |