Theorem isffth2

Description: A fully faithful functor is a functor which is bijective on hom-sets. (Contributed by Mario Carneiro, 27-Jan-2017)

	Ref	Expression
Hypotheses	isfth.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	isfth.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
	isfth.j	⊢ 𝐽 = ( Hom ‘ 𝐷 )
Assertion	isffth2	⊢ ( 𝐹 ( ( 𝐶 Full 𝐷 ) ∩ ( 𝐶 Faith 𝐷 ) ) 𝐺 ↔ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) –1-1-onto→ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		isfth.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
2		isfth.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
3		isfth.j	⊢ 𝐽 = ( Hom ‘ 𝐷 )
4	1 3 2	isfull2	⊢ ( 𝐹 ( 𝐶 Full 𝐷 ) 𝐺 ↔ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) –onto→ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) )
5	1 2 3	isfth2	⊢ ( 𝐹 ( 𝐶 Faith 𝐷 ) 𝐺 ↔ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) –1-1→ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) )
6	4 5	anbi12i	⊢ ( ( 𝐹 ( 𝐶 Full 𝐷 ) 𝐺 ∧ 𝐹 ( 𝐶 Faith 𝐷 ) 𝐺 ) ↔ ( ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) –onto→ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) –1-1→ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) ) )
7		brin	⊢ ( 𝐹 ( ( 𝐶 Full 𝐷 ) ∩ ( 𝐶 Faith 𝐷 ) ) 𝐺 ↔ ( 𝐹 ( 𝐶 Full 𝐷 ) 𝐺 ∧ 𝐹 ( 𝐶 Faith 𝐷 ) 𝐺 ) )
8		df-f1o	⊢ ( ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) –1-1-onto→ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ↔ ( ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) –1-1→ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) –onto→ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) )
9	8	biancomi	⊢ ( ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) –1-1-onto→ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ↔ ( ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) –onto→ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) –1-1→ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) )
10	9	2ralbii	⊢ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) –1-1-onto→ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) –onto→ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) –1-1→ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) )
11		r19.26-2	⊢ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) –onto→ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) –1-1→ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) ↔ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) –onto→ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) –1-1→ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) )
12	10 11	bitri	⊢ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) –1-1-onto→ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ↔ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) –onto→ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) –1-1→ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) )
13	12	anbi2i	⊢ ( ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) –1-1-onto→ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) ↔ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∧ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) –onto→ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) –1-1→ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) ) )
14		anandi	⊢ ( ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∧ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) –onto→ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) –1-1→ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) ) ↔ ( ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) –onto→ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) –1-1→ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) ) )
15	13 14	bitri	⊢ ( ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) –1-1-onto→ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) ↔ ( ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) –onto→ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) –1-1→ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) ) )
16	6 7 15	3bitr4i	⊢ ( 𝐹 ( ( 𝐶 Full 𝐷 ) ∩ ( 𝐶 Faith 𝐷 ) ) 𝐺 ↔ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) –1-1-onto→ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) )