Metamath Proof Explorer

Theorem fulloppc

Description: The opposite functor of a full functor is also full. Proposition 3.43(d) in Adamek p. 39. (Contributed by Mario Carneiro, 27-Jan-2017)

Ref Expression
Hypotheses fulloppc.o ⊢ 𝑂 = ( oppCat ‘ 𝐶 )
fulloppc.p ⊢ 𝑃 = ( oppCat ‘ 𝐷 )
fulloppc.f ⊢ ( 𝜑 → 𝐹 ( 𝐶 Full 𝐷 ) 𝐺 )
Assertion fulloppc ( 𝜑 → 𝐹 ( 𝑂 Full 𝑃 ) tpos 𝐺 )

Proof

Step Hyp Ref Expression
1 fulloppc.o ⊢ 𝑂 = ( oppCat ‘ 𝐶 )
2 fulloppc.p ⊢ 𝑃 = ( oppCat ‘ 𝐷 )
3 fulloppc.f ⊢ ( 𝜑 → 𝐹 ( 𝐶 Full 𝐷 ) 𝐺 )
4 fullfunc ⊢ ( 𝐶 Full 𝐷 ) ⊆ ( 𝐶 Func 𝐷 )
5 4 ssbri ⊢ ( 𝐹 ( 𝐶 Full 𝐷 ) 𝐺 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
6 3 5 syl ⊢ ( 𝜑 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
7 1 2 6 funcoppc ⊢ ( 𝜑 → 𝐹 ( 𝑂 Func 𝑃 ) tpos 𝐺 )
8 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
9 eqid ⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
10 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
11 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → 𝐹 ( 𝐶 Full 𝐷 ) 𝐺 )
12 simprr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑦 ∈ ( Base ‘ 𝐶 ) )
13 simprl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
14 8 9 10 11 12 13 fullfo ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑦 𝐺 𝑥 ) : ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) –onto→ ( ( 𝐹 ‘ 𝑦 ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ 𝑥 ) ) )
15 forn ⊢ ( ( 𝑦 𝐺 𝑥 ) : ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) –onto→ ( ( 𝐹 ‘ 𝑦 ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ 𝑥 ) ) → ran ( 𝑦 𝐺 𝑥 ) = ( ( 𝐹 ‘ 𝑦 ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ 𝑥 ) ) )
16 14 15 syl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ran ( 𝑦 𝐺 𝑥 ) = ( ( 𝐹 ‘ 𝑦 ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ 𝑥 ) ) )
17 ovtpos ⊢ ( 𝑥 tpos 𝐺 𝑦 ) = ( 𝑦 𝐺 𝑥 )
18 17 rneqi ⊢ ran ( 𝑥 tpos 𝐺 𝑦 ) = ran ( 𝑦 𝐺 𝑥 )
19 9 2 oppchom ⊢ ( ( 𝐹 ‘ 𝑥 ) ( Hom ‘ 𝑃 ) ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑦 ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ 𝑥 ) )
20 16 18 19 3eqtr4g ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ran ( 𝑥 tpos 𝐺 𝑦 ) = ( ( 𝐹 ‘ 𝑥 ) ( Hom ‘ 𝑃 ) ( 𝐹 ‘ 𝑦 ) ) )
21 20 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ran ( 𝑥 tpos 𝐺 𝑦 ) = ( ( 𝐹 ‘ 𝑥 ) ( Hom ‘ 𝑃 ) ( 𝐹 ‘ 𝑦 ) ) )
22 1 8 oppcbas ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝑂 )
23 eqid ⊢ ( Hom ‘ 𝑃 ) = ( Hom ‘ 𝑃 )
24 22 23 isfull ⊢ ( 𝐹 ( 𝑂 Full 𝑃 ) tpos 𝐺 ↔ ( 𝐹 ( 𝑂 Func 𝑃 ) tpos 𝐺 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ran ( 𝑥 tpos 𝐺 𝑦 ) = ( ( 𝐹 ‘ 𝑥 ) ( Hom ‘ 𝑃 ) ( 𝐹 ‘ 𝑦 ) ) ) )
25 7 21 24 sylanbrc ⊢ ( 𝜑 → 𝐹 ( 𝑂 Full 𝑃 ) tpos 𝐺 )