Theorem 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	Could not format assertion : No typesetting found for |- ( A e. dom R -> [ A ] QMap R = { [ A ] R } ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		dfec2	Could not format ( A e. dom R -> [ A ] QMap R = { y | A QMap R y } ) : No typesetting found for |- ( A e. dom R -> [ A ] QMap R = { y | A QMap R y } ) with typecode |-
2		eleq1	$$⊢x=A\to \left(x\in \mathrm{dom}R\leftrightarrow A\in \mathrm{dom}R\right)$$
3	2	adantr	$$⊢\left(x=A\wedge z=y\right)\to \left(x\in \mathrm{dom}R\leftrightarrow A\in \mathrm{dom}R\right)$$
4		eceq1	$$⊢x=A\to \left[x\right]R=\left[A\right]R$$
5	4	eqeqan2d	$$⊢\left(z=y\wedge x=A\right)\to \left(z=\left[x\right]R\leftrightarrow y=\left[A\right]R\right)$$
6	5	ancoms	$$⊢\left(x=A\wedge z=y\right)\to \left(z=\left[x\right]R\leftrightarrow y=\left[A\right]R\right)$$
7	3 6	anbi12d	$$⊢\left(x=A\wedge z=y\right)\to \left(\left(x\in \mathrm{dom}R\wedge z=\left[x\right]R\right)\leftrightarrow \left(A\in \mathrm{dom}R\wedge y=\left[A\right]R\right)\right)$$
8		dfqmap3	Could not format QMap R = { <. x , z >. | ( x e. dom R /\ z = [ x ] R ) } : No typesetting found for |- QMap R = { <. x , z >. | ( x e. dom R /\ z = [ x ] R ) } with typecode |-
9	7 8	brabga	Could not format ( ( A e. dom R /\ y e. _V ) -> ( A QMap R y <-> ( A e. dom R /\ y = [ A ] R ) ) ) : No typesetting found for |- ( ( A e. dom R /\ y e. _V ) -> ( A QMap R y <-> ( A e. dom R /\ y = [ A ] R ) ) ) with typecode |-
10	9	elvd	Could not format ( A e. dom R -> ( A QMap R y <-> ( A e. dom R /\ y = [ A ] R ) ) ) : No typesetting found for |- ( A e. dom R -> ( A QMap R y <-> ( A e. dom R /\ y = [ A ] R ) ) ) with typecode |-
11	10	abbidv	Could not format ( A e. dom R -> { y | A QMap R y } = { y | ( A e. dom R /\ y = [ A ] R ) } ) : No typesetting found for |- ( A e. dom R -> { y | A QMap R y } = { y | ( A e. dom R /\ y = [ A ] R ) } ) with typecode |-
12		inab	$$⊢\left\{y|A\in \mathrm{dom}R\right\}\cap \left\{y|y=\left[A\right]R\right\}=\left\{y|\left(A\in \mathrm{dom}R\wedge y=\left[A\right]R\right)\right\}$$
13	11 12	eqtr4di	Could not format ( A e. dom R -> { y | A QMap R y } = ( { y | A e. dom R } i^i { y | y = [ A ] R } ) ) : No typesetting found for |- ( A e. dom R -> { y | A QMap R y } = ( { y | A e. dom R } i^i { y | y = [ A ] R } ) ) with typecode |-
14		ax-5	$$⊢A\in \mathrm{dom}R\to \forall yA\in \mathrm{dom}R$$
15		abv	$$⊢\left\{y|A\in \mathrm{dom}R\right\}=\mathrm{V}\leftrightarrow \forall yA\in \mathrm{dom}R$$
16	14 15	sylibr	$$⊢A\in \mathrm{dom}R\to \left\{y|A\in \mathrm{dom}R\right\}=\mathrm{V}$$
17	16	ineq1d	$$⊢A\in \mathrm{dom}R\to \left\{y|A\in \mathrm{dom}R\right\}\cap \left\{y|y=\left[A\right]R\right\}=\mathrm{V}\cap \left\{y|y=\left[A\right]R\right\}$$
18		inv1	$$⊢\left\{y|y=\left[A\right]R\right\}\cap \mathrm{V}=\left\{y|y=\left[A\right]R\right\}$$
19	18	ineqcomi	$$⊢\mathrm{V}\cap \left\{y|y=\left[A\right]R\right\}=\left\{y|y=\left[A\right]R\right\}$$
20	17 19	eqtrdi	$$⊢A\in \mathrm{dom}R\to \left\{y|A\in \mathrm{dom}R\right\}\cap \left\{y|y=\left[A\right]R\right\}=\left\{y|y=\left[A\right]R\right\}$$
21	13 20	eqtrd	Could not format ( A e. dom R -> { y | A QMap R y } = { y | y = [ A ] R } ) : No typesetting found for |- ( A e. dom R -> { y | A QMap R y } = { y | y = [ A ] R } ) with typecode |-
22		df-sn	$$⊢\left\{\left[A\right]R\right\}=\left\{y|y=\left[A\right]R\right\}$$
23	21 22	eqtr4di	Could not format ( A e. dom R -> { y | A QMap R y } = { [ A ] R } ) : No typesetting found for |- ( A e. dom R -> { y | A QMap R y } = { [ A ] R } ) with typecode |-
24	1 23	eqtrd	Could not format ( A e. dom R -> [ A ] QMap R = { [ A ] R } ) : No typesetting found for |- ( A e. dom R -> [ A ] QMap R = { [ A ] R } ) with typecode |-