Metamath Proof Explorer

Theorem qmapeldisjsim

Description: Injectivity of coset map from QMap being disjoint (implication form): under the Disjs condition on QMap R , the coset assignment is injective on dom R . (Contributed by Peter Mazsa, 16-Feb-2026)

Ref Expression
Assertion qmapeldisjsim ( ( 𝑅 ∈ 𝑉 ∧ QMap 𝑅 ∈ Disjs ∧ ( 𝐴 ∈ dom 𝑅 ∧ 𝐵 ∈ dom 𝑅 ) ) → ( [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 → 𝐴 = 𝐵 ) )

Proof

Step Hyp Ref Expression
1 qmapeldisjs ⊢ ( 𝑅 ∈ 𝑉 → ( QMap 𝑅 ∈ Disjs ↔ Disj QMap 𝑅 ) )
2 disjimeceqim2 ⊢ ( Disj QMap 𝑅 → ( ( 𝐴 ∈ dom QMap 𝑅 ∧ 𝐵 ∈ dom QMap 𝑅 ) → ( [ 𝐴 ] QMap 𝑅 = [ 𝐵 ] QMap 𝑅 → 𝐴 = 𝐵 ) ) )
3 dmqmap ⊢ ( 𝑅 ∈ 𝑉 → dom QMap 𝑅 = dom 𝑅 )
4 3 eleq2d ⊢ ( 𝑅 ∈ 𝑉 → ( 𝐴 ∈ dom QMap 𝑅 ↔ 𝐴 ∈ dom 𝑅 ) )
5 3 eleq2d ⊢ ( 𝑅 ∈ 𝑉 → ( 𝐵 ∈ dom QMap 𝑅 ↔ 𝐵 ∈ dom 𝑅 ) )
6 4 5 anbi12d ⊢ ( 𝑅 ∈ 𝑉 → ( ( 𝐴 ∈ dom QMap 𝑅 ∧ 𝐵 ∈ dom QMap 𝑅 ) ↔ ( 𝐴 ∈ dom 𝑅 ∧ 𝐵 ∈ dom 𝑅 ) ) )
7 6 pm5.32i ⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝐴 ∈ dom QMap 𝑅 ∧ 𝐵 ∈ dom QMap 𝑅 ) ) ↔ ( 𝑅 ∈ 𝑉 ∧ ( 𝐴 ∈ dom 𝑅 ∧ 𝐵 ∈ dom 𝑅 ) ) )
8 7 imbi1i ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ ( 𝐴 ∈ dom QMap 𝑅 ∧ 𝐵 ∈ dom QMap 𝑅 ) ) → ( [ 𝐴 ] QMap 𝑅 = [ 𝐵 ] QMap 𝑅 → 𝐴 = 𝐵 ) ) ↔ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝐴 ∈ dom 𝑅 ∧ 𝐵 ∈ dom 𝑅 ) ) → ( [ 𝐴 ] QMap 𝑅 = [ 𝐵 ] QMap 𝑅 → 𝐴 = 𝐵 ) ) )
9 ecqmap ⊢ ( 𝐴 ∈ dom 𝑅 → [ 𝐴 ] QMap 𝑅 = { [ 𝐴 ] 𝑅 } )
10 ecqmap ⊢ ( 𝐵 ∈ dom 𝑅 → [ 𝐵 ] QMap 𝑅 = { [ 𝐵 ] 𝑅 } )
11 9 10 eqeqan12d ⊢ ( ( 𝐴 ∈ dom 𝑅 ∧ 𝐵 ∈ dom 𝑅 ) → ( [ 𝐴 ] QMap 𝑅 = [ 𝐵 ] QMap 𝑅 ↔ { [ 𝐴 ] 𝑅 } = { [ 𝐵 ] 𝑅 } ) )
12 11 imbi1d ⊢ ( ( 𝐴 ∈ dom 𝑅 ∧ 𝐵 ∈ dom 𝑅 ) → ( ( [ 𝐴 ] QMap 𝑅 = [ 𝐵 ] QMap 𝑅 → 𝐴 = 𝐵 ) ↔ ( { [ 𝐴 ] 𝑅 } = { [ 𝐵 ] 𝑅 } → 𝐴 = 𝐵 ) ) )
13 ecexg ⊢ ( 𝑅 ∈ 𝑉 → [ 𝐴 ] 𝑅 ∈ V )
14 sneqbg ⊢ ( [ 𝐴 ] 𝑅 ∈ V → ( { [ 𝐴 ] 𝑅 } = { [ 𝐵 ] 𝑅 } ↔ [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 ) )
15 13 14 syl ⊢ ( 𝑅 ∈ 𝑉 → ( { [ 𝐴 ] 𝑅 } = { [ 𝐵 ] 𝑅 } ↔ [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 ) )
16 15 imbi1d ⊢ ( 𝑅 ∈ 𝑉 → ( ( { [ 𝐴 ] 𝑅 } = { [ 𝐵 ] 𝑅 } → 𝐴 = 𝐵 ) ↔ ( [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 → 𝐴 = 𝐵 ) ) )
17 12 16 sylan9bbr ⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝐴 ∈ dom 𝑅 ∧ 𝐵 ∈ dom 𝑅 ) ) → ( ( [ 𝐴 ] QMap 𝑅 = [ 𝐵 ] QMap 𝑅 → 𝐴 = 𝐵 ) ↔ ( [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 → 𝐴 = 𝐵 ) ) )
18 17 pm5.74i ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ ( 𝐴 ∈ dom 𝑅 ∧ 𝐵 ∈ dom 𝑅 ) ) → ( [ 𝐴 ] QMap 𝑅 = [ 𝐵 ] QMap 𝑅 → 𝐴 = 𝐵 ) ) ↔ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝐴 ∈ dom 𝑅 ∧ 𝐵 ∈ dom 𝑅 ) ) → ( [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 → 𝐴 = 𝐵 ) ) )
19 8 18 bitri ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ ( 𝐴 ∈ dom QMap 𝑅 ∧ 𝐵 ∈ dom QMap 𝑅 ) ) → ( [ 𝐴 ] QMap 𝑅 = [ 𝐵 ] QMap 𝑅 → 𝐴 = 𝐵 ) ) ↔ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝐴 ∈ dom 𝑅 ∧ 𝐵 ∈ dom 𝑅 ) ) → ( [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 → 𝐴 = 𝐵 ) ) )
20 impexp ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ ( 𝐴 ∈ dom QMap 𝑅 ∧ 𝐵 ∈ dom QMap 𝑅 ) ) → ( [ 𝐴 ] QMap 𝑅 = [ 𝐵 ] QMap 𝑅 → 𝐴 = 𝐵 ) ) ↔ ( 𝑅 ∈ 𝑉 → ( ( 𝐴 ∈ dom QMap 𝑅 ∧ 𝐵 ∈ dom QMap 𝑅 ) → ( [ 𝐴 ] QMap 𝑅 = [ 𝐵 ] QMap 𝑅 → 𝐴 = 𝐵 ) ) ) )
21 impexp ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ ( 𝐴 ∈ dom 𝑅 ∧ 𝐵 ∈ dom 𝑅 ) ) → ( [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 → 𝐴 = 𝐵 ) ) ↔ ( 𝑅 ∈ 𝑉 → ( ( 𝐴 ∈ dom 𝑅 ∧ 𝐵 ∈ dom 𝑅 ) → ( [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 → 𝐴 = 𝐵 ) ) ) )
22 19 20 21 3bitr3i ⊢ ( ( 𝑅 ∈ 𝑉 → ( ( 𝐴 ∈ dom QMap 𝑅 ∧ 𝐵 ∈ dom QMap 𝑅 ) → ( [ 𝐴 ] QMap 𝑅 = [ 𝐵 ] QMap 𝑅 → 𝐴 = 𝐵 ) ) ) ↔ ( 𝑅 ∈ 𝑉 → ( ( 𝐴 ∈ dom 𝑅 ∧ 𝐵 ∈ dom 𝑅 ) → ( [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 → 𝐴 = 𝐵 ) ) ) )
23 22 pm5.74ri ⊢ ( 𝑅 ∈ 𝑉 → ( ( ( 𝐴 ∈ dom QMap 𝑅 ∧ 𝐵 ∈ dom QMap 𝑅 ) → ( [ 𝐴 ] QMap 𝑅 = [ 𝐵 ] QMap 𝑅 → 𝐴 = 𝐵 ) ) ↔ ( ( 𝐴 ∈ dom 𝑅 ∧ 𝐵 ∈ dom 𝑅 ) → ( [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 → 𝐴 = 𝐵 ) ) ) )
24 2 23 imbitrid ⊢ ( 𝑅 ∈ 𝑉 → ( Disj QMap 𝑅 → ( ( 𝐴 ∈ dom 𝑅 ∧ 𝐵 ∈ dom 𝑅 ) → ( [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 → 𝐴 = 𝐵 ) ) ) )
25 1 24 sylbid ⊢ ( 𝑅 ∈ 𝑉 → ( QMap 𝑅 ∈ Disjs → ( ( 𝐴 ∈ dom 𝑅 ∧ 𝐵 ∈ dom 𝑅 ) → ( [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 → 𝐴 = 𝐵 ) ) ) )
26 25 3imp ⊢ ( ( 𝑅 ∈ 𝑉 ∧ QMap 𝑅 ∈ Disjs ∧ ( 𝐴 ∈ dom 𝑅 ∧ 𝐵 ∈ dom 𝑅 ) ) → ( [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 → 𝐴 = 𝐵 ) )