Theorem reldmlan2

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

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

Proof

Step	Hyp	Ref	Expression
1		rel0	$$⊢\mathrm{Rel}\varnothing$$
2		df-ov	Could not format ( P Lan E ) = ( Lan ` <. P , E >. ) : No typesetting found for |- ( P Lan E ) = ( Lan ` <. P , E >. ) with typecode |-
3		id	Could not format ( ( Lan ` <. P , E >. ) = (/) -> ( Lan ` <. P , E >. ) = (/) ) : No typesetting found for |- ( ( Lan ` <. P , E >. ) = (/) -> ( Lan ` <. P , E >. ) = (/) ) with typecode |-
4	2 3	eqtrid	Could not format ( ( Lan ` <. P , E >. ) = (/) -> ( P Lan E ) = (/) ) : No typesetting found for |- ( ( Lan ` <. P , E >. ) = (/) -> ( P Lan E ) = (/) ) with typecode |-
5	4	dmeqd	Could not format ( ( Lan ` <. P , E >. ) = (/) -> dom ( P Lan E ) = dom (/) ) : No typesetting found for |- ( ( Lan ` <. P , E >. ) = (/) -> dom ( P Lan E ) = dom (/) ) with typecode |-
6		dm0	$$⊢\mathrm{dom}\varnothing =\varnothing$$
7	5 6	eqtrdi	Could not format ( ( Lan ` <. P , E >. ) = (/) -> dom ( P Lan E ) = (/) ) : No typesetting found for |- ( ( Lan ` <. P , E >. ) = (/) -> dom ( P Lan E ) = (/) ) with typecode |-
8	7	releqd	Could not format ( ( Lan ` <. P , E >. ) = (/) -> ( Rel dom ( P Lan E ) <-> Rel (/) ) ) : No typesetting found for |- ( ( Lan ` <. P , E >. ) = (/) -> ( Rel dom ( P Lan E ) <-> Rel (/) ) ) with typecode |-
9	1 8	mpbiri	Could not format ( ( Lan ` <. P , E >. ) = (/) -> Rel dom ( P Lan E ) ) : No typesetting found for |- ( ( Lan ` <. P , E >. ) = (/) -> Rel dom ( P Lan E ) ) with typecode |-
10		eqid	Could not format ( 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 ) ) : No typesetting found for |- ( 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 ) ) with typecode |-
11	10	reldmmpo	Could not format 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 ) ) : No typesetting found for |- 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 ) ) with typecode |-
12		fvfundmfvn0	Could not format ( ( Lan ` <. P , E >. ) =/= (/) -> ( <. P , E >. e. dom Lan /\ Fun ( Lan |` { <. P , E >. } ) ) ) : No typesetting found for |- ( ( Lan ` <. P , E >. ) =/= (/) -> ( <. P , E >. e. dom Lan /\ Fun ( Lan |` { <. P , E >. } ) ) ) with typecode |-
13	12	simpld	Could not format ( ( Lan ` <. P , E >. ) =/= (/) -> <. P , E >. e. dom Lan ) : No typesetting found for |- ( ( Lan ` <. P , E >. ) =/= (/) -> <. P , E >. e. dom Lan ) with typecode |-
14		lanfn	Could not format Lan Fn ( ( _V X. _V ) X. _V ) : No typesetting found for |- Lan Fn ( ( _V X. _V ) X. _V ) with typecode |-
15	14	fndmi	Could not format dom Lan = ( ( _V X. _V ) X. _V ) : No typesetting found for |- dom Lan = ( ( _V X. _V ) X. _V ) with typecode |-
16	13 15	eleqtrdi	Could not format ( ( Lan ` <. P , E >. ) =/= (/) -> <. P , E >. e. ( ( _V X. _V ) X. _V ) ) : No typesetting found for |- ( ( Lan ` <. 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 ( ( Lan ` <. P , E >. ) =/= (/) -> P = <. ( 1st ` P ) , ( 2nd ` P ) >. ) : No typesetting found for |- ( ( Lan ` <. P , E >. ) =/= (/) -> P = <. ( 1st ` P ) , ( 2nd ` P ) >. ) with typecode |-
20	19	oveq1d	Could not format ( ( Lan ` <. P , E >. ) =/= (/) -> ( P Lan E ) = ( <. ( 1st ` P ) , ( 2nd ` P ) >. Lan E ) ) : No typesetting found for |- ( ( Lan ` <. P , E >. ) =/= (/) -> ( P Lan E ) = ( <. ( 1st ` P ) , ( 2nd ` P ) >. Lan 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 ( ( Lan ` <. P , E >. ) =/= (/) -> ( 1st ` P ) e. _V ) : No typesetting found for |- ( ( Lan ` <. P , E >. ) =/= (/) -> ( 1st ` P ) e. _V ) with typecode |-
24		fvexd	Could not format ( ( Lan ` <. P , E >. ) =/= (/) -> ( 2nd ` P ) e. _V ) : No typesetting found for |- ( ( Lan ` <. 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 ( ( Lan ` <. P , E >. ) =/= (/) -> E e. _V ) : No typesetting found for |- ( ( Lan ` <. P , E >. ) =/= (/) -> E e. _V ) with typecode |-
27	21 22 23 24 26	lanfval	Could not format ( ( 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 ) ) ) : No typesetting found for |- ( ( 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 ) ) ) with typecode |-
28	20 27	eqtrd	Could not format ( ( 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 ) ) ) : No typesetting found for |- ( ( 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 ) ) ) with typecode |-
29	28	dmeqd	Could not format ( ( 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 ) ) ) : No typesetting found for |- ( ( 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 ) ) ) with typecode |-
30	29	releqd	Could not format ( ( 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 ) ) ) ) : No typesetting found for |- ( ( 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 ) ) ) ) with typecode |-
31	11 30	mpbiri	Could not format ( ( Lan ` <. P , E >. ) =/= (/) -> Rel dom ( P Lan E ) ) : No typesetting found for |- ( ( Lan ` <. P , E >. ) =/= (/) -> Rel dom ( P Lan E ) ) with typecode |-
32	9 31	pm2.61ine	Could not format Rel dom ( P Lan E ) : No typesetting found for |- Rel dom ( P Lan E ) with typecode |-