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

Metamath Proof Explorer

Theorem eldisjs5

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

		Ref	Expression
	Assertion	eldisjs5	⊢ ( 𝑅 ∈ 𝑉 → ( 𝑅 ∈ Disjs ↔ ( ∀ 𝑢 ∈ dom 𝑅 ∀ 𝑣 ∈ dom 𝑅 ( 𝑢 = 𝑣 ∨ ( [ 𝑢 ] 𝑅 ∩ [ 𝑣 ] 𝑅 ) = ∅ ) ∧ 𝑅 ∈ Rels ) ) )

Proof

Step	Hyp	Ref	Expression
1		eldisjs2	⊢ ( 𝑅 ∈ Disjs ↔ ( ≀ ^◡ 𝑅 ⊆ I ∧ 𝑅 ∈ Rels ) )
2		cosscnvssid5	⊢ ( ( ≀ ^◡ 𝑅 ⊆ I ∧ Rel 𝑅 ) ↔ ( ∀ 𝑢 ∈ dom 𝑅 ∀ 𝑣 ∈ dom 𝑅 ( 𝑢 = 𝑣 ∨ ( [ 𝑢 ] 𝑅 ∩ [ 𝑣 ] 𝑅 ) = ∅ ) ∧ Rel 𝑅 ) )
3		elrelsrel	⊢ ( 𝑅 ∈ 𝑉 → ( 𝑅 ∈ Rels ↔ Rel 𝑅 ) )
4	3	anbi2d	⊢ ( 𝑅 ∈ 𝑉 → ( ( ≀ ^◡ 𝑅 ⊆ I ∧ 𝑅 ∈ Rels ) ↔ ( ≀ ^◡ 𝑅 ⊆ I ∧ Rel 𝑅 ) ) )
5	3	anbi2d	⊢ ( 𝑅 ∈ 𝑉 → ( ( ∀ 𝑢 ∈ dom 𝑅 ∀ 𝑣 ∈ dom 𝑅 ( 𝑢 = 𝑣 ∨ ( [ 𝑢 ] 𝑅 ∩ [ 𝑣 ] 𝑅 ) = ∅ ) ∧ 𝑅 ∈ Rels ) ↔ ( ∀ 𝑢 ∈ dom 𝑅 ∀ 𝑣 ∈ dom 𝑅 ( 𝑢 = 𝑣 ∨ ( [ 𝑢 ] 𝑅 ∩ [ 𝑣 ] 𝑅 ) = ∅ ) ∧ Rel 𝑅 ) ) )
6	4 5	bibi12d	⊢ ( 𝑅 ∈ 𝑉 → ( ( ( ≀ ^◡ 𝑅 ⊆ I ∧ 𝑅 ∈ Rels ) ↔ ( ∀ 𝑢 ∈ dom 𝑅 ∀ 𝑣 ∈ dom 𝑅 ( 𝑢 = 𝑣 ∨ ( [ 𝑢 ] 𝑅 ∩ [ 𝑣 ] 𝑅 ) = ∅ ) ∧ 𝑅 ∈ Rels ) ) ↔ ( ( ≀ ^◡ 𝑅 ⊆ I ∧ Rel 𝑅 ) ↔ ( ∀ 𝑢 ∈ dom 𝑅 ∀ 𝑣 ∈ dom 𝑅 ( 𝑢 = 𝑣 ∨ ( [ 𝑢 ] 𝑅 ∩ [ 𝑣 ] 𝑅 ) = ∅ ) ∧ Rel 𝑅 ) ) ) )
7	2 6	mpbiri	⊢ ( 𝑅 ∈ 𝑉 → ( ( ≀ ^◡ 𝑅 ⊆ I ∧ 𝑅 ∈ Rels ) ↔ ( ∀ 𝑢 ∈ dom 𝑅 ∀ 𝑣 ∈ dom 𝑅 ( 𝑢 = 𝑣 ∨ ( [ 𝑢 ] 𝑅 ∩ [ 𝑣 ] 𝑅 ) = ∅ ) ∧ 𝑅 ∈ Rels ) ) )
8	1 7	bitrid	⊢ ( 𝑅 ∈ 𝑉 → ( 𝑅 ∈ Disjs ↔ ( ∀ 𝑢 ∈ dom 𝑅 ∀ 𝑣 ∈ dom 𝑅 ( 𝑢 = 𝑣 ∨ ( [ 𝑢 ] 𝑅 ∩ [ 𝑣 ] 𝑅 ) = ∅ ) ∧ 𝑅 ∈ Rels ) ) )