Theorem oppfvallem

Description: Lemma for oppfval . (Contributed by Zhi Wang, 13-Nov-2025)

	Ref	Expression
Assertion	oppfvallem	$$⊢F\left(C\mathrm{Func}D\right)G\to \left(\mathrm{Rel}G\wedge \mathrm{Rel}\mathrm{dom}G\right)$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
2		id	$$⊢F\left(C\mathrm{Func}D\right)G\to F\left(C\mathrm{Func}D\right)G$$
3	1 2	funcfn2	$$⊢F\left(C\mathrm{Func}D\right)G\to GFn\left({\mathrm{Base}}_C\times {\mathrm{Base}}_C\right)$$
4		fnrel	$$⊢GFn\left({\mathrm{Base}}_C\times {\mathrm{Base}}_C\right)\to \mathrm{Rel}G$$
5	3 4	syl	$$⊢F\left(C\mathrm{Func}D\right)G\to \mathrm{Rel}G$$
6		relxp	$$⊢\mathrm{Rel}\left({\mathrm{Base}}_C\times {\mathrm{Base}}_C\right)$$
7	3	fndmd	$$⊢F\left(C\mathrm{Func}D\right)G\to \mathrm{dom}G={\mathrm{Base}}_C\times {\mathrm{Base}}_C$$
8	7	releqd	$$⊢F\left(C\mathrm{Func}D\right)G\to \left(\mathrm{Rel}\mathrm{dom}G\leftrightarrow \mathrm{Rel}\left({\mathrm{Base}}_C\times {\mathrm{Base}}_C\right)\right)$$
9	6 8	mpbiri	$$⊢F\left(C\mathrm{Func}D\right)G\to \mathrm{Rel}\mathrm{dom}G$$
10	5 9	jca	$$⊢F\left(C\mathrm{Func}D\right)G\to \left(\mathrm{Rel}G\wedge \mathrm{Rel}\mathrm{dom}G\right)$$