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 ( 𝐹 ( 𝐶 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 𝐺 ) )