Theorem eloppf

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

	Ref	Expression
Hypotheses	eloppf.g	No typesetting found for |- G = ( oppFunc ` F ) with typecode |-
	eloppf.x	$$⊢\phi \to X\in G$$
Assertion	eloppf	$$⊢\phi \to \left(F\ne \varnothing \wedge \left(\mathrm{Rel}{2}^{nd}\left(F\right)\wedge \mathrm{Rel}\mathrm{dom}{2}^{nd}\left(F\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		eloppf.g	Could not format G = ( oppFunc ` F ) : No typesetting found for |- G = ( oppFunc ` F ) with typecode |-
2		eloppf.x	$$⊢\phi \to X\in G$$
3	2 1	eleqtrdi	Could not format ( ph -> X e. ( oppFunc ` F ) ) : No typesetting found for |- ( ph -> X e. ( oppFunc ` F ) ) with typecode |-
4		elfvdm	Could not format ( X e. ( oppFunc ` F ) -> F e. dom oppFunc ) : No typesetting found for |- ( X e. ( oppFunc ` F ) -> F e. dom oppFunc ) with typecode |-
5		oppffn	Could not format oppFunc Fn ( _V X. _V ) : No typesetting found for |- oppFunc Fn ( _V X. _V ) with typecode |-
6	5	fndmi	Could not format dom oppFunc = ( _V X. _V ) : No typesetting found for |- dom oppFunc = ( _V X. _V ) with typecode |-
7	4 6	eleqtrdi	Could not format ( X e. ( oppFunc ` F ) -> F e. ( _V X. _V ) ) : No typesetting found for |- ( X e. ( oppFunc ` F ) -> F e. ( _V X. _V ) ) with typecode |-
8	3 7	syl	$$⊢\phi \to F\in \left(\mathrm{V}\times \mathrm{V}\right)$$
9		0nelxp	$$⊢\neg \varnothing \in \left(\mathrm{V}\times \mathrm{V}\right)$$
10		nelne2	$$⊢\left(F\in \left(\mathrm{V}\times \mathrm{V}\right)\wedge \neg \varnothing \in \left(\mathrm{V}\times \mathrm{V}\right)\right)\to F\ne \varnothing$$
11	8 9 10	sylancl	$$⊢\phi \to F\ne \varnothing$$
12		1st2nd2	$$⊢F\in \left(\mathrm{V}\times \mathrm{V}\right)\to F=⟨1^{st}\left(F\right),2^{nd}\left(F\right)⟩$$
13	3 7 12	3syl	$$⊢\phi \to F=⟨1^{st}\left(F\right),2^{nd}\left(F\right)⟩$$
14	13	fveq2d	Could not format ( ph -> ( oppFunc ` F ) = ( oppFunc ` <. ( 1st ` F ) , ( 2nd ` F ) >. ) ) : No typesetting found for |- ( ph -> ( oppFunc ` F ) = ( oppFunc ` <. ( 1st ` F ) , ( 2nd ` F ) >. ) ) with typecode |-
15		df-ov	Could not format ( ( 1st ` F ) oppFunc ( 2nd ` F ) ) = ( oppFunc ` <. ( 1st ` F ) , ( 2nd ` F ) >. ) : No typesetting found for |- ( ( 1st ` F ) oppFunc ( 2nd ` F ) ) = ( oppFunc ` <. ( 1st ` F ) , ( 2nd ` F ) >. ) with typecode |-
16		fvex	$$⊢1^{st}\left(F\right)\in \mathrm{V}$$
17		fvex	$$⊢2^{nd}\left(F\right)\in \mathrm{V}$$
18		oppfvalg	Could not format ( ( ( 1st ` F ) e. _V /\ ( 2nd ` F ) e. _V ) -> ( ( 1st ` F ) oppFunc ( 2nd ` F ) ) = if ( ( Rel ( 2nd ` F ) /\ Rel dom ( 2nd ` F ) ) , <. ( 1st ` F ) , tpos ( 2nd ` F ) >. , (/) ) ) : No typesetting found for |- ( ( ( 1st ` F ) e. _V /\ ( 2nd ` F ) e. _V ) -> ( ( 1st ` F ) oppFunc ( 2nd ` F ) ) = if ( ( Rel ( 2nd ` F ) /\ Rel dom ( 2nd ` F ) ) , <. ( 1st ` F ) , tpos ( 2nd ` F ) >. , (/) ) ) with typecode |-
19	16 17 18	mp2an	Could not format ( ( 1st ` F ) oppFunc ( 2nd ` F ) ) = if ( ( Rel ( 2nd ` F ) /\ Rel dom ( 2nd ` F ) ) , <. ( 1st ` F ) , tpos ( 2nd ` F ) >. , (/) ) : No typesetting found for |- ( ( 1st ` F ) oppFunc ( 2nd ` F ) ) = if ( ( Rel ( 2nd ` F ) /\ Rel dom ( 2nd ` F ) ) , <. ( 1st ` F ) , tpos ( 2nd ` F ) >. , (/) ) with typecode |-
20	15 19	eqtr3i	Could not format ( oppFunc ` <. ( 1st ` F ) , ( 2nd ` F ) >. ) = if ( ( Rel ( 2nd ` F ) /\ Rel dom ( 2nd ` F ) ) , <. ( 1st ` F ) , tpos ( 2nd ` F ) >. , (/) ) : No typesetting found for |- ( oppFunc ` <. ( 1st ` F ) , ( 2nd ` F ) >. ) = if ( ( Rel ( 2nd ` F ) /\ Rel dom ( 2nd ` F ) ) , <. ( 1st ` F ) , tpos ( 2nd ` F ) >. , (/) ) with typecode |-
21	14 20	eqtrdi	Could not format ( ph -> ( oppFunc ` F ) = if ( ( Rel ( 2nd ` F ) /\ Rel dom ( 2nd ` F ) ) , <. ( 1st ` F ) , tpos ( 2nd ` F ) >. , (/) ) ) : No typesetting found for |- ( ph -> ( oppFunc ` F ) = if ( ( Rel ( 2nd ` F ) /\ Rel dom ( 2nd ` F ) ) , <. ( 1st ` F ) , tpos ( 2nd ` F ) >. , (/) ) ) with typecode |-
22	3 21	eleqtrd	$$⊢\phi \to X\in if\left(\left(\mathrm{Rel}{2}^{nd}\left(F\right)\wedge \mathrm{Rel}\mathrm{dom}{2}^{nd}\left(F\right)\right),⟨1^{st}\left(F\right),tpos{2}^{nd}\left(F\right)⟩,\varnothing \right)$$
23	22	ne0d	$$⊢\phi \to if\left(\left(\mathrm{Rel}{2}^{nd}\left(F\right)\wedge \mathrm{Rel}\mathrm{dom}{2}^{nd}\left(F\right)\right),⟨1^{st}\left(F\right),tpos{2}^{nd}\left(F\right)⟩,\varnothing \right)\ne \varnothing$$
24		iffalse	$$⊢\neg \left(\mathrm{Rel}{2}^{nd}\left(F\right)\wedge \mathrm{Rel}\mathrm{dom}{2}^{nd}\left(F\right)\right)\to if\left(\left(\mathrm{Rel}{2}^{nd}\left(F\right)\wedge \mathrm{Rel}\mathrm{dom}{2}^{nd}\left(F\right)\right),⟨1^{st}\left(F\right),tpos{2}^{nd}\left(F\right)⟩,\varnothing \right)=\varnothing$$
25	24	necon1ai	$$⊢if\left(\left(\mathrm{Rel}{2}^{nd}\left(F\right)\wedge \mathrm{Rel}\mathrm{dom}{2}^{nd}\left(F\right)\right),⟨1^{st}\left(F\right),tpos{2}^{nd}\left(F\right)⟩,\varnothing \right)\ne \varnothing \to \left(\mathrm{Rel}{2}^{nd}\left(F\right)\wedge \mathrm{Rel}\mathrm{dom}{2}^{nd}\left(F\right)\right)$$
26	23 25	syl	$$⊢\phi \to \left(\mathrm{Rel}{2}^{nd}\left(F\right)\wedge \mathrm{Rel}\mathrm{dom}{2}^{nd}\left(F\right)\right)$$
27	11 26	jca	$$⊢\phi \to \left(F\ne \varnothing \wedge \left(\mathrm{Rel}{2}^{nd}\left(F\right)\wedge \mathrm{Rel}\mathrm{dom}{2}^{nd}\left(F\right)\right)\right)$$