This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )