Theorem swapfffth

Description: The swap functor is a fully faithful functor. (Contributed by Zhi Wang, 8-Oct-2025)

	Ref	Expression
Hypotheses	swapfid.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	swapfid.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
	swapfid.s	⊢ 𝑆 = ( 𝐶 ×c 𝐷 )
	swapfid.t	⊢ 𝑇 = ( 𝐷 ×c 𝐶 )
	swapfid.o	⊢ ( 𝜑 → ( 𝐶 swapF 𝐷 ) = ⟨ 𝑂 , 𝑃 ⟩ )
Assertion	swapfffth	⊢ ( 𝜑 → 𝑂 ( ( 𝑆 Full 𝑇 ) ∩ ( 𝑆 Faith 𝑇 ) ) 𝑃 )

Proof

Step	Hyp	Ref	Expression
1		swapfid.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
2		swapfid.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
3		swapfid.s	⊢ 𝑆 = ( 𝐶 ×c 𝐷 )
4		swapfid.t	⊢ 𝑇 = ( 𝐷 ×c 𝐶 )
5		swapfid.o	⊢ ( 𝜑 → ( 𝐶 swapF 𝐷 ) = ⟨ 𝑂 , 𝑃 ⟩ )
6	1 2 3 4 5	swapffunc	⊢ ( 𝜑 → 𝑂 ( 𝑆 Func 𝑇 ) 𝑃 )
7	5	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝐶 swapF 𝐷 ) = ⟨ 𝑂 , 𝑃 ⟩ )
8		eqid	⊢ ( Hom ‘ 𝑆 ) = ( Hom ‘ 𝑆 )
9		eqid	⊢ ( Hom ‘ 𝑇 ) = ( Hom ‘ 𝑇 )
10		eqid	⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
11		simprl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → 𝑥 ∈ ( Base ‘ 𝑆 ) )
12		simprr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → 𝑦 ∈ ( Base ‘ 𝑆 ) )
13	7 3 4 8 9 10 11 12	swapf2f1oa	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝑥 𝑃 𝑦 ) : ( 𝑥 ( Hom ‘ 𝑆 ) 𝑦 ) –1-1-onto→ ( ( 𝑂 ‘ 𝑥 ) ( Hom ‘ 𝑇 ) ( 𝑂 ‘ 𝑦 ) ) )
14	13	ralrimivva	⊢ ( 𝜑 → ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ∀ 𝑦 ∈ ( Base ‘ 𝑆 ) ( 𝑥 𝑃 𝑦 ) : ( 𝑥 ( Hom ‘ 𝑆 ) 𝑦 ) –1-1-onto→ ( ( 𝑂 ‘ 𝑥 ) ( Hom ‘ 𝑇 ) ( 𝑂 ‘ 𝑦 ) ) )
15	10 8 9	isffth2	⊢ ( 𝑂 ( ( 𝑆 Full 𝑇 ) ∩ ( 𝑆 Faith 𝑇 ) ) 𝑃 ↔ ( 𝑂 ( 𝑆 Func 𝑇 ) 𝑃 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ∀ 𝑦 ∈ ( Base ‘ 𝑆 ) ( 𝑥 𝑃 𝑦 ) : ( 𝑥 ( Hom ‘ 𝑆 ) 𝑦 ) –1-1-onto→ ( ( 𝑂 ‘ 𝑥 ) ( Hom ‘ 𝑇 ) ( 𝑂 ‘ 𝑦 ) ) ) )
16	6 14 15	sylanbrc	⊢ ( 𝜑 → 𝑂 ( ( 𝑆 Full 𝑇 ) ∩ ( 𝑆 Faith 𝑇 ) ) 𝑃 )