Theorem disjres

Description: Disjoint restriction. (Contributed by Peter Mazsa, 25-Aug-2023)

	Ref	Expression
Assertion	disjres	⊢ ( Rel 𝑅 → ( Disj ( 𝑅 ↾ 𝐴 ) ↔ ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( 𝑢 = 𝑣 ∨ ( [ 𝑢 ] 𝑅 ∩ [ 𝑣 ] 𝑅 ) = ∅ ) ) )

Proof

Step	Hyp	Ref	Expression
1		relres	⊢ Rel ( 𝑅 ↾ 𝐴 )
2		dfdisjALTV4	⊢ ( Disj ( 𝑅 ↾ 𝐴 ) ↔ ( ∀ 𝑥 ∃* 𝑢 𝑢 ( 𝑅 ↾ 𝐴 ) 𝑥 ∧ Rel ( 𝑅 ↾ 𝐴 ) ) )
3	1 2	mpbiran2	⊢ ( Disj ( 𝑅 ↾ 𝐴 ) ↔ ∀ 𝑥 ∃* 𝑢 𝑢 ( 𝑅 ↾ 𝐴 ) 𝑥 )
4		brres	⊢ ( 𝑥 ∈ V → ( 𝑢 ( 𝑅 ↾ 𝐴 ) 𝑥 ↔ ( 𝑢 ∈ 𝐴 ∧ 𝑢 𝑅 𝑥 ) ) )
5	4	elv	⊢ ( 𝑢 ( 𝑅 ↾ 𝐴 ) 𝑥 ↔ ( 𝑢 ∈ 𝐴 ∧ 𝑢 𝑅 𝑥 ) )
6	5	mobii	⊢ ( ∃* 𝑢 𝑢 ( 𝑅 ↾ 𝐴 ) 𝑥 ↔ ∃* 𝑢 ( 𝑢 ∈ 𝐴 ∧ 𝑢 𝑅 𝑥 ) )
7		df-rmo	⊢ ( ∃* 𝑢 ∈ 𝐴 𝑢 𝑅 𝑥 ↔ ∃* 𝑢 ( 𝑢 ∈ 𝐴 ∧ 𝑢 𝑅 𝑥 ) )
8	6 7	bitr4i	⊢ ( ∃* 𝑢 𝑢 ( 𝑅 ↾ 𝐴 ) 𝑥 ↔ ∃* 𝑢 ∈ 𝐴 𝑢 𝑅 𝑥 )
9	8	albii	⊢ ( ∀ 𝑥 ∃* 𝑢 𝑢 ( 𝑅 ↾ 𝐴 ) 𝑥 ↔ ∀ 𝑥 ∃* 𝑢 ∈ 𝐴 𝑢 𝑅 𝑥 )
10	3 9	bitri	⊢ ( Disj ( 𝑅 ↾ 𝐴 ) ↔ ∀ 𝑥 ∃* 𝑢 ∈ 𝐴 𝑢 𝑅 𝑥 )
11		id	⊢ ( 𝑢 = 𝑣 → 𝑢 = 𝑣 )
12	11	inecmo	⊢ ( Rel 𝑅 → ( ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( 𝑢 = 𝑣 ∨ ( [ 𝑢 ] 𝑅 ∩ [ 𝑣 ] 𝑅 ) = ∅ ) ↔ ∀ 𝑥 ∃* 𝑢 ∈ 𝐴 𝑢 𝑅 𝑥 ) )
13	10 12	bitr4id	⊢ ( Rel 𝑅 → ( Disj ( 𝑅 ↾ 𝐴 ) ↔ ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( 𝑢 = 𝑣 ∨ ( [ 𝑢 ] 𝑅 ∩ [ 𝑣 ] 𝑅 ) = ∅ ) ) )