This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem elfunsALTV5

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

Ref Expression
Assertion elfunsALTV5 ( 𝐹 ∈ FunsALTV ↔ ( ∀ 𝑥 ∈ ran 𝐹 ∀ 𝑦 ∈ ran 𝐹 ( 𝑥 = 𝑦 ∨ ( [ 𝑥 ] ◡ 𝐹 ∩ [ 𝑦 ] ◡ 𝐹 ) = ∅ ) ∧ 𝐹 ∈ Rels ) )

Proof

Step Hyp Ref Expression
1 elfunsALTV ⊢ ( 𝐹 ∈ FunsALTV ↔ ( ≀ 𝐹 ∈ CnvRefRels ∧ 𝐹 ∈ Rels ) )
2 cosselcnvrefrels5 ⊢ ( ≀ 𝐹 ∈ CnvRefRels ↔ ( ∀ 𝑥 ∈ ran 𝐹 ∀ 𝑦 ∈ ran 𝐹 ( 𝑥 = 𝑦 ∨ ( [ 𝑥 ] ◡ 𝐹 ∩ [ 𝑦 ] ◡ 𝐹 ) = ∅ ) ∧ ≀ 𝐹 ∈ Rels ) )
3 cosselrels ⊢ ( 𝐹 ∈ Rels → ≀ 𝐹 ∈ Rels )
4 3 biantrud ⊢ ( 𝐹 ∈ Rels → ( ∀ 𝑥 ∈ ran 𝐹 ∀ 𝑦 ∈ ran 𝐹 ( 𝑥 = 𝑦 ∨ ( [ 𝑥 ] ◡ 𝐹 ∩ [ 𝑦 ] ◡ 𝐹 ) = ∅ ) ↔ ( ∀ 𝑥 ∈ ran 𝐹 ∀ 𝑦 ∈ ran 𝐹 ( 𝑥 = 𝑦 ∨ ( [ 𝑥 ] ◡ 𝐹 ∩ [ 𝑦 ] ◡ 𝐹 ) = ∅ ) ∧ ≀ 𝐹 ∈ Rels ) ) )
5 2 4 bitr4id ⊢ ( 𝐹 ∈ Rels → ( ≀ 𝐹 ∈ CnvRefRels ↔ ∀ 𝑥 ∈ ran 𝐹 ∀ 𝑦 ∈ ran 𝐹 ( 𝑥 = 𝑦 ∨ ( [ 𝑥 ] ◡ 𝐹 ∩ [ 𝑦 ] ◡ 𝐹 ) = ∅ ) ) )
6 5 pm5.32ri ⊢ ( ( ≀ 𝐹 ∈ CnvRefRels ∧ 𝐹 ∈ Rels ) ↔ ( ∀ 𝑥 ∈ ran 𝐹 ∀ 𝑦 ∈ ran 𝐹 ( 𝑥 = 𝑦 ∨ ( [ 𝑥 ] ◡ 𝐹 ∩ [ 𝑦 ] ◡ 𝐹 ) = ∅ ) ∧ 𝐹 ∈ Rels ) )
7 1 6 bitri ⊢ ( 𝐹 ∈ FunsALTV ↔ ( ∀ 𝑥 ∈ ran 𝐹 ∀ 𝑦 ∈ ran 𝐹 ( 𝑥 = 𝑦 ∨ ( [ 𝑥 ] ◡ 𝐹 ∩ [ 𝑦 ] ◡ 𝐹 ) = ∅ ) ∧ 𝐹 ∈ Rels ) )