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

Metamath Proof Explorer

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 𝑟 ( 𝑢 = 𝑣 ∨ ( [ 𝑢 ] 𝑟 ∩ [ 𝑣 ] 𝑟 ) = ∅ ) }