ecqmap

Description: QMap fibers are singletons of blocks. Makes QMap behave like a "block constructor function" on dom R . (Contributed by Peter Mazsa, 14-Feb-2026)

		Ref	Expression
	Assertion	ecqmap	⊢ ( 𝐴 ∈ dom 𝑅 → [ 𝐴 ] QMap 𝑅 = { [ 𝐴 ] 𝑅 } )

Proof

Step	Hyp	Ref	Expression
1		dfec2	⊢ ( 𝐴 ∈ dom 𝑅 → [ 𝐴 ] QMap 𝑅 = { 𝑦 ∣ 𝐴 QMap 𝑅 𝑦 } )
2		eleq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ dom 𝑅 ↔ 𝐴 ∈ dom 𝑅 ) )
3	2	adantr	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑧 = 𝑦 ) → ( 𝑥 ∈ dom 𝑅 ↔ 𝐴 ∈ dom 𝑅 ) )
4		eceq1	⊢ ( 𝑥 = 𝐴 → [ 𝑥 ] 𝑅 = [ 𝐴 ] 𝑅 )
5	4	eqeqan2d	⊢ ( ( 𝑧 = 𝑦 ∧ 𝑥 = 𝐴 ) → ( 𝑧 = [ 𝑥 ] 𝑅 ↔ 𝑦 = [ 𝐴 ] 𝑅 ) )
6	5	ancoms	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑧 = 𝑦 ) → ( 𝑧 = [ 𝑥 ] 𝑅 ↔ 𝑦 = [ 𝐴 ] 𝑅 ) )
7	3 6	anbi12d	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑧 = 𝑦 ) → ( ( 𝑥 ∈ dom 𝑅 ∧ 𝑧 = [ 𝑥 ] 𝑅 ) ↔ ( 𝐴 ∈ dom 𝑅 ∧ 𝑦 = [ 𝐴 ] 𝑅 ) ) )
8		dfqmap3	⊢ QMap 𝑅 = { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑥 ∈ dom 𝑅 ∧ 𝑧 = [ 𝑥 ] 𝑅 ) }
9	7 8	brabga	⊢ ( ( 𝐴 ∈ dom 𝑅 ∧ 𝑦 ∈ V ) → ( 𝐴 QMap 𝑅 𝑦 ↔ ( 𝐴 ∈ dom 𝑅 ∧ 𝑦 = [ 𝐴 ] 𝑅 ) ) )
10	9	elvd	⊢ ( 𝐴 ∈ dom 𝑅 → ( 𝐴 QMap 𝑅 𝑦 ↔ ( 𝐴 ∈ dom 𝑅 ∧ 𝑦 = [ 𝐴 ] 𝑅 ) ) )
11	10	abbidv	⊢ ( 𝐴 ∈ dom 𝑅 → { 𝑦 ∣ 𝐴 QMap 𝑅 𝑦 } = { 𝑦 ∣ ( 𝐴 ∈ dom 𝑅 ∧ 𝑦 = [ 𝐴 ] 𝑅 ) } )
12		inab	⊢ ( { 𝑦 ∣ 𝐴 ∈ dom 𝑅 } ∩ { 𝑦 ∣ 𝑦 = [ 𝐴 ] 𝑅 } ) = { 𝑦 ∣ ( 𝐴 ∈ dom 𝑅 ∧ 𝑦 = [ 𝐴 ] 𝑅 ) }
13	11 12	eqtr4di	⊢ ( 𝐴 ∈ dom 𝑅 → { 𝑦 ∣ 𝐴 QMap 𝑅 𝑦 } = ( { 𝑦 ∣ 𝐴 ∈ dom 𝑅 } ∩ { 𝑦 ∣ 𝑦 = [ 𝐴 ] 𝑅 } ) )
14		ax-5	⊢ ( 𝐴 ∈ dom 𝑅 → ∀ 𝑦 𝐴 ∈ dom 𝑅 )
15		abv	⊢ ( { 𝑦 ∣ 𝐴 ∈ dom 𝑅 } = V ↔ ∀ 𝑦 𝐴 ∈ dom 𝑅 )
16	14 15	sylibr	⊢ ( 𝐴 ∈ dom 𝑅 → { 𝑦 ∣ 𝐴 ∈ dom 𝑅 } = V )
17	16	ineq1d	⊢ ( 𝐴 ∈ dom 𝑅 → ( { 𝑦 ∣ 𝐴 ∈ dom 𝑅 } ∩ { 𝑦 ∣ 𝑦 = [ 𝐴 ] 𝑅 } ) = ( V ∩ { 𝑦 ∣ 𝑦 = [ 𝐴 ] 𝑅 } ) )
18		inv1	⊢ ( { 𝑦 ∣ 𝑦 = [ 𝐴 ] 𝑅 } ∩ V ) = { 𝑦 ∣ 𝑦 = [ 𝐴 ] 𝑅 }
19	18	ineqcomi	⊢ ( V ∩ { 𝑦 ∣ 𝑦 = [ 𝐴 ] 𝑅 } ) = { 𝑦 ∣ 𝑦 = [ 𝐴 ] 𝑅 }
20	17 19	eqtrdi	⊢ ( 𝐴 ∈ dom 𝑅 → ( { 𝑦 ∣ 𝐴 ∈ dom 𝑅 } ∩ { 𝑦 ∣ 𝑦 = [ 𝐴 ] 𝑅 } ) = { 𝑦 ∣ 𝑦 = [ 𝐴 ] 𝑅 } )
21	13 20	eqtrd	⊢ ( 𝐴 ∈ dom 𝑅 → { 𝑦 ∣ 𝐴 QMap 𝑅 𝑦 } = { 𝑦 ∣ 𝑦 = [ 𝐴 ] 𝑅 } )
22		df-sn	⊢ { [ 𝐴 ] 𝑅 } = { 𝑦 ∣ 𝑦 = [ 𝐴 ] 𝑅 }
23	21 22	eqtr4di	⊢ ( 𝐴 ∈ dom 𝑅 → { 𝑦 ∣ 𝐴 QMap 𝑅 𝑦 } = { [ 𝐴 ] 𝑅 } )
24	1 23	eqtrd	⊢ ( 𝐴 ∈ dom 𝑅 → [ 𝐴 ] QMap 𝑅 = { [ 𝐴 ] 𝑅 } )

Metamath Proof Explorer

Theorem ecqmap

Proof