Metamath Proof Explorer

Theorem elfunsALTV5

Description: Elementhood in the class of functions. (Contributed by Peter Mazsa, 5-Sep-2021)

Ref Expression
Assertion elfunsALTV5 ⊢ F ∈ FunsALTV ↔ ∀ x ∈ ran ⁡ F ∀ y ∈ ran ⁡ F x = y ∨ x F -1 ∩ y F -1 = ∅ ∧ F ∈ Rels

Proof

Step Hyp Ref Expression
1 elfunsALTV ⊢ F ∈ FunsALTV ↔ ≀ F ∈ CnvRefRels ∧ F ∈ Rels
2 cosselrels ⊢ F ∈ Rels → ≀ F ∈ Rels
3 2 biantrud ⊢ F ∈ Rels → ∀ x ∈ ran ⁡ F ∀ y ∈ ran ⁡ F x = y ∨ x F -1 ∩ y F -1 = ∅ ↔ ∀ x ∈ ran ⁡ F ∀ y ∈ ran ⁡ F x = y ∨ x F -1 ∩ y F -1 = ∅ ∧ ≀ F ∈ Rels
4 cosselcnvrefrels5 ⊢ ≀ F ∈ CnvRefRels ↔ ∀ x ∈ ran ⁡ F ∀ y ∈ ran ⁡ F x = y ∨ x F -1 ∩ y F -1 = ∅ ∧ ≀ F ∈ Rels
5 3 4 syl6rbbr ⊢ F ∈ Rels → ≀ F ∈ CnvRefRels ↔ ∀ x ∈ ran ⁡ F ∀ y ∈ ran ⁡ F x = y ∨ x F -1 ∩ y F -1 = ∅
6 5 pm5.32ri ⊢ ≀ F ∈ CnvRefRels ∧ F ∈ Rels ↔ ∀ x ∈ ran ⁡ F ∀ y ∈ ran ⁡ F x = y ∨ x F -1 ∩ y F -1 = ∅ ∧ F ∈ Rels
7 1 6 bitri ⊢ F ∈ FunsALTV ↔ ∀ x ∈ ran ⁡ F ∀ y ∈ ran ⁡ F x = y ∨ x F -1 ∩ y F -1 = ∅ ∧ F ∈ Rels