Metamath Proof Explorer

Theorem reldmran2

Description: The domain of ( P Ran E ) is a relation. (Contributed by Zhi Wang, 4-Nov-2025)

Ref Expression
Assertion reldmran2 
|- Rel dom ( P Ran E )

Proof

Step Hyp Ref Expression
1 rel0 
 |-  Rel (/)
2 df-ov 
 |-  ( P Ran E ) = ( Ran ` <. P , E >. )
3 id 
 |-  ( ( Ran ` <. P , E >. ) = (/) -> ( Ran ` <. P , E >. ) = (/) )
4 2 3 eqtrid 
 |-  ( ( Ran ` <. P , E >. ) = (/) -> ( P Ran E ) = (/) )
5 4 dmeqd 
 |-  ( ( Ran ` <. P , E >. ) = (/) -> dom ( P Ran E ) = dom (/) )
6 dm0 
 |-  dom (/) = (/)
7 5 6 eqtrdi 
 |-  ( ( Ran ` <. P , E >. ) = (/) -> dom ( P Ran E ) = (/) )
8 7 releqd 
 |-  ( ( Ran ` <. P , E >. ) = (/) -> ( Rel dom ( P Ran E ) <-> Rel (/) ) )
9 1 8 mpbiri 
 |-  ( ( Ran ` <. P , E >. ) = (/) -> Rel dom ( P Ran E ) )
10 eqid 
 |-  ( f e. ( ( 1st ` P ) Func ( 2nd ` P ) ) , x e. ( ( 1st ` P ) Func E ) |-> ( ( oppFunc ` ( <. ( 2nd ` P ) , E >. -o.F f ) ) ( ( oppCat ` ( ( 2nd ` P ) FuncCat E ) ) UP ( oppCat ` ( ( 1st ` P ) FuncCat E ) ) ) x ) ) = ( f e. ( ( 1st ` P ) Func ( 2nd ` P ) ) , x e. ( ( 1st ` P ) Func E ) |-> ( ( oppFunc ` ( <. ( 2nd ` P ) , E >. -o.F f ) ) ( ( oppCat ` ( ( 2nd ` P ) FuncCat E ) ) UP ( oppCat ` ( ( 1st ` P ) FuncCat E ) ) ) x ) )
11 10 reldmmpo 
 |-  Rel dom ( f e. ( ( 1st ` P ) Func ( 2nd ` P ) ) , x e. ( ( 1st ` P ) Func E ) |-> ( ( oppFunc ` ( <. ( 2nd ` P ) , E >. -o.F f ) ) ( ( oppCat ` ( ( 2nd ` P ) FuncCat E ) ) UP ( oppCat ` ( ( 1st ` P ) FuncCat E ) ) ) x ) )
12 fvfundmfvn0 
 |-  ( ( Ran ` <. P , E >. ) =/= (/) -> ( <. P , E >. e. dom Ran /\ Fun ( Ran |` { <. P , E >. } ) ) )
13 12 simpld 
 |-  ( ( Ran ` <. P , E >. ) =/= (/) -> <. P , E >. e. dom Ran )
14 ranfn 
 |-  Ran Fn ( ( _V X. _V ) X. _V )
15 14 fndmi 
 |-  dom Ran = ( ( _V X. _V ) X. _V )
16 13 15 eleqtrdi 
 |-  ( ( Ran ` <. P , E >. ) =/= (/) -> <. P , E >. e. ( ( _V X. _V ) X. _V ) )
17 opelxp1 
 |-  ( <. P , E >. e. ( ( _V X. _V ) X. _V ) -> P e. ( _V X. _V ) )
18 1st2nd2 
 |-  ( P e. ( _V X. _V ) -> P = <. ( 1st ` P ) , ( 2nd ` P ) >. )
19 16 17 18 3syl 
 |-  ( ( Ran ` <. P , E >. ) =/= (/) -> P = <. ( 1st ` P ) , ( 2nd ` P ) >. )
20 19 oveq1d 
 |-  ( ( Ran ` <. P , E >. ) =/= (/) -> ( P Ran E ) = ( <. ( 1st ` P ) , ( 2nd ` P ) >. Ran E ) )
21 eqid 
 |-  ( ( 2nd ` P ) FuncCat E ) = ( ( 2nd ` P ) FuncCat E )
22 eqid 
 |-  ( ( 1st ` P ) FuncCat E ) = ( ( 1st ` P ) FuncCat E )
23 fvexd 
 |-  ( ( Ran ` <. P , E >. ) =/= (/) -> ( 1st ` P ) e. _V )
24 fvexd 
 |-  ( ( Ran ` <. P , E >. ) =/= (/) -> ( 2nd ` P ) e. _V )
25 opelxp2 
 |-  ( <. P , E >. e. ( ( _V X. _V ) X. _V ) -> E e. _V )
26 16 25 syl 
 |-  ( ( Ran ` <. P , E >. ) =/= (/) -> E e. _V )
27 eqid 
 |-  ( oppCat ` ( ( 2nd ` P ) FuncCat E ) ) = ( oppCat ` ( ( 2nd ` P ) FuncCat E ) )
28 eqid 
 |-  ( oppCat ` ( ( 1st ` P ) FuncCat E ) ) = ( oppCat ` ( ( 1st ` P ) FuncCat E ) )
29 21 22 23 24 26 27 28 ranfval 
 |-  ( ( Ran ` <. P , E >. ) =/= (/) -> ( <. ( 1st ` P ) , ( 2nd ` P ) >. Ran E ) = ( f e. ( ( 1st ` P ) Func ( 2nd ` P ) ) , x e. ( ( 1st ` P ) Func E ) |-> ( ( oppFunc ` ( <. ( 2nd ` P ) , E >. -o.F f ) ) ( ( oppCat ` ( ( 2nd ` P ) FuncCat E ) ) UP ( oppCat ` ( ( 1st ` P ) FuncCat E ) ) ) x ) ) )
30 20 29 eqtrd 
 |-  ( ( Ran ` <. P , E >. ) =/= (/) -> ( P Ran E ) = ( f e. ( ( 1st ` P ) Func ( 2nd ` P ) ) , x e. ( ( 1st ` P ) Func E ) |-> ( ( oppFunc ` ( <. ( 2nd ` P ) , E >. -o.F f ) ) ( ( oppCat ` ( ( 2nd ` P ) FuncCat E ) ) UP ( oppCat ` ( ( 1st ` P ) FuncCat E ) ) ) x ) ) )
31 30 dmeqd 
 |-  ( ( Ran ` <. P , E >. ) =/= (/) -> dom ( P Ran E ) = dom ( f e. ( ( 1st ` P ) Func ( 2nd ` P ) ) , x e. ( ( 1st ` P ) Func E ) |-> ( ( oppFunc ` ( <. ( 2nd ` P ) , E >. -o.F f ) ) ( ( oppCat ` ( ( 2nd ` P ) FuncCat E ) ) UP ( oppCat ` ( ( 1st ` P ) FuncCat E ) ) ) x ) ) )
32 31 releqd 
 |-  ( ( Ran ` <. P , E >. ) =/= (/) -> ( Rel dom ( P Ran E ) <-> Rel dom ( f e. ( ( 1st ` P ) Func ( 2nd ` P ) ) , x e. ( ( 1st ` P ) Func E ) |-> ( ( oppFunc ` ( <. ( 2nd ` P ) , E >. -o.F f ) ) ( ( oppCat ` ( ( 2nd ` P ) FuncCat E ) ) UP ( oppCat ` ( ( 1st ` P ) FuncCat E ) ) ) x ) ) ) )
33 11 32 mpbiri 
 |-  ( ( Ran ` <. P , E >. ) =/= (/) -> Rel dom ( P Ran E ) )
34 9 33 pm2.61ine 
 |-  Rel dom ( P Ran E )