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

Metamath Proof Explorer

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 ( 𝑅 ↾ 𝐴 ) ↔ ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( 𝑢 = 𝑣 ∨ ( [ 𝑢 ] 𝑅 ∩ [ 𝑣 ] 𝑅 ) = ∅ ) ) )