Theorem dfdisjs4

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

	Ref	Expression
Assertion	dfdisjs4	⊢ Disjs = { 𝑟 ∈ Rels ∣ ∀ 𝑥 ∃* 𝑢 𝑢 𝑟 𝑥 }

Proof

Step	Hyp	Ref	Expression
1		dfdisjs2	⊢ Disjs = { 𝑟 ∈ Rels ∣ ≀ ◡ 𝑟 ⊆ I }
2		cosscnvssid4	⊢ ( ≀ ◡ 𝑟 ⊆ I ↔ ∀ 𝑥 ∃* 𝑢 𝑢 𝑟 𝑥 )
3	1 2	rabbieq	⊢ Disjs = { 𝑟 ∈ Rels ∣ ∀ 𝑥 ∃* 𝑢 𝑢 𝑟 𝑥 }