isfth

Description: Value of the set of faithful functors between two categories. (Contributed by Mario Carneiro, 27-Jan-2017)

		Ref	Expression
	Hypothesis	isfth.b	$⊢ B = {Base}_{C}$
	Assertion	isfth	$⊢ F (C Faith D) G \leftrightarrow (F (C Func D) G \land \forall x \in B \forall y \in B Fun {(x G y)}^{-1})$

Proof

Step	Hyp	Ref	Expression
1		isfth.b	$⊢ B = {Base}_{C}$
2		fthfunc	$⊢ C Faith D \subseteq C Func D$
3	2	ssbri	$⊢ F (C Faith D) G \to F (C Func D) G$
4		df-br	$⊢ F (C Func D) G \leftrightarrow ⟨F, G⟩ \in (C Func D)$
5		funcrcl	$⊢ ⟨F, G⟩ \in (C Func D) \to (C \in Cat \land D \in Cat)$
6	4 5	sylbi	$⊢ F (C Func D) G \to (C \in Cat \land D \in Cat)$
7		oveq12	$⊢ (c = C \land d = D) \to c Func d = C Func D$
8	7	breqd	$⊢ (c = C \land d = D) \to (f (c Func d) g \leftrightarrow f (C Func D) g)$
9		simpl	$⊢ (c = C \land d = D) \to c = C$
10	9	fveq2d	$⊢ (c = C \land d = D) \to {Base}_{c} = {Base}_{C}$
11	10 1	eqtr4di	$⊢ (c = C \land d = D) \to {Base}_{c} = B$
12	11	raleqdv	$⊢ (c = C \land d = D) \to (\forall y \in {Base}_{c} Fun {(x g y)}^{-1} \leftrightarrow \forall y \in B Fun {(x g y)}^{-1})$
13	11 12	raleqbidv	$⊢ (c = C \land d = D) \to (\forall x \in {Base}_{c} \forall y \in {Base}_{c} Fun {(x g y)}^{-1} \leftrightarrow \forall x \in B \forall y \in B Fun {(x g y)}^{-1})$
14	8 13	anbi12d	$⊢ (c = C \land d = D) \to ((f (c Func d) g \land \forall x \in {Base}_{c} \forall y \in {Base}_{c} Fun {(x g y)}^{-1}) \leftrightarrow (f (C Func D) g \land \forall x \in B \forall y \in B Fun {(x g y)}^{-1}))$
15	14	opabbidv	$⊢ (c = C \land d = D) \to \{⟨f, g⟩ \| (f (c Func d) g \land \forall x \in {Base}_{c} \forall y \in {Base}_{c} Fun {(x g y)}^{-1})\} = \{⟨f, g⟩ \| (f (C Func D) g \land \forall x \in B \forall y \in B Fun {(x g y)}^{-1})\}$
16		df-fth	$⊢ Faith = (c \in Cat, d \in Cat ⟼ \{⟨f, g⟩ \| (f (c Func d) g \land \forall x \in {Base}_{c} \forall y \in {Base}_{c} Fun {(x g y)}^{-1})\})$
17		ovex	$⊢ C Func D \in V$
18		simpl	$⊢ (f (C Func D) g \land \forall x \in B \forall y \in B Fun {(x g y)}^{-1}) \to f (C Func D) g$
19	18	ssopab2i	$⊢ \{⟨f, g⟩ \| (f (C Func D) g \land \forall x \in B \forall y \in B Fun {(x g y)}^{-1})\} \subseteq \{⟨f, g⟩ \| f (C Func D) g\}$
20		opabss	$⊢ \{⟨f, g⟩ \| f (C Func D) g\} \subseteq C Func D$
21	19 20	sstri	$⊢ \{⟨f, g⟩ \| (f (C Func D) g \land \forall x \in B \forall y \in B Fun {(x g y)}^{-1})\} \subseteq C Func D$
22	17 21	ssexi	$⊢ \{⟨f, g⟩ \| (f (C Func D) g \land \forall x \in B \forall y \in B Fun {(x g y)}^{-1})\} \in V$
23	15 16 22	ovmpoa	$⊢ (C \in Cat \land D \in Cat) \to C Faith D = \{⟨f, g⟩ \| (f (C Func D) g \land \forall x \in B \forall y \in B Fun {(x g y)}^{-1})\}$
24	6 23	syl	$⊢ F (C Func D) G \to C Faith D = \{⟨f, g⟩ \| (f (C Func D) g \land \forall x \in B \forall y \in B Fun {(x g y)}^{-1})\}$
25	24	breqd	$⊢ F (C Func D) G \to (F (C Faith D) G \leftrightarrow F \{⟨f, g⟩ \| (f (C Func D) g \land \forall x \in B \forall y \in B Fun {(x g y)}^{-1})\} G)$
26		relfunc	$⊢ Rel (C Func D)$
27	26	brrelex12i	$⊢ F (C Func D) G \to (F \in V \land G \in V)$
28		breq12	$⊢ (f = F \land g = G) \to (f (C Func D) g \leftrightarrow F (C Func D) G)$
29		simpr	$⊢ (f = F \land g = G) \to g = G$
30	29	oveqd	$⊢ (f = F \land g = G) \to x g y = x G y$
31	30	cnveqd	$⊢ (f = F \land g = G) \to {(x g y)}^{-1} = {(x G y)}^{-1}$
32	31	funeqd	$⊢ (f = F \land g = G) \to (Fun {(x g y)}^{-1} \leftrightarrow Fun {(x G y)}^{-1})$
33	32	2ralbidv	$⊢ (f = F \land g = G) \to (\forall x \in B \forall y \in B Fun {(x g y)}^{-1} \leftrightarrow \forall x \in B \forall y \in B Fun {(x G y)}^{-1})$
34	28 33	anbi12d	$⊢ (f = F \land g = G) \to ((f (C Func D) g \land \forall x \in B \forall y \in B Fun {(x g y)}^{-1}) \leftrightarrow (F (C Func D) G \land \forall x \in B \forall y \in B Fun {(x G y)}^{-1}))$
35		eqid	$⊢ \{⟨f, g⟩ \| (f (C Func D) g \land \forall x \in B \forall y \in B Fun {(x g y)}^{-1})\} = \{⟨f, g⟩ \| (f (C Func D) g \land \forall x \in B \forall y \in B Fun {(x g y)}^{-1})\}$
36	34 35	brabga	$⊢ (F \in V \land G \in V) \to (F \{⟨f, g⟩ \| (f (C Func D) g \land \forall x \in B \forall y \in B Fun {(x g y)}^{-1})\} G \leftrightarrow (F (C Func D) G \land \forall x \in B \forall y \in B Fun {(x G y)}^{-1}))$
37	27 36	syl	$⊢ F (C Func D) G \to (F \{⟨f, g⟩ \| (f (C Func D) g \land \forall x \in B \forall y \in B Fun {(x g y)}^{-1})\} G \leftrightarrow (F (C Func D) G \land \forall x \in B \forall y \in B Fun {(x G y)}^{-1}))$
38	25 37	bitrd	$⊢ F (C Func D) G \to (F (C Faith D) G \leftrightarrow (F (C Func D) G \land \forall x \in B \forall y \in B Fun {(x G y)}^{-1}))$
39	38	bianabs	$⊢ F (C Func D) G \to (F (C Faith D) G \leftrightarrow \forall x \in B \forall y \in B Fun {(x G y)}^{-1})$
40	3 39	biadanii	$⊢ F (C Faith D) G \leftrightarrow (F (C Func D) G \land \forall x \in B \forall y \in B Fun {(x G y)}^{-1})$

Metamath Proof Explorer

Theorem isfth

Proof