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

Metamath Proof Explorer

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	$⊢ φ \to X \in K$
	Assertion	eloppf2	$⊢ φ \to ((F \in V \land G \in V) \land (Rel G \land Rel dom G))$

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	$⊢ φ \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	$⊢ φ \to (F \in V \land G \in V)$
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	$⊢ φ \to X \in if ((Rel G \land Rel dom G), ⟨F, tpos G⟩, \emptyset)$
10	9	ne0d	$⊢ φ \to if ((Rel G \land Rel dom G), ⟨F, tpos G⟩, \emptyset) \neq \emptyset$
11		iffalse	$⊢ \neg (Rel G \land Rel dom G) \to if ((Rel G \land Rel dom G), ⟨F, tpos G⟩, \emptyset) = \emptyset$
12	11	necon1ai	$⊢ if ((Rel G \land Rel dom G), ⟨F, tpos G⟩, \emptyset) \neq \emptyset \to (Rel G \land Rel dom G)$
13	10 12	syl	$⊢ φ \to (Rel G \land Rel dom G)$
14	6 13	jca	$⊢ φ \to ((F \in V \land G \in V) \land (Rel G \land Rel dom G))$