Theorem eloppf2

Description: Both components of a pre-image of a non-empty opposite functor exist; and the second component is a relation on triples. (Contributed by Zhi Wang, 18-Nov-2025)

	Ref	Expression
Hypotheses	eloppf2.k	|- ( F oppFunc G ) = K
	eloppf2.x	|- ( ph -> X e. K )
Assertion	eloppf2	|- ( ph -> ( ( F e. _V /\ G e. _V ) /\ ( Rel G /\ Rel dom G ) ) )

Proof

Step	Hyp	Ref	Expression
1		eloppf2.k	|- ( F oppFunc G ) = K
2		eloppf2.x	|- ( ph -> X e. K )
3	2 1	eleqtrrdi	|- ( ph -> X e. ( F oppFunc G ) )
4		df-oppf	|- oppFunc = ( f e. _V , g e. _V |-> if ( ( Rel g /\ Rel dom g ) , <. f , tpos g >. , (/) ) )
5	4	elmpocl	|- ( X e. ( F oppFunc G ) -> ( F e. _V /\ G e. _V ) )
6	3 5	syl	|- ( ph -> ( F e. _V /\ G e. _V ) )
7		oppfvalg	|- ( ( F e. _V /\ G e. _V ) -> ( F oppFunc G ) = if ( ( Rel G /\ Rel dom G ) , <. F , tpos G >. , (/) ) )
8	6 7	syl	|- ( ph -> ( F oppFunc G ) = if ( ( Rel G /\ Rel dom G ) , <. F , tpos G >. , (/) ) )
9	3 8	eleqtrd	|- ( ph -> X e. if ( ( Rel G /\ Rel dom G ) , <. F , tpos G >. , (/) ) )
10	9	ne0d	|- ( ph -> if ( ( Rel G /\ Rel dom G ) , <. F , tpos G >. , (/) ) =/= (/) )
11		iffalse	|- ( -. ( Rel G /\ Rel dom G ) -> if ( ( Rel G /\ Rel dom G ) , <. F , tpos G >. , (/) ) = (/) )
12	11	necon1ai	|- ( if ( ( Rel G /\ Rel dom G ) , <. F , tpos G >. , (/) ) =/= (/) -> ( Rel G /\ Rel dom G ) )
13	10 12	syl	|- ( ph -> ( Rel G /\ Rel dom G ) )
14	6 13	jca	|- ( ph -> ( ( F e. _V /\ G e. _V ) /\ ( Rel G /\ Rel dom G ) ) )