Theorem reldmran2

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

	Ref	Expression
Assertion	reldmran2	Could not format assertion : No typesetting found for |- Rel dom ( P Ran E ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		rel0	$$⊢\mathrm{Rel}\varnothing$$
2		df-ov	Could not format ( P Ran E ) = ( Ran ` <. P , E >. ) : No typesetting found for |- ( P Ran E ) = ( Ran ` <. P , E >. ) with typecode |-
3		id	Could not format ( ( Ran ` <. P , E >. ) = (/) -> ( Ran ` <. P , E >. ) = (/) ) : No typesetting found for |- ( ( Ran ` <. P , E >. ) = (/) -> ( Ran ` <. P , E >. ) = (/) ) with typecode |-
4	2 3	eqtrid	Could not format ( ( Ran ` <. P , E >. ) = (/) -> ( P Ran E ) = (/) ) : No typesetting found for |- ( ( Ran ` <. P , E >. ) = (/) -> ( P Ran E ) = (/) ) with typecode |-
5	4	dmeqd	Could not format ( ( Ran ` <. P , E >. ) = (/) -> dom ( P Ran E ) = dom (/) ) : No typesetting found for |- ( ( Ran ` <. P , E >. ) = (/) -> dom ( P Ran E ) = dom (/) ) with typecode |-
6		dm0	$$⊢\mathrm{dom}\varnothing =\varnothing$$
7	5 6	eqtrdi	Could not format ( ( Ran ` <. P , E >. ) = (/) -> dom ( P Ran E ) = (/) ) : No typesetting found for |- ( ( Ran ` <. P , E >. ) = (/) -> dom ( P Ran E ) = (/) ) with typecode |-
8	7	releqd	Could not format ( ( Ran ` <. P , E >. ) = (/) -> ( Rel dom ( P Ran E ) <-> Rel (/) ) ) : No typesetting found for |- ( ( Ran ` <. P , E >. ) = (/) -> ( Rel dom ( P Ran E ) <-> Rel (/) ) ) with typecode |-
9	1 8	mpbiri	Could not format ( ( Ran ` <. P , E >. ) = (/) -> Rel dom ( P Ran E ) ) : No typesetting found for |- ( ( Ran ` <. P , E >. ) = (/) -> Rel dom ( P Ran E ) ) with typecode |-
10		eqid	Could not format ( 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 ) ) : No typesetting found for |- ( 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 ) ) with typecode |-
11	10	reldmmpo	Could not format 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 ) ) : No typesetting found for |- 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 ) ) with typecode |-
12		fvfundmfvn0	Could not format ( ( Ran ` <. P , E >. ) =/= (/) -> ( <. P , E >. e. dom Ran /\ Fun ( Ran |` { <. P , E >. } ) ) ) : No typesetting found for |- ( ( Ran ` <. P , E >. ) =/= (/) -> ( <. P , E >. e. dom Ran /\ Fun ( Ran |` { <. P , E >. } ) ) ) with typecode |-
13	12	simpld	Could not format ( ( Ran ` <. P , E >. ) =/= (/) -> <. P , E >. e. dom Ran ) : No typesetting found for |- ( ( Ran ` <. P , E >. ) =/= (/) -> <. P , E >. e. dom Ran ) with typecode |-
14		ranfn	Could not format Ran Fn ( ( _V X. _V ) X. _V ) : No typesetting found for |- Ran Fn ( ( _V X. _V ) X. _V ) with typecode |-
15	14	fndmi	Could not format dom Ran = ( ( _V X. _V ) X. _V ) : No typesetting found for |- dom Ran = ( ( _V X. _V ) X. _V ) with typecode |-
16	13 15	eleqtrdi	Could not format ( ( Ran ` <. P , E >. ) =/= (/) -> <. P , E >. e. ( ( _V X. _V ) X. _V ) ) : No typesetting found for |- ( ( Ran ` <. P , E >. ) =/= (/) -> <. P , E >. e. ( ( _V X. _V ) X. _V ) ) with typecode |-
17		opelxp1	$$⊢⟨P,E⟩\in \left(\left(\mathrm{V}\times \mathrm{V}\right)\times \mathrm{V}\right)\to P\in \left(\mathrm{V}\times \mathrm{V}\right)$$
18		1st2nd2	$$⊢P\in \left(\mathrm{V}\times \mathrm{V}\right)\to P=⟨1^{st}\left(P\right),2^{nd}\left(P\right)⟩$$
19	16 17 18	3syl	Could not format ( ( Ran ` <. P , E >. ) =/= (/) -> P = <. ( 1st ` P ) , ( 2nd ` P ) >. ) : No typesetting found for |- ( ( Ran ` <. P , E >. ) =/= (/) -> P = <. ( 1st ` P ) , ( 2nd ` P ) >. ) with typecode |-
20	19	oveq1d	Could not format ( ( Ran ` <. P , E >. ) =/= (/) -> ( P Ran E ) = ( <. ( 1st ` P ) , ( 2nd ` P ) >. Ran E ) ) : No typesetting found for |- ( ( Ran ` <. P , E >. ) =/= (/) -> ( P Ran E ) = ( <. ( 1st ` P ) , ( 2nd ` P ) >. Ran E ) ) with typecode |-
21		eqid	$$⊢2^{nd}\left(P\right)\mathrm{FuncCat}E=2^{nd}\left(P\right)\mathrm{FuncCat}E$$
22		eqid	$$⊢1^{st}\left(P\right)\mathrm{FuncCat}E=1^{st}\left(P\right)\mathrm{FuncCat}E$$
23		fvexd	Could not format ( ( Ran ` <. P , E >. ) =/= (/) -> ( 1st ` P ) e. _V ) : No typesetting found for |- ( ( Ran ` <. P , E >. ) =/= (/) -> ( 1st ` P ) e. _V ) with typecode |-
24		fvexd	Could not format ( ( Ran ` <. P , E >. ) =/= (/) -> ( 2nd ` P ) e. _V ) : No typesetting found for |- ( ( Ran ` <. P , E >. ) =/= (/) -> ( 2nd ` P ) e. _V ) with typecode |-
25		opelxp2	$$⊢⟨P,E⟩\in \left(\left(\mathrm{V}\times \mathrm{V}\right)\times \mathrm{V}\right)\to E\in \mathrm{V}$$
26	16 25	syl	Could not format ( ( Ran ` <. P , E >. ) =/= (/) -> E e. _V ) : No typesetting found for |- ( ( Ran ` <. P , E >. ) =/= (/) -> E e. _V ) with typecode |-
27		eqid	$$⊢\mathrm{oppCat}\left(2^{nd}\left(P\right)\mathrm{FuncCat}E\right)=\mathrm{oppCat}\left(2^{nd}\left(P\right)\mathrm{FuncCat}E\right)$$
28		eqid	$$⊢\mathrm{oppCat}\left(1^{st}\left(P\right)\mathrm{FuncCat}E\right)=\mathrm{oppCat}\left(1^{st}\left(P\right)\mathrm{FuncCat}E\right)$$
29	21 22 23 24 26 27 28	ranfval	Could not format ( ( 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 ) ) ) : No typesetting found for |- ( ( 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 ) ) ) with typecode |-
30	20 29	eqtrd	Could not format ( ( 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 ) ) ) : No typesetting found for |- ( ( 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 ) ) ) with typecode |-
31	30	dmeqd	Could not format ( ( 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 ) ) ) : No typesetting found for |- ( ( 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 ) ) ) with typecode |-
32	31	releqd	Could not format ( ( 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 ) ) ) ) : No typesetting found for |- ( ( 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 ) ) ) ) with typecode |-
33	11 32	mpbiri	Could not format ( ( Ran ` <. P , E >. ) =/= (/) -> Rel dom ( P Ran E ) ) : No typesetting found for |- ( ( Ran ` <. P , E >. ) =/= (/) -> Rel dom ( P Ran E ) ) with typecode |-
34	9 33	pm2.61ine	Could not format Rel dom ( P Ran E ) : No typesetting found for |- Rel dom ( P Ran E ) with typecode |-