This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem disjqmap2

Description: Disjointness of QMap equals E* -generation. Pairs with disjqmap and raldmqseu to move between E* and E! depending on context. (Contributed by Peter Mazsa, 12-Feb-2026)

Ref Expression
Assertion disjqmap2 
|- ( R e. V -> ( Disj QMap R <-> A. u E* t e. dom R u = [ t ] R ) )

Proof

Step Hyp Ref Expression
1 relqmap 
 |-  Rel QMap R
2 dfdisjALTV 
 |-  ( Disj QMap R <-> ( FunALTV `' QMap R /\ Rel QMap R ) )
3 1 2 mpbiran2 
 |-  ( Disj QMap R <-> FunALTV `' QMap R )
4 funALTVfun 
 |-  ( FunALTV `' QMap R <-> Fun `' QMap R )
5 3 4 bitri 
 |-  ( Disj QMap R <-> Fun `' QMap R )
6 nfv 
 |-  F/ t R e. V
7 nfcv 
 |-  F/_ t dom R
8 nfcv 
 |-  F/_ t QMap R
9 df-qmap 
 |-  QMap R = ( t e. dom R |-> [ t ] R )
10 resexg 
 |-  ( R e. V -> ( R |` dom R ) e. _V )
11 elecex 
 |-  ( ( R |` dom R ) e. _V -> ( t e. dom R -> [ t ] R e. _V ) )
12 10 11 syl 
 |-  ( R e. V -> ( t e. dom R -> [ t ] R e. _V ) )
13 12 imp 
 |-  ( ( R e. V /\ t e. dom R ) -> [ t ] R e. _V )
14 6 7 8 9 13 funcnvmpt 
 |-  ( R e. V -> ( Fun `' QMap R <-> A. u E* t e. dom R u = [ t ] R ) )
15 5 14 bitrid 
 |-  ( R e. V -> ( Disj QMap R <-> A. u E* t e. dom R u = [ t ] R ) )