oppc1stflem

Description: A utility theorem for proving theorems on projection functors of opposite categories. (Contributed by Zhi Wang, 19-Nov-2025)

	Ref	Expression
Hypotheses	oppc1stf.o	⊢ 𝑂 = ( oppCat ‘ 𝐶 )
	oppc1stf.p	⊢ 𝑃 = ( oppCat ‘ 𝐷 )
	oppc1stf.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
	oppc1stf.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑊 )
	oppc1stflem.1	⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) ) → ( oppFunc ‘ ( 𝐶 𝐹 𝐷 ) ) = ( 𝑂 𝐹 𝑃 ) )
	oppc1stflem.f	⊢ 𝐹 = ( 𝑐 ∈ Cat , 𝑑 ∈ Cat ↦ 𝑌 )
Assertion	oppc1stflem	⊢ ( 𝜑 → ( oppFunc ‘ ( 𝐶 𝐹 𝐷 ) ) = ( 𝑂 𝐹 𝑃 ) )

Proof

Step	Hyp	Ref	Expression
1		oppc1stf.o	⊢ 𝑂 = ( oppCat ‘ 𝐶 )
2		oppc1stf.p	⊢ 𝑃 = ( oppCat ‘ 𝐷 )
3		oppc1stf.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
4		oppc1stf.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑊 )
5		oppc1stflem.1	⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) ) → ( oppFunc ‘ ( 𝐶 𝐹 𝐷 ) ) = ( 𝑂 𝐹 𝑃 ) )
6		oppc1stflem.f	⊢ 𝐹 = ( 𝑐 ∈ Cat , 𝑑 ∈ Cat ↦ 𝑌 )
7		eqid	⊢ ( oppFunc ‘ ( 𝐶 𝐹 𝐷 ) ) = ( oppFunc ‘ ( 𝐶 𝐹 𝐷 ) )
8		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( oppFunc ‘ ( 𝐶 𝐹 𝐷 ) ) ) → 𝑥 ∈ ( oppFunc ‘ ( 𝐶 𝐹 𝐷 ) ) )
9	7 8	eloppf	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( oppFunc ‘ ( 𝐶 𝐹 𝐷 ) ) ) → ( ( 𝐶 𝐹 𝐷 ) ≠ ∅ ∧ ( Rel ( 2^nd ‘ ( 𝐶 𝐹 𝐷 ) ) ∧ Rel dom ( 2^nd ‘ ( 𝐶 𝐹 𝐷 ) ) ) ) )
10	9	simpld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( oppFunc ‘ ( 𝐶 𝐹 𝐷 ) ) ) → ( 𝐶 𝐹 𝐷 ) ≠ ∅ )
11	6	mpondm0	⊢ ( ¬ ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) → ( 𝐶 𝐹 𝐷 ) = ∅ )
12	11	necon1ai	⊢ ( ( 𝐶 𝐹 𝐷 ) ≠ ∅ → ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) )
13	10 12	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( oppFunc ‘ ( 𝐶 𝐹 𝐷 ) ) ) → ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) )
14		simplr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( oppFunc ‘ ( 𝐶 𝐹 𝐷 ) ) ) ∧ ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) ) → 𝑥 ∈ ( oppFunc ‘ ( 𝐶 𝐹 𝐷 ) ) )
15	5	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( oppFunc ‘ ( 𝐶 𝐹 𝐷 ) ) ) ∧ ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) ) → ( oppFunc ‘ ( 𝐶 𝐹 𝐷 ) ) = ( 𝑂 𝐹 𝑃 ) )
16	14 15	eleqtrd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( oppFunc ‘ ( 𝐶 𝐹 𝐷 ) ) ) ∧ ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) ) → 𝑥 ∈ ( 𝑂 𝐹 𝑃 ) )
17	13 16	mpdan	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( oppFunc ‘ ( 𝐶 𝐹 𝐷 ) ) ) → 𝑥 ∈ ( 𝑂 𝐹 𝑃 ) )
18	1 3	oppccatb	⊢ ( 𝜑 → ( 𝐶 ∈ Cat ↔ 𝑂 ∈ Cat ) )
19	2 4	oppccatb	⊢ ( 𝜑 → ( 𝐷 ∈ Cat ↔ 𝑃 ∈ Cat ) )
20	18 19	anbi12d	⊢ ( 𝜑 → ( ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) ↔ ( 𝑂 ∈ Cat ∧ 𝑃 ∈ Cat ) ) )
21	20	biimprd	⊢ ( 𝜑 → ( ( 𝑂 ∈ Cat ∧ 𝑃 ∈ Cat ) → ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) ) )
22	6	elmpocl	⊢ ( 𝑥 ∈ ( 𝑂 𝐹 𝑃 ) → ( 𝑂 ∈ Cat ∧ 𝑃 ∈ Cat ) )
23	21 22	impel	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑂 𝐹 𝑃 ) ) → ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) )
24		simplr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑂 𝐹 𝑃 ) ) ∧ ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) ) → 𝑥 ∈ ( 𝑂 𝐹 𝑃 ) )
25	5	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑂 𝐹 𝑃 ) ) ∧ ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) ) → ( oppFunc ‘ ( 𝐶 𝐹 𝐷 ) ) = ( 𝑂 𝐹 𝑃 ) )
26	24 25	eleqtrrd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑂 𝐹 𝑃 ) ) ∧ ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) ) → 𝑥 ∈ ( oppFunc ‘ ( 𝐶 𝐹 𝐷 ) ) )
27	23 26	mpdan	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑂 𝐹 𝑃 ) ) → 𝑥 ∈ ( oppFunc ‘ ( 𝐶 𝐹 𝐷 ) ) )
28	17 27	impbida	⊢ ( 𝜑 → ( 𝑥 ∈ ( oppFunc ‘ ( 𝐶 𝐹 𝐷 ) ) ↔ 𝑥 ∈ ( 𝑂 𝐹 𝑃 ) ) )
29	28	eqrdv	⊢ ( 𝜑 → ( oppFunc ‘ ( 𝐶 𝐹 𝐷 ) ) = ( 𝑂 𝐹 𝑃 ) )

Metamath Proof Explorer

Theorem oppc1stflem

Proof