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 (x \in dom R \leftrightarrow A \in dom R)$
3	2	adantr	$⊢ (x = A \land z = y) \to (x \in dom R \leftrightarrow A \in dom R)$
4		eceq1	$⊢ x = A \to [x] R = [A] R$
5	4	eqeqan2d	$⊢ (z = y \land x = A) \to (z = [x] R \leftrightarrow y = [A] R)$
6	5	ancoms	$⊢ (x = A \land z = y) \to (z = [x] R \leftrightarrow y = [A] R)$
7	3 6	anbi12d	$⊢ (x = A \land z = y) \to ((x \in dom R \land z = [x] R) \leftrightarrow (A \in dom R \land y = [A] R))$
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	$⊢ \{y \| A \in dom R\} \cap \{y \| y = [A] R\} = \{y \| (A \in dom R \land y = [A] R)\}$
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 dom R \to \forall y A \in dom R$
15		abv	$⊢ \{y \| A \in dom R\} = V \leftrightarrow \forall y A \in dom R$
16	14 15	sylibr	$⊢ A \in dom R \to \{y \| A \in dom R\} = V$
17	16	ineq1d	$⊢ A \in dom R \to \{y \| A \in dom R\} \cap \{y \| y = [A] R\} = V \cap \{y \| y = [A] R\}$
18		inv1	$⊢ \{y \| y = [A] R\} \cap V = \{y \| y = [A] R\}$
19	18	ineqcomi	$⊢ V \cap \{y \| y = [A] R\} = \{y \| y = [A] R\}$
20	17 19	eqtrdi	$⊢ A \in dom R \to \{y \| A \in dom R\} \cap \{y \| y = [A] R\} = \{y \| y = [A] R\}$
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	$⊢ \{[A] R\} = \{y \| y = [A] R\}$
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 \|-

Metamath Proof Explorer

Theorem ecqmap

Proof