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	⊢ ( 𝐹 oppFunc 𝐺 ) = 𝐾
	eloppf2.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐾 )
Assertion	eloppf2	⊢ ( 𝜑 → ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ ( Rel 𝐺 ∧ Rel dom 𝐺 ) ) )

Proof

Step	Hyp	Ref	Expression
1		eloppf2.k	⊢ ( 𝐹 oppFunc 𝐺 ) = 𝐾
2		eloppf2.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐾 )
3	2 1	eleqtrrdi	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐹 oppFunc 𝐺 ) )
4		df-oppf	⊢ oppFunc = ( 𝑓 ∈ V , 𝑔 ∈ V ↦ if ( ( Rel 𝑔 ∧ Rel dom 𝑔 ) , ⟨ 𝑓 , tpos 𝑔 ⟩ , ∅ ) )
5	4	elmpocl	⊢ ( 𝑋 ∈ ( 𝐹 oppFunc 𝐺 ) → ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) )
6	3 5	syl	⊢ ( 𝜑 → ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) )
7		oppfvalg	⊢ ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) → ( 𝐹 oppFunc 𝐺 ) = if ( ( Rel 𝐺 ∧ Rel dom 𝐺 ) , ⟨ 𝐹 , tpos 𝐺 ⟩ , ∅ ) )
8	6 7	syl	⊢ ( 𝜑 → ( 𝐹 oppFunc 𝐺 ) = if ( ( Rel 𝐺 ∧ Rel dom 𝐺 ) , ⟨ 𝐹 , tpos 𝐺 ⟩ , ∅ ) )
9	3 8	eleqtrd	⊢ ( 𝜑 → 𝑋 ∈ if ( ( Rel 𝐺 ∧ Rel dom 𝐺 ) , ⟨ 𝐹 , tpos 𝐺 ⟩ , ∅ ) )
10	9	ne0d	⊢ ( 𝜑 → if ( ( Rel 𝐺 ∧ Rel dom 𝐺 ) , ⟨ 𝐹 , tpos 𝐺 ⟩ , ∅ ) ≠ ∅ )
11		iffalse	⊢ ( ¬ ( Rel 𝐺 ∧ Rel dom 𝐺 ) → if ( ( Rel 𝐺 ∧ Rel dom 𝐺 ) , ⟨ 𝐹 , tpos 𝐺 ⟩ , ∅ ) = ∅ )
12	11	necon1ai	⊢ ( if ( ( Rel 𝐺 ∧ Rel dom 𝐺 ) , ⟨ 𝐹 , tpos 𝐺 ⟩ , ∅ ) ≠ ∅ → ( Rel 𝐺 ∧ Rel dom 𝐺 ) )
13	10 12	syl	⊢ ( 𝜑 → ( Rel 𝐺 ∧ Rel dom 𝐺 ) )
14	6 13	jca	⊢ ( 𝜑 → ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ ( Rel 𝐺 ∧ Rel dom 𝐺 ) ) )