Theorem oppfvallem

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

	Ref	Expression
Assertion	oppfvallem	|- ( F ( C Func D ) G -> ( Rel G /\ Rel dom G ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	|- ( Base ` C ) = ( Base ` C )
2		id	|- ( F ( C Func D ) G -> F ( C Func D ) G )
3	1 2	funcfn2	|- ( F ( C Func D ) G -> G Fn ( ( Base ` C ) X. ( Base ` C ) ) )
4		fnrel	|- ( G Fn ( ( Base ` C ) X. ( Base ` C ) ) -> Rel G )
5	3 4	syl	|- ( F ( C Func D ) G -> Rel G )
6		relxp	|- Rel ( ( Base ` C ) X. ( Base ` C ) )
7	3	fndmd	|- ( F ( C Func D ) G -> dom G = ( ( Base ` C ) X. ( Base ` C ) ) )
8	7	releqd	|- ( F ( C Func D ) G -> ( Rel dom G <-> Rel ( ( Base ` C ) X. ( Base ` C ) ) ) )
9	6 8	mpbiri	|- ( F ( C Func D ) G -> Rel dom G )
10	5 9	jca	|- ( F ( C Func D ) G -> ( Rel G /\ Rel dom G ) )