Theorem elfunsALTV3

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

	Ref	Expression
Assertion	elfunsALTV3	⊢ ( 𝐹 ∈ FunsALTV ↔ ( ∀ 𝑢 ∀ 𝑥 ∀ 𝑦 ( ( 𝑢 𝐹 𝑥 ∧ 𝑢 𝐹 𝑦 ) → 𝑥 = 𝑦 ) ∧ 𝐹 ∈ Rels ) )

Proof

Step	Hyp	Ref	Expression
1		elfunsALTV	⊢ ( 𝐹 ∈ FunsALTV ↔ ( ≀ 𝐹 ∈ CnvRefRels ∧ 𝐹 ∈ Rels ) )
2		cosselcnvrefrels3	⊢ ( ≀ 𝐹 ∈ CnvRefRels ↔ ( ∀ 𝑢 ∀ 𝑥 ∀ 𝑦 ( ( 𝑢 𝐹 𝑥 ∧ 𝑢 𝐹 𝑦 ) → 𝑥 = 𝑦 ) ∧ ≀ 𝐹 ∈ Rels ) )
3		cosselrels	⊢ ( 𝐹 ∈ Rels → ≀ 𝐹 ∈ Rels )
4	3	biantrud	⊢ ( 𝐹 ∈ Rels → ( ∀ 𝑢 ∀ 𝑥 ∀ 𝑦 ( ( 𝑢 𝐹 𝑥 ∧ 𝑢 𝐹 𝑦 ) → 𝑥 = 𝑦 ) ↔ ( ∀ 𝑢 ∀ 𝑥 ∀ 𝑦 ( ( 𝑢 𝐹 𝑥 ∧ 𝑢 𝐹 𝑦 ) → 𝑥 = 𝑦 ) ∧ ≀ 𝐹 ∈ Rels ) ) )
5	2 4	bitr4id	⊢ ( 𝐹 ∈ Rels → ( ≀ 𝐹 ∈ CnvRefRels ↔ ∀ 𝑢 ∀ 𝑥 ∀ 𝑦 ( ( 𝑢 𝐹 𝑥 ∧ 𝑢 𝐹 𝑦 ) → 𝑥 = 𝑦 ) ) )
6	5	pm5.32ri	⊢ ( ( ≀ 𝐹 ∈ CnvRefRels ∧ 𝐹 ∈ Rels ) ↔ ( ∀ 𝑢 ∀ 𝑥 ∀ 𝑦 ( ( 𝑢 𝐹 𝑥 ∧ 𝑢 𝐹 𝑦 ) → 𝑥 = 𝑦 ) ∧ 𝐹 ∈ Rels ) )
7	1 6	bitri	⊢ ( 𝐹 ∈ FunsALTV ↔ ( ∀ 𝑢 ∀ 𝑥 ∀ 𝑦 ( ( 𝑢 𝐹 𝑥 ∧ 𝑢 𝐹 𝑦 ) → 𝑥 = 𝑦 ) ∧ 𝐹 ∈ Rels ) )