Theorem dffunsALTV5

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

	Ref	Expression
Assertion	dffunsALTV5	⊢ FunsALTV = { 𝑓 ∈ Rels ∣ ∀ 𝑥 ∈ ran 𝑓 ∀ 𝑦 ∈ ran 𝑓 ( 𝑥 = 𝑦 ∨ ( [ 𝑥 ] ◡ 𝑓 ∩ [ 𝑦 ] ◡ 𝑓 ) = ∅ ) }

Proof

Step	Hyp	Ref	Expression
1		dffunsALTV4	⊢ FunsALTV = { 𝑓 ∈ Rels ∣ ∀ 𝑢 ∃* 𝑥 𝑢 𝑓 𝑥 }
2		ineccnvmo2	⊢ ( ∀ 𝑥 ∈ ran 𝑓 ∀ 𝑦 ∈ ran 𝑓 ( 𝑥 = 𝑦 ∨ ( [ 𝑥 ] ◡ 𝑓 ∩ [ 𝑦 ] ◡ 𝑓 ) = ∅ ) ↔ ∀ 𝑢 ∃* 𝑥 𝑢 𝑓 𝑥 )
3	2	rabbii	⊢ { 𝑓 ∈ Rels ∣ ∀ 𝑥 ∈ ran 𝑓 ∀ 𝑦 ∈ ran 𝑓 ( 𝑥 = 𝑦 ∨ ( [ 𝑥 ] ◡ 𝑓 ∩ [ 𝑦 ] ◡ 𝑓 ) = ∅ ) } = { 𝑓 ∈ Rels ∣ ∀ 𝑢 ∃* 𝑥 𝑢 𝑓 𝑥 }
4	1 3	eqtr4i	⊢ FunsALTV = { 𝑓 ∈ Rels ∣ ∀ 𝑥 ∈ ran 𝑓 ∀ 𝑦 ∈ ran 𝑓 ( 𝑥 = 𝑦 ∨ ( [ 𝑥 ] ◡ 𝑓 ∩ [ 𝑦 ] ◡ 𝑓 ) = ∅ ) }