Theorem dfdisjs5

Description: Alternate definition of the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021)

	Ref	Expression
Assertion	dfdisjs5	⊢ Disjs = { 𝑟 ∈ Rels ∣ ∀ 𝑢 ∈ dom 𝑟 ∀ 𝑣 ∈ dom 𝑟 ( 𝑢 = 𝑣 ∨ ( [ 𝑢 ] 𝑟 ∩ [ 𝑣 ] 𝑟 ) = ∅ ) }

Proof

Step	Hyp	Ref	Expression
1		dfdisjs2	⊢ Disjs = { 𝑟 ∈ Rels ∣ ≀ ◡ 𝑟 ⊆ I }
2		cosscnvssid5	⊢ ( ( ≀ ◡ 𝑟 ⊆ I ∧ Rel 𝑟 ) ↔ ( ∀ 𝑢 ∈ dom 𝑟 ∀ 𝑣 ∈ dom 𝑟 ( 𝑢 = 𝑣 ∨ ( [ 𝑢 ] 𝑟 ∩ [ 𝑣 ] 𝑟 ) = ∅ ) ∧ Rel 𝑟 ) )
3		elrelsrelim	⊢ ( 𝑟 ∈ Rels → Rel 𝑟 )
4	3	biantrud	⊢ ( 𝑟 ∈ Rels → ( ≀ ◡ 𝑟 ⊆ I ↔ ( ≀ ◡ 𝑟 ⊆ I ∧ Rel 𝑟 ) ) )
5	3	biantrud	⊢ ( 𝑟 ∈ Rels → ( ∀ 𝑢 ∈ dom 𝑟 ∀ 𝑣 ∈ dom 𝑟 ( 𝑢 = 𝑣 ∨ ( [ 𝑢 ] 𝑟 ∩ [ 𝑣 ] 𝑟 ) = ∅ ) ↔ ( ∀ 𝑢 ∈ dom 𝑟 ∀ 𝑣 ∈ dom 𝑟 ( 𝑢 = 𝑣 ∨ ( [ 𝑢 ] 𝑟 ∩ [ 𝑣 ] 𝑟 ) = ∅ ) ∧ Rel 𝑟 ) ) )
6	4 5	bibi12d	⊢ ( 𝑟 ∈ Rels → ( ( ≀ ◡ 𝑟 ⊆ I ↔ ∀ 𝑢 ∈ dom 𝑟 ∀ 𝑣 ∈ dom 𝑟 ( 𝑢 = 𝑣 ∨ ( [ 𝑢 ] 𝑟 ∩ [ 𝑣 ] 𝑟 ) = ∅ ) ) ↔ ( ( ≀ ◡ 𝑟 ⊆ I ∧ Rel 𝑟 ) ↔ ( ∀ 𝑢 ∈ dom 𝑟 ∀ 𝑣 ∈ dom 𝑟 ( 𝑢 = 𝑣 ∨ ( [ 𝑢 ] 𝑟 ∩ [ 𝑣 ] 𝑟 ) = ∅ ) ∧ Rel 𝑟 ) ) ) )
7	2 6	mpbiri	⊢ ( 𝑟 ∈ Rels → ( ≀ ◡ 𝑟 ⊆ I ↔ ∀ 𝑢 ∈ dom 𝑟 ∀ 𝑣 ∈ dom 𝑟 ( 𝑢 = 𝑣 ∨ ( [ 𝑢 ] 𝑟 ∩ [ 𝑣 ] 𝑟 ) = ∅ ) ) )
8	1 7	rabimbieq	⊢ Disjs = { 𝑟 ∈ Rels ∣ ∀ 𝑢 ∈ dom 𝑟 ∀ 𝑣 ∈ dom 𝑟 ( 𝑢 = 𝑣 ∨ ( [ 𝑢 ] 𝑟 ∩ [ 𝑣 ] 𝑟 ) = ∅ ) }