Theorem dffunALTV5

Description: Alternate definition of the function relation predicate, cf. dfdisjALTV5 . (Contributed by Peter Mazsa, 5-Sep-2021)

	Ref	Expression
Assertion	dffunALTV5	⊢ ( FunALTV 𝐹 ↔ ( ∀ 𝑥 ∈ ran 𝐹 ∀ 𝑦 ∈ ran 𝐹 ( 𝑥 = 𝑦 ∨ ( [ 𝑥 ] ◡ 𝐹 ∩ [ 𝑦 ] ◡ 𝐹 ) = ∅ ) ∧ Rel 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		dffunALTV2	⊢ ( FunALTV 𝐹 ↔ ( ≀ 𝐹 ⊆ I ∧ Rel 𝐹 ) )
2		cossssid5	⊢ ( ≀ 𝐹 ⊆ I ↔ ∀ 𝑥 ∈ ran 𝐹 ∀ 𝑦 ∈ ran 𝐹 ( 𝑥 = 𝑦 ∨ ( [ 𝑥 ] ◡ 𝐹 ∩ [ 𝑦 ] ◡ 𝐹 ) = ∅ ) )
3	2	anbi1i	⊢ ( ( ≀ 𝐹 ⊆ I ∧ Rel 𝐹 ) ↔ ( ∀ 𝑥 ∈ ran 𝐹 ∀ 𝑦 ∈ ran 𝐹 ( 𝑥 = 𝑦 ∨ ( [ 𝑥 ] ◡ 𝐹 ∩ [ 𝑦 ] ◡ 𝐹 ) = ∅ ) ∧ Rel 𝐹 ) )
4	1 3	bitri	⊢ ( FunALTV 𝐹 ↔ ( ∀ 𝑥 ∈ ran 𝐹 ∀ 𝑦 ∈ ran 𝐹 ( 𝑥 = 𝑦 ∨ ( [ 𝑥 ] ◡ 𝐹 ∩ [ 𝑦 ] ◡ 𝐹 ) = ∅ ) ∧ Rel 𝐹 ) )