Metamath Proof Explorer

Theorem reldmlan2

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

Ref Expression
Assertion reldmlan2 
|- Rel dom ( P Lan E )

Proof

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