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

Metamath Proof Explorer

Theorem fulloppf

Description: The opposite functor of a full functor is also full. Proposition 3.43(d) in Adamek p. 39. (Contributed by Zhi Wang, 26-Nov-2025)

Ref Expression
Hypotheses fulloppf.o ⊢ 𝑂 = ( oppCat ‘ 𝐶 )
fulloppf.p ⊢ 𝑃 = ( oppCat ‘ 𝐷 )
fulloppf.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Full 𝐷 ) )
Assertion fulloppf ( 𝜑 → ( oppFunc ‘ 𝐹 ) ∈ ( 𝑂 Full 𝑃 ) )

Proof

Step Hyp Ref Expression
1 fulloppf.o ⊢ 𝑂 = ( oppCat ‘ 𝐶 )
2 fulloppf.p ⊢ 𝑃 = ( oppCat ‘ 𝐷 )
3 fulloppf.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Full 𝐷 ) )
4 fullfunc ⊢ ( 𝐶 Full 𝐷 ) ⊆ ( 𝐶 Func 𝐷 )
5 4 sseli ⊢ ( 𝐹 ∈ ( 𝐶 Full 𝐷 ) → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
6 oppfval2 ⊢ ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) → ( oppFunc ‘ 𝐹 ) = ⟨ ( 1st ‘ 𝐹 ) , tpos ( 2nd ‘ 𝐹 ) ⟩ )
7 3 5 6 3syl ⊢ ( 𝜑 → ( oppFunc ‘ 𝐹 ) = ⟨ ( 1st ‘ 𝐹 ) , tpos ( 2nd ‘ 𝐹 ) ⟩ )
8 relfull ⊢ Rel ( 𝐶 Full 𝐷 )
9 1st2ndbr ⊢ ( ( Rel ( 𝐶 Full 𝐷 ) ∧ 𝐹 ∈ ( 𝐶 Full 𝐷 ) ) → ( 1st ‘ 𝐹 ) ( 𝐶 Full 𝐷 ) ( 2nd ‘ 𝐹 ) )
10 8 3 9 sylancr ⊢ ( 𝜑 → ( 1st ‘ 𝐹 ) ( 𝐶 Full 𝐷 ) ( 2nd ‘ 𝐹 ) )
11 1 2 10 fulloppc ⊢ ( 𝜑 → ( 1st ‘ 𝐹 ) ( 𝑂 Full 𝑃 ) tpos ( 2nd ‘ 𝐹 ) )
12 df-br ⊢ ( ( 1st ‘ 𝐹 ) ( 𝑂 Full 𝑃 ) tpos ( 2nd ‘ 𝐹 ) ↔ ⟨ ( 1st ‘ 𝐹 ) , tpos ( 2nd ‘ 𝐹 ) ⟩ ∈ ( 𝑂 Full 𝑃 ) )
13 11 12 sylib ⊢ ( 𝜑 → ⟨ ( 1st ‘ 𝐹 ) , tpos ( 2nd ‘ 𝐹 ) ⟩ ∈ ( 𝑂 Full 𝑃 ) )
14 7 13 eqeltrd ⊢ ( 𝜑 → ( oppFunc ‘ 𝐹 ) ∈ ( 𝑂 Full 𝑃 ) )