Theorem reldmoppf

Description: The domain of oppFunc is a relation. (Contributed by Zhi Wang, 13-Nov-2025)

	Ref	Expression
Assertion	reldmoppf	Could not format assertion : No typesetting found for |- Rel dom oppFunc with typecode |-

Proof

Step	Hyp	Ref	Expression
1		df-oppf	Could not format oppFunc = ( f e. _V , g e. _V |-> if ( ( Rel g /\ Rel dom g ) , <. f , tpos g >. , (/) ) ) : No typesetting found for |- oppFunc = ( f e. _V , g e. _V |-> if ( ( Rel g /\ Rel dom g ) , <. f , tpos g >. , (/) ) ) with typecode |-
2	1	reldmmpo	Could not format Rel dom oppFunc : No typesetting found for |- Rel dom oppFunc with typecode |-