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

Metamath Proof Explorer

Theorem oppfvalg

Description: Value of the opposite functor. (Contributed by Zhi Wang, 13-Nov-2025)

Ref Expression
Assertion oppfvalg Could not format assertion : No typesetting found for |- ( ( F e. _V /\ G e. _V ) -> ( F oppFunc G ) = if ( ( Rel G /\ Rel dom G ) , <. F , tpos G >. , (/) ) ) with typecode |-

Proof

Step Hyp Ref Expression
1 simpr ⊢ f = F ∧ g = G → g = G
2 1 releqd ⊢ f = F ∧ g = G → Rel ⁡ g ↔ Rel ⁡ G
3 1 dmeqd ⊢ f = F ∧ g = G → dom ⁡ g = dom ⁡ G
4 3 releqd ⊢ f = F ∧ g = G → Rel ⁡ dom ⁡ g ↔ Rel ⁡ dom ⁡ G
5 2 4 anbi12d ⊢ f = F ∧ g = G → Rel ⁡ g ∧ Rel ⁡ dom ⁡ g ↔ Rel ⁡ G ∧ Rel ⁡ dom ⁡ G
6 simpl ⊢ f = F ∧ g = G → f = F
7 1 tposeqd ⊢ f = F ∧ g = G → tpos g = tpos G
8 6 7 opeq12d ⊢ f = F ∧ g = G → f tpos g = F tpos G
9 5 8 ifbieq1d ⊢ f = F ∧ g = G → if Rel ⁡ g ∧ Rel ⁡ dom ⁡ g f tpos g ∅ = if Rel ⁡ G ∧ Rel ⁡ dom ⁡ G F tpos G ∅
10 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 |-
11 opex ⊢ F tpos G ∈ V
12 0ex ⊢ ∅ ∈ V
13 11 12 ifex ⊢ if Rel ⁡ G ∧ Rel ⁡ dom ⁡ G F tpos G ∅ ∈ V
14 9 10 13 ovmpoa Could not format ( ( F e. _V /\ G e. _V ) -> ( F oppFunc G ) = if ( ( Rel G /\ Rel dom G ) , <. F , tpos G >. , (/) ) ) : No typesetting found for |- ( ( F e. _V /\ G e. _V ) -> ( F oppFunc G ) = if ( ( Rel G /\ Rel dom G ) , <. F , tpos G >. , (/) ) ) with typecode |-