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	No typesetting found for |- ( F oppFunc G ) = K with typecode |-
	eloppf2.x	$$⊢\phi \to X\in K$$
Assertion	eloppf2	$$⊢\phi \to \left(\left(F\in \mathrm{V}\wedge G\in \mathrm{V}\right)\wedge \left(\mathrm{Rel}G\wedge \mathrm{Rel}\mathrm{dom}G\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		eloppf2.k	Could not format ( F oppFunc G ) = K : No typesetting found for |- ( F oppFunc G ) = K with typecode |-
2		eloppf2.x	$$⊢\phi \to X\in K$$
3	2 1	eleqtrrdi	Could not format ( ph -> X e. ( F oppFunc G ) ) : No typesetting found for |- ( ph -> X e. ( F oppFunc G ) ) with typecode |-
4		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 |-
5	4	elmpocl	Could not format ( X e. ( F oppFunc G ) -> ( F e. _V /\ G e. _V ) ) : No typesetting found for |- ( X e. ( F oppFunc G ) -> ( F e. _V /\ G e. _V ) ) with typecode |-
6	3 5	syl	$$⊢\phi \to \left(F\in \mathrm{V}\wedge G\in \mathrm{V}\right)$$
7		oppfvalg	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 |-
8	6 7	syl	Could not format ( ph -> ( F oppFunc G ) = if ( ( Rel G /\ Rel dom G ) , <. F , tpos G >. , (/) ) ) : No typesetting found for |- ( ph -> ( F oppFunc G ) = if ( ( Rel G /\ Rel dom G ) , <. F , tpos G >. , (/) ) ) with typecode |-
9	3 8	eleqtrd	$$⊢\phi \to X\in if\left(\left(\mathrm{Rel}G\wedge \mathrm{Rel}\mathrm{dom}G\right),⟨F,tposG⟩,\varnothing \right)$$
10	9	ne0d	$$⊢\phi \to if\left(\left(\mathrm{Rel}G\wedge \mathrm{Rel}\mathrm{dom}G\right),⟨F,tposG⟩,\varnothing \right)\ne \varnothing$$
11		iffalse	$$⊢\neg \left(\mathrm{Rel}G\wedge \mathrm{Rel}\mathrm{dom}G\right)\to if\left(\left(\mathrm{Rel}G\wedge \mathrm{Rel}\mathrm{dom}G\right),⟨F,tposG⟩,\varnothing \right)=\varnothing$$
12	11	necon1ai	$$⊢if\left(\left(\mathrm{Rel}G\wedge \mathrm{Rel}\mathrm{dom}G\right),⟨F,tposG⟩,\varnothing \right)\ne \varnothing \to \left(\mathrm{Rel}G\wedge \mathrm{Rel}\mathrm{dom}G\right)$$
13	10 12	syl	$$⊢\phi \to \left(\mathrm{Rel}G\wedge \mathrm{Rel}\mathrm{dom}G\right)$$
14	6 13	jca	$$⊢\phi \to \left(\left(F\in \mathrm{V}\wedge G\in \mathrm{V}\right)\wedge \left(\mathrm{Rel}G\wedge \mathrm{Rel}\mathrm{dom}G\right)\right)$$