oppfvallem

		Ref	Expression
	Assertion	oppfvallem	$⊢ F (C Func D) G \to (Rel G \land Rel dom G)$

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

Metamath Proof Explorer