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	⊢ 𝐺 = ( oppFunc ‘ 𝐹 )
	eloppf.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐺 )
Assertion	eloppf	⊢ ( 𝜑 → ( 𝐹 ≠ ∅ ∧ ( Rel ( 2^nd ‘ 𝐹 ) ∧ Rel dom ( 2^nd ‘ 𝐹 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		eloppf.g	⊢ 𝐺 = ( oppFunc ‘ 𝐹 )
2		eloppf.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐺 )
3	2 1	eleqtrdi	⊢ ( 𝜑 → 𝑋 ∈ ( oppFunc ‘ 𝐹 ) )
4		elfvdm	⊢ ( 𝑋 ∈ ( oppFunc ‘ 𝐹 ) → 𝐹 ∈ dom oppFunc )
5		oppffn	⊢ oppFunc Fn ( V × V )
6	5	fndmi	⊢ dom oppFunc = ( V × V )
7	4 6	eleqtrdi	⊢ ( 𝑋 ∈ ( oppFunc ‘ 𝐹 ) → 𝐹 ∈ ( V × V ) )
8	3 7	syl	⊢ ( 𝜑 → 𝐹 ∈ ( V × V ) )
9		0nelxp	⊢ ¬ ∅ ∈ ( V × V )
10		nelne2	⊢ ( ( 𝐹 ∈ ( V × V ) ∧ ¬ ∅ ∈ ( V × V ) ) → 𝐹 ≠ ∅ )
11	8 9 10	sylancl	⊢ ( 𝜑 → 𝐹 ≠ ∅ )
12		1st2nd2	⊢ ( 𝐹 ∈ ( V × V ) → 𝐹 = ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ )
13	3 7 12	3syl	⊢ ( 𝜑 → 𝐹 = ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ )
14	13	fveq2d	⊢ ( 𝜑 → ( oppFunc ‘ 𝐹 ) = ( oppFunc ‘ ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ ) )
15		df-ov	⊢ ( ( 1^st ‘ 𝐹 ) oppFunc ( 2^nd ‘ 𝐹 ) ) = ( oppFunc ‘ ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ )
16		fvex	⊢ ( 1^st ‘ 𝐹 ) ∈ V
17		fvex	⊢ ( 2^nd ‘ 𝐹 ) ∈ V
18		oppfvalg	⊢ ( ( ( 1^st ‘ 𝐹 ) ∈ V ∧ ( 2^nd ‘ 𝐹 ) ∈ V ) → ( ( 1^st ‘ 𝐹 ) oppFunc ( 2^nd ‘ 𝐹 ) ) = if ( ( Rel ( 2^nd ‘ 𝐹 ) ∧ Rel dom ( 2^nd ‘ 𝐹 ) ) , ⟨ ( 1^st ‘ 𝐹 ) , tpos ( 2^nd ‘ 𝐹 ) ⟩ , ∅ ) )
19	16 17 18	mp2an	⊢ ( ( 1^st ‘ 𝐹 ) oppFunc ( 2^nd ‘ 𝐹 ) ) = if ( ( Rel ( 2^nd ‘ 𝐹 ) ∧ Rel dom ( 2^nd ‘ 𝐹 ) ) , ⟨ ( 1^st ‘ 𝐹 ) , tpos ( 2^nd ‘ 𝐹 ) ⟩ , ∅ )
20	15 19	eqtr3i	⊢ ( oppFunc ‘ ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ ) = if ( ( Rel ( 2^nd ‘ 𝐹 ) ∧ Rel dom ( 2^nd ‘ 𝐹 ) ) , ⟨ ( 1^st ‘ 𝐹 ) , tpos ( 2^nd ‘ 𝐹 ) ⟩ , ∅ )
21	14 20	eqtrdi	⊢ ( 𝜑 → ( oppFunc ‘ 𝐹 ) = if ( ( Rel ( 2^nd ‘ 𝐹 ) ∧ Rel dom ( 2^nd ‘ 𝐹 ) ) , ⟨ ( 1^st ‘ 𝐹 ) , tpos ( 2^nd ‘ 𝐹 ) ⟩ , ∅ ) )
22	3 21	eleqtrd	⊢ ( 𝜑 → 𝑋 ∈ if ( ( Rel ( 2^nd ‘ 𝐹 ) ∧ Rel dom ( 2^nd ‘ 𝐹 ) ) , ⟨ ( 1^st ‘ 𝐹 ) , tpos ( 2^nd ‘ 𝐹 ) ⟩ , ∅ ) )
23	22	ne0d	⊢ ( 𝜑 → if ( ( Rel ( 2^nd ‘ 𝐹 ) ∧ Rel dom ( 2^nd ‘ 𝐹 ) ) , ⟨ ( 1^st ‘ 𝐹 ) , tpos ( 2^nd ‘ 𝐹 ) ⟩ , ∅ ) ≠ ∅ )
24		iffalse	⊢ ( ¬ ( Rel ( 2^nd ‘ 𝐹 ) ∧ Rel dom ( 2^nd ‘ 𝐹 ) ) → if ( ( Rel ( 2^nd ‘ 𝐹 ) ∧ Rel dom ( 2^nd ‘ 𝐹 ) ) , ⟨ ( 1^st ‘ 𝐹 ) , tpos ( 2^nd ‘ 𝐹 ) ⟩ , ∅ ) = ∅ )
25	24	necon1ai	⊢ ( if ( ( Rel ( 2^nd ‘ 𝐹 ) ∧ Rel dom ( 2^nd ‘ 𝐹 ) ) , ⟨ ( 1^st ‘ 𝐹 ) , tpos ( 2^nd ‘ 𝐹 ) ⟩ , ∅ ) ≠ ∅ → ( Rel ( 2^nd ‘ 𝐹 ) ∧ Rel dom ( 2^nd ‘ 𝐹 ) ) )
26	23 25	syl	⊢ ( 𝜑 → ( Rel ( 2^nd ‘ 𝐹 ) ∧ Rel dom ( 2^nd ‘ 𝐹 ) ) )
27	11 26	jca	⊢ ( 𝜑 → ( 𝐹 ≠ ∅ ∧ ( Rel ( 2^nd ‘ 𝐹 ) ∧ Rel dom ( 2^nd ‘ 𝐹 ) ) ) )

Metamath Proof Explorer

Theorem eloppf

Proof