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

Metamath Proof Explorer

Theorem disjimeceqim2

Description: Disj implies injectivity (pairwise form). The same content as disjimeceqim but packaged for direct use with explicit hypotheses ( A e. dom R /\ B e. dom R ) . (Contributed by Peter Mazsa, 16-Feb-2026)

Ref Expression
Assertion disjimeceqim2 ( Disj 𝑅 → ( ( 𝐴 ∈ dom 𝑅 ∧ 𝐵 ∈ dom 𝑅 ) → ( [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 → 𝐴 = 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 simprl ⊢ ( ( Disj 𝑅 ∧ ( 𝐴 ∈ dom 𝑅 ∧ 𝐵 ∈ dom 𝑅 ) ) → 𝐴 ∈ dom 𝑅 )
2 simprr ⊢ ( ( Disj 𝑅 ∧ ( 𝐴 ∈ dom 𝑅 ∧ 𝐵 ∈ dom 𝑅 ) ) → 𝐵 ∈ dom 𝑅 )
3 eleq1 ⊢ ( 𝑢 = 𝐴 → ( 𝑢 ∈ dom 𝑅 ↔ 𝐴 ∈ dom 𝑅 ) )
4 eleq1 ⊢ ( 𝑣 = 𝐵 → ( 𝑣 ∈ dom 𝑅 ↔ 𝐵 ∈ dom 𝑅 ) )
5 3 4 bi2anan9 ⊢ ( ( 𝑢 = 𝐴 ∧ 𝑣 = 𝐵 ) → ( ( 𝑢 ∈ dom 𝑅 ∧ 𝑣 ∈ dom 𝑅 ) ↔ ( 𝐴 ∈ dom 𝑅 ∧ 𝐵 ∈ dom 𝑅 ) ) )
6 eceq1 ⊢ ( 𝑢 = 𝐴 → [ 𝑢 ] 𝑅 = [ 𝐴 ] 𝑅 )
7 eceq1 ⊢ ( 𝑣 = 𝐵 → [ 𝑣 ] 𝑅 = [ 𝐵 ] 𝑅 )
8 6 7 eqeqan12d ⊢ ( ( 𝑢 = 𝐴 ∧ 𝑣 = 𝐵 ) → ( [ 𝑢 ] 𝑅 = [ 𝑣 ] 𝑅 ↔ [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 ) )
9 eqeq12 ⊢ ( ( 𝑢 = 𝐴 ∧ 𝑣 = 𝐵 ) → ( 𝑢 = 𝑣 ↔ 𝐴 = 𝐵 ) )
10 8 9 imbi12d ⊢ ( ( 𝑢 = 𝐴 ∧ 𝑣 = 𝐵 ) → ( ( [ 𝑢 ] 𝑅 = [ 𝑣 ] 𝑅 → 𝑢 = 𝑣 ) ↔ ( [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 → 𝐴 = 𝐵 ) ) )
11 5 10 imbi12d ⊢ ( ( 𝑢 = 𝐴 ∧ 𝑣 = 𝐵 ) → ( ( ( 𝑢 ∈ dom 𝑅 ∧ 𝑣 ∈ dom 𝑅 ) → ( [ 𝑢 ] 𝑅 = [ 𝑣 ] 𝑅 → 𝑢 = 𝑣 ) ) ↔ ( ( 𝐴 ∈ dom 𝑅 ∧ 𝐵 ∈ dom 𝑅 ) → ( [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 → 𝐴 = 𝐵 ) ) ) )
12 disjimeceqim ⊢ ( Disj 𝑅 → ∀ 𝑢 ∈ dom 𝑅 ∀ 𝑣 ∈ dom 𝑅 ( [ 𝑢 ] 𝑅 = [ 𝑣 ] 𝑅 → 𝑢 = 𝑣 ) )
13 rsp2 ⊢ ( ∀ 𝑢 ∈ dom 𝑅 ∀ 𝑣 ∈ dom 𝑅 ( [ 𝑢 ] 𝑅 = [ 𝑣 ] 𝑅 → 𝑢 = 𝑣 ) → ( ( 𝑢 ∈ dom 𝑅 ∧ 𝑣 ∈ dom 𝑅 ) → ( [ 𝑢 ] 𝑅 = [ 𝑣 ] 𝑅 → 𝑢 = 𝑣 ) ) )
14 12 13 syl ⊢ ( Disj 𝑅 → ( ( 𝑢 ∈ dom 𝑅 ∧ 𝑣 ∈ dom 𝑅 ) → ( [ 𝑢 ] 𝑅 = [ 𝑣 ] 𝑅 → 𝑢 = 𝑣 ) ) )
15 14 adantr ⊢ ( ( Disj 𝑅 ∧ ( 𝐴 ∈ dom 𝑅 ∧ 𝐵 ∈ dom 𝑅 ) ) → ( ( 𝑢 ∈ dom 𝑅 ∧ 𝑣 ∈ dom 𝑅 ) → ( [ 𝑢 ] 𝑅 = [ 𝑣 ] 𝑅 → 𝑢 = 𝑣 ) ) )
16 1 2 11 15 vtocl2d ⊢ ( ( Disj 𝑅 ∧ ( 𝐴 ∈ dom 𝑅 ∧ 𝐵 ∈ dom 𝑅 ) ) → ( ( 𝐴 ∈ dom 𝑅 ∧ 𝐵 ∈ dom 𝑅 ) → ( [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 → 𝐴 = 𝐵 ) ) )
17 16 ex ⊢ ( Disj 𝑅 → ( ( 𝐴 ∈ dom 𝑅 ∧ 𝐵 ∈ dom 𝑅 ) → ( ( 𝐴 ∈ dom 𝑅 ∧ 𝐵 ∈ dom 𝑅 ) → ( [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 → 𝐴 = 𝐵 ) ) ) )
18 17 pm2.43d ⊢ ( Disj 𝑅 → ( ( 𝐴 ∈ dom 𝑅 ∧ 𝐵 ∈ dom 𝑅 ) → ( [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 → 𝐴 = 𝐵 ) ) )