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 ⊢ ( 𝐹 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 𝐺 ) ) )