Theorem oppfvallem

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

	Ref	Expression
Assertion	oppfvallem	⊢ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 → ( Rel 𝐺 ∧ Rel dom 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
2		id	⊢ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
3	1 2	funcfn2	⊢ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 → 𝐺 Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) )
4		fnrel	⊢ ( 𝐺 Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) → Rel 𝐺 )
5	3 4	syl	⊢ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 → Rel 𝐺 )
6		relxp	⊢ Rel ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) )
7	3	fndmd	⊢ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 → dom 𝐺 = ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) )
8	7	releqd	⊢ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 → ( Rel dom 𝐺 ↔ Rel ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ) )
9	6 8	mpbiri	⊢ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 → Rel dom 𝐺 )
10	5 9	jca	⊢ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 → ( Rel 𝐺 ∧ Rel dom 𝐺 ) )