Metamath Proof Explorer

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 
|- ( A e. dom R -> [ A ] QMap R = { [ A ] R } )

Proof

Step Hyp Ref Expression
1 dfec2 
 |-  ( A e. dom R -> [ A ] QMap R = { y | A QMap R y } )
2 eleq1 
 |-  ( x = A -> ( x e. dom R <-> A e. dom R ) )
3 2 adantr 
 |-  ( ( x = A /\ z = y ) -> ( x e. dom R <-> A e. dom R ) )
4 eceq1 
 |-  ( x = A -> [ x ] R = [ A ] R )
5 4 eqeqan2d 
 |-  ( ( z = y /\ x = A ) -> ( z = [ x ] R <-> y = [ A ] R ) )
6 5 ancoms 
 |-  ( ( x = A /\ z = y ) -> ( z = [ x ] R <-> y = [ A ] R ) )
7 3 6 anbi12d 
 |-  ( ( x = A /\ z = y ) -> ( ( x e. dom R /\ z = [ x ] R ) <-> ( A e. dom R /\ y = [ A ] R ) ) )
8 dfqmap3 
 |-  QMap R = { <. x , z >. | ( x e. dom R /\ z = [ x ] R ) }
9 7 8 brabga 
 |-  ( ( A e. dom R /\ y e. _V ) -> ( A QMap R y <-> ( A e. dom R /\ y = [ A ] R ) ) )
10 9 elvd 
 |-  ( A e. dom R -> ( A QMap R y <-> ( A e. dom R /\ y = [ A ] R ) ) )
11 10 abbidv 
 |-  ( A e. dom R -> { y | A QMap R y } = { y | ( A e. dom R /\ y = [ A ] R ) } )
12 inab 
 |-  ( { y | A e. dom R } i^i { y | y = [ A ] R } ) = { y | ( A e. dom R /\ y = [ A ] R ) }
13 11 12 eqtr4di 
 |-  ( A e. dom R -> { y | A QMap R y } = ( { y | A e. dom R } i^i { y | y = [ A ] R } ) )
14 ax-5 
 |-  ( A e. dom R -> A. y A e. dom R )
15 abv 
 |-  ( { y | A e. dom R } = _V <-> A. y A e. dom R )
16 14 15 sylibr 
 |-  ( A e. dom R -> { y | A e. dom R } = _V )
17 16 ineq1d 
 |-  ( A e. dom R -> ( { y | A e. dom R } i^i { y | y = [ A ] R } ) = ( _V i^i { y | y = [ A ] R } ) )
18 inv1 
 |-  ( { y | y = [ A ] R } i^i _V ) = { y | y = [ A ] R }
19 18 ineqcomi 
 |-  ( _V i^i { y | y = [ A ] R } ) = { y | y = [ A ] R }
20 17 19 eqtrdi 
 |-  ( A e. dom R -> ( { y | A e. dom R } i^i { y | y = [ A ] R } ) = { y | y = [ A ] R } )
21 13 20 eqtrd 
 |-  ( A e. dom R -> { y | A QMap R y } = { y | y = [ A ] R } )
22 df-sn 
 |-  { [ A ] R } = { y | y = [ A ] R }
23 21 22 eqtr4di 
 |-  ( A e. dom R -> { y | A QMap R y } = { [ A ] R } )
24 1 23 eqtrd 
 |-  ( A e. dom R -> [ A ] QMap R = { [ A ] R } )