fullthinc

Description: A functor to a thin category is full iff empty hom-sets are mapped to empty hom-sets. (Contributed by Zhi Wang, 1-Oct-2024)

	Ref	Expression
Hypotheses	fullthinc.b	$⊢ B = {Base}_{C}$
	fullthinc.j	$⊢ J = Hom (D)$
	fullthinc.h	$⊢ H = Hom (C)$
	fullthinc.d	$⊢ φ \to D \in ThinCat$
	fullthinc.f	$⊢ φ \to F (C Func D) G$
Assertion	fullthinc	$⊢ φ \to (F (C Full D) G \leftrightarrow \forall x \in B \forall y \in B (x H y = \emptyset \to F (x) J F (y) = \emptyset))$

Proof

Step	Hyp	Ref	Expression
1		fullthinc.b	$⊢ B = {Base}_{C}$
2		fullthinc.j	$⊢ J = Hom (D)$
3		fullthinc.h	$⊢ H = Hom (C)$
4		fullthinc.d	$⊢ φ \to D \in ThinCat$
5		fullthinc.f	$⊢ φ \to F (C Func D) G$
6	1 2 3	isfull2	$⊢ F (C Full D) G \leftrightarrow (F (C Func D) G \land \forall x \in B \forall y \in B (x G y) : x H y \underset{onto}{⟶} F (x) J F (y))$
7		foeq2	$⊢ x H y = \emptyset \to ((x G y) : x H y \underset{onto}{⟶} F (x) J F (y) \leftrightarrow (x G y) : \emptyset \underset{onto}{⟶} F (x) J F (y))$
8		fo00	$⊢ (x G y) : \emptyset \underset{onto}{⟶} F (x) J F (y) \leftrightarrow (x G y = \emptyset \land F (x) J F (y) = \emptyset)$
9	8	simprbi	$⊢ (x G y) : \emptyset \underset{onto}{⟶} F (x) J F (y) \to F (x) J F (y) = \emptyset$
10	7 9	biimtrdi	$⊢ x H y = \emptyset \to ((x G y) : x H y \underset{onto}{⟶} F (x) J F (y) \to F (x) J F (y) = \emptyset)$
11	10	com12	$⊢ (x G y) : x H y \underset{onto}{⟶} F (x) J F (y) \to (x H y = \emptyset \to F (x) J F (y) = \emptyset)$
12	11	2ralimi	$⊢ \forall x \in B \forall y \in B (x G y) : x H y \underset{onto}{⟶} F (x) J F (y) \to \forall x \in B \forall y \in B (x H y = \emptyset \to F (x) J F (y) = \emptyset)$
13	6 12	simplbiim	$⊢ F (C Full D) G \to \forall x \in B \forall y \in B (x H y = \emptyset \to F (x) J F (y) = \emptyset)$
14	13	adantl	$⊢ ((D \in ThinCat \land F (C Func D) G) \land F (C Full D) G) \to \forall x \in B \forall y \in B (x H y = \emptyset \to F (x) J F (y) = \emptyset)$
15		simplr	$⊢ ((D \in ThinCat \land F (C Func D) G) \land \forall x \in B \forall y \in B (x H y = \emptyset \to F (x) J F (y) = \emptyset)) \to F (C Func D) G$
16		imor	$⊢ (x H y = \emptyset \to F (x) J F (y) = \emptyset) \leftrightarrow (\neg x H y = \emptyset \lor F (x) J F (y) = \emptyset)$
17		simplr	$⊢ ((D \in ThinCat \land F (C Func D) G) \land (x \in B \land y \in B)) \to F (C Func D) G$
18		simprl	$⊢ ((D \in ThinCat \land F (C Func D) G) \land (x \in B \land y \in B)) \to x \in B$
19		simprr	$⊢ ((D \in ThinCat \land F (C Func D) G) \land (x \in B \land y \in B)) \to y \in B$
20	1 3 2 17 18 19	funcf2	$⊢ ((D \in ThinCat \land F (C Func D) G) \land (x \in B \land y \in B)) \to (x G y) : x H y ⟶ F (x) J F (y)$
21	20	adantr	$⊢ (((D \in ThinCat \land F (C Func D) G) \land (x \in B \land y \in B)) \land \neg x H y = \emptyset) \to (x G y) : x H y ⟶ F (x) J F (y)$
22		simpr	$⊢ (((D \in ThinCat \land F (C Func D) G) \land (x \in B \land y \in B)) \land \neg x H y = \emptyset) \to \neg x H y = \emptyset$
23	22	neqned	$⊢ (((D \in ThinCat \land F (C Func D) G) \land (x \in B \land y \in B)) \land \neg x H y = \emptyset) \to x H y \neq \emptyset$
24		fdomne0	$⊢ ((x G y) : x H y ⟶ F (x) J F (y) \land x H y \neq \emptyset) \to (x G y \neq \emptyset \land F (x) J F (y) \neq \emptyset)$
25	21 23 24	syl2anc	$⊢ (((D \in ThinCat \land F (C Func D) G) \land (x \in B \land y \in B)) \land \neg x H y = \emptyset) \to (x G y \neq \emptyset \land F (x) J F (y) \neq \emptyset)$
26	25	simprd	$⊢ (((D \in ThinCat \land F (C Func D) G) \land (x \in B \land y \in B)) \land \neg x H y = \emptyset) \to F (x) J F (y) \neq \emptyset$
27		simplll	$⊢ (((D \in ThinCat \land F (C Func D) G) \land (x \in B \land y \in B)) \land \neg x H y = \emptyset) \to D \in ThinCat$
28		eqid	$⊢ {Base}_{D} = {Base}_{D}$
29	17	adantr	$⊢ (((D \in ThinCat \land F (C Func D) G) \land (x \in B \land y \in B)) \land \neg x H y = \emptyset) \to F (C Func D) G$
30	1 28 29	funcf1	$⊢ (((D \in ThinCat \land F (C Func D) G) \land (x \in B \land y \in B)) \land \neg x H y = \emptyset) \to F : B ⟶ {Base}_{D}$
31	18	adantr	$⊢ (((D \in ThinCat \land F (C Func D) G) \land (x \in B \land y \in B)) \land \neg x H y = \emptyset) \to x \in B$
32	30 31	ffvelcdmd	$⊢ (((D \in ThinCat \land F (C Func D) G) \land (x \in B \land y \in B)) \land \neg x H y = \emptyset) \to F (x) \in {Base}_{D}$
33	19	adantr	$⊢ (((D \in ThinCat \land F (C Func D) G) \land (x \in B \land y \in B)) \land \neg x H y = \emptyset) \to y \in B$
34	30 33	ffvelcdmd	$⊢ (((D \in ThinCat \land F (C Func D) G) \land (x \in B \land y \in B)) \land \neg x H y = \emptyset) \to F (y) \in {Base}_{D}$
35		eqidd	$⊢ (((D \in ThinCat \land F (C Func D) G) \land (x \in B \land y \in B)) \land \neg x H y = \emptyset) \to {Base}_{D} = {Base}_{D}$
36	2	a1i	$⊢ (((D \in ThinCat \land F (C Func D) G) \land (x \in B \land y \in B)) \land \neg x H y = \emptyset) \to J = Hom (D)$
37	27 32 34 35 36	thincn0eu	$⊢ (((D \in ThinCat \land F (C Func D) G) \land (x \in B \land y \in B)) \land \neg x H y = \emptyset) \to (F (x) J F (y) \neq \emptyset \leftrightarrow \exists! f f \in (F (x) J F (y)))$
38	26 37	mpbid	$⊢ (((D \in ThinCat \land F (C Func D) G) \land (x \in B \land y \in B)) \land \neg x H y = \emptyset) \to \exists! f f \in (F (x) J F (y))$
39		eusn	$⊢ \exists! f f \in (F (x) J F (y)) \leftrightarrow \exists f F (x) J F (y) = \{f\}$
40	38 39	sylib	$⊢ (((D \in ThinCat \land F (C Func D) G) \land (x \in B \land y \in B)) \land \neg x H y = \emptyset) \to \exists f F (x) J F (y) = \{f\}$
41	25	simpld	$⊢ (((D \in ThinCat \land F (C Func D) G) \land (x \in B \land y \in B)) \land \neg x H y = \emptyset) \to x G y \neq \emptyset$
42		foconst	$⊢ ((x G y) : x H y ⟶ \{f\} \land x G y \neq \emptyset) \to (x G y) : x H y \underset{onto}{⟶} \{f\}$
43		feq3	$⊢ F (x) J F (y) = \{f\} \to ((x G y) : x H y ⟶ F (x) J F (y) \leftrightarrow (x G y) : x H y ⟶ \{f\})$
44	43	anbi1d	$⊢ F (x) J F (y) = \{f\} \to (((x G y) : x H y ⟶ F (x) J F (y) \land x G y \neq \emptyset) \leftrightarrow ((x G y) : x H y ⟶ \{f\} \land x G y \neq \emptyset))$
45		foeq3	$⊢ F (x) J F (y) = \{f\} \to ((x G y) : x H y \underset{onto}{⟶} F (x) J F (y) \leftrightarrow (x G y) : x H y \underset{onto}{⟶} \{f\})$
46	44 45	imbi12d	$⊢ F (x) J F (y) = \{f\} \to ((((x G y) : x H y ⟶ F (x) J F (y) \land x G y \neq \emptyset) \to (x G y) : x H y \underset{onto}{⟶} F (x) J F (y)) \leftrightarrow (((x G y) : x H y ⟶ \{f\} \land x G y \neq \emptyset) \to (x G y) : x H y \underset{onto}{⟶} \{f\}))$
47	42 46	mpbiri	$⊢ F (x) J F (y) = \{f\} \to (((x G y) : x H y ⟶ F (x) J F (y) \land x G y \neq \emptyset) \to (x G y) : x H y \underset{onto}{⟶} F (x) J F (y))$
48	47	exlimiv	$⊢ \exists f F (x) J F (y) = \{f\} \to (((x G y) : x H y ⟶ F (x) J F (y) \land x G y \neq \emptyset) \to (x G y) : x H y \underset{onto}{⟶} F (x) J F (y))$
49	48	imp	$⊢ (\exists f F (x) J F (y) = \{f\} \land ((x G y) : x H y ⟶ F (x) J F (y) \land x G y \neq \emptyset)) \to (x G y) : x H y \underset{onto}{⟶} F (x) J F (y)$
50	40 21 41 49	syl12anc	$⊢ (((D \in ThinCat \land F (C Func D) G) \land (x \in B \land y \in B)) \land \neg x H y = \emptyset) \to (x G y) : x H y \underset{onto}{⟶} F (x) J F (y)$
51	20	adantr	$⊢ (((D \in ThinCat \land F (C Func D) G) \land (x \in B \land y \in B)) \land F (x) J F (y) = \emptyset) \to (x G y) : x H y ⟶ F (x) J F (y)$
52		feq3	$⊢ F (x) J F (y) = \emptyset \to ((x G y) : x H y ⟶ F (x) J F (y) \leftrightarrow (x G y) : x H y ⟶ \emptyset)$
53	52	adantl	$⊢ (((D \in ThinCat \land F (C Func D) G) \land (x \in B \land y \in B)) \land F (x) J F (y) = \emptyset) \to ((x G y) : x H y ⟶ F (x) J F (y) \leftrightarrow (x G y) : x H y ⟶ \emptyset)$
54	51 53	mpbid	$⊢ (((D \in ThinCat \land F (C Func D) G) \land (x \in B \land y \in B)) \land F (x) J F (y) = \emptyset) \to (x G y) : x H y ⟶ \emptyset$
55		f00	$⊢ (x G y) : x H y ⟶ \emptyset \leftrightarrow (x G y = \emptyset \land x H y = \emptyset)$
56	54 55	sylib	$⊢ (((D \in ThinCat \land F (C Func D) G) \land (x \in B \land y \in B)) \land F (x) J F (y) = \emptyset) \to (x G y = \emptyset \land x H y = \emptyset)$
57	56	simprd	$⊢ (((D \in ThinCat \land F (C Func D) G) \land (x \in B \land y \in B)) \land F (x) J F (y) = \emptyset) \to x H y = \emptyset$
58	56	simpld	$⊢ (((D \in ThinCat \land F (C Func D) G) \land (x \in B \land y \in B)) \land F (x) J F (y) = \emptyset) \to x G y = \emptyset$
59		simpr	$⊢ (((D \in ThinCat \land F (C Func D) G) \land (x \in B \land y \in B)) \land F (x) J F (y) = \emptyset) \to F (x) J F (y) = \emptyset$
60	8	biimpri	$⊢ (x G y = \emptyset \land F (x) J F (y) = \emptyset) \to (x G y) : \emptyset \underset{onto}{⟶} F (x) J F (y)$
61	60 7	imbitrrid	$⊢ x H y = \emptyset \to ((x G y = \emptyset \land F (x) J F (y) = \emptyset) \to (x G y) : x H y \underset{onto}{⟶} F (x) J F (y))$
62	61	imp	$⊢ (x H y = \emptyset \land (x G y = \emptyset \land F (x) J F (y) = \emptyset)) \to (x G y) : x H y \underset{onto}{⟶} F (x) J F (y)$
63	57 58 59 62	syl12anc	$⊢ (((D \in ThinCat \land F (C Func D) G) \land (x \in B \land y \in B)) \land F (x) J F (y) = \emptyset) \to (x G y) : x H y \underset{onto}{⟶} F (x) J F (y)$
64	50 63	jaodan	$⊢ (((D \in ThinCat \land F (C Func D) G) \land (x \in B \land y \in B)) \land (\neg x H y = \emptyset \lor F (x) J F (y) = \emptyset)) \to (x G y) : x H y \underset{onto}{⟶} F (x) J F (y)$
65	16 64	sylan2b	$⊢ (((D \in ThinCat \land F (C Func D) G) \land (x \in B \land y \in B)) \land (x H y = \emptyset \to F (x) J F (y) = \emptyset)) \to (x G y) : x H y \underset{onto}{⟶} F (x) J F (y)$
66	65	ex	$⊢ ((D \in ThinCat \land F (C Func D) G) \land (x \in B \land y \in B)) \to ((x H y = \emptyset \to F (x) J F (y) = \emptyset) \to (x G y) : x H y \underset{onto}{⟶} F (x) J F (y))$
67	66	ralimdvva	$⊢ (D \in ThinCat \land F (C Func D) G) \to (\forall x \in B \forall y \in B (x H y = \emptyset \to F (x) J F (y) = \emptyset) \to \forall x \in B \forall y \in B (x G y) : x H y \underset{onto}{⟶} F (x) J F (y))$
68	67	imp	$⊢ ((D \in ThinCat \land F (C Func D) G) \land \forall x \in B \forall y \in B (x H y = \emptyset \to F (x) J F (y) = \emptyset)) \to \forall x \in B \forall y \in B (x G y) : x H y \underset{onto}{⟶} F (x) J F (y)$
69	15 68 6	sylanbrc	$⊢ ((D \in ThinCat \land F (C Func D) G) \land \forall x \in B \forall y \in B (x H y = \emptyset \to F (x) J F (y) = \emptyset)) \to F (C Full D) G$
70	14 69	impbida	$⊢ (D \in ThinCat \land F (C Func D) G) \to (F (C Full D) G \leftrightarrow \forall x \in B \forall y \in B (x H y = \emptyset \to F (x) J F (y) = \emptyset))$
71	4 5 70	syl2anc	$⊢ φ \to (F (C Full D) G \leftrightarrow \forall x \in B \forall y \in B (x H y = \emptyset \to F (x) J F (y) = \emptyset))$

Metamath Proof Explorer

Theorem fullthinc

Proof