Theorem 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={\mathrm{Base}}_C$$
	fullthinc.j	$$⊢J=\mathrm{Hom}\left(D\right)$$
	fullthinc.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
	fullthinc.d	No typesetting found for |- ( ph -> D e. ThinCat ) with typecode |-
	fullthinc.f	$$⊢\phi \to F\left(C\mathrm{Func}D\right)G$$
Assertion	fullthinc	$$⊢\phi \to \left(F\left(C\mathrm{Full}D\right)G\leftrightarrow \forall x\in B\forall y\in B\left(xHy=\varnothing \to F\left(x\right)JF\left(y\right)=\varnothing \right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		fullthinc.b	$$⊢B={\mathrm{Base}}_C$$
2		fullthinc.j	$$⊢J=\mathrm{Hom}\left(D\right)$$
3		fullthinc.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
4		fullthinc.d	Could not format ( ph -> D e. ThinCat ) : No typesetting found for |- ( ph -> D e. ThinCat ) with typecode |-
5		fullthinc.f	$$⊢\phi \to F\left(C\mathrm{Func}D\right)G$$
6	1 2 3	isfull2	$$⊢F\left(C\mathrm{Full}D\right)G\leftrightarrow \left(F\left(C\mathrm{Func}D\right)G\wedge \forall x\in B\forall y\in B\left(xGy\right):xHy\underset{onto}{⟶}F\left(x\right)JF\left(y\right)\right)$$
7		foeq2	$$⊢xHy=\varnothing \to \left(\left(xGy\right):xHy\underset{onto}{⟶}F\left(x\right)JF\left(y\right)\leftrightarrow \left(xGy\right):\varnothing \underset{onto}{⟶}F\left(x\right)JF\left(y\right)\right)$$
8		fo00	$$⊢\left(xGy\right):\varnothing \underset{onto}{⟶}F\left(x\right)JF\left(y\right)\leftrightarrow \left(xGy=\varnothing \wedge F\left(x\right)JF\left(y\right)=\varnothing \right)$$
9	8	simprbi	$$⊢\left(xGy\right):\varnothing \underset{onto}{⟶}F\left(x\right)JF\left(y\right)\to F\left(x\right)JF\left(y\right)=\varnothing$$
10	7 9	syl6bi	$$⊢xHy=\varnothing \to \left(\left(xGy\right):xHy\underset{onto}{⟶}F\left(x\right)JF\left(y\right)\to F\left(x\right)JF\left(y\right)=\varnothing \right)$$
11	10	com12	$$⊢\left(xGy\right):xHy\underset{onto}{⟶}F\left(x\right)JF\left(y\right)\to \left(xHy=\varnothing \to F\left(x\right)JF\left(y\right)=\varnothing \right)$$
12	11	2ralimi	$$⊢\forall x\in B\forall y\in B\left(xGy\right):xHy\underset{onto}{⟶}F\left(x\right)JF\left(y\right)\to \forall x\in B\forall y\in B\left(xHy=\varnothing \to F\left(x\right)JF\left(y\right)=\varnothing \right)$$
13	6 12	simplbiim	$$⊢F\left(C\mathrm{Full}D\right)G\to \forall x\in B\forall y\in B\left(xHy=\varnothing \to F\left(x\right)JF\left(y\right)=\varnothing \right)$$
14	13	adantl	Could not format ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ F ( C Full D ) G ) -> A. x e. B A. y e. B ( ( x H y ) = (/) -> ( ( F ` x ) J ( F ` y ) ) = (/) ) ) : No typesetting found for |- ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ F ( C Full D ) G ) -> A. x e. B A. y e. B ( ( x H y ) = (/) -> ( ( F ` x ) J ( F ` y ) ) = (/) ) ) with typecode |-
15		simplr	Could not format ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ A. x e. B A. y e. B ( ( x H y ) = (/) -> ( ( F ` x ) J ( F ` y ) ) = (/) ) ) -> F ( C Func D ) G ) : No typesetting found for |- ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ A. x e. B A. y e. B ( ( x H y ) = (/) -> ( ( F ` x ) J ( F ` y ) ) = (/) ) ) -> F ( C Func D ) G ) with typecode |-
16		imor	$$⊢\left(xHy=\varnothing \to F\left(x\right)JF\left(y\right)=\varnothing \right)\leftrightarrow \left(\neg xHy=\varnothing \vee F\left(x\right)JF\left(y\right)=\varnothing \right)$$
17		simplr	Could not format ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) -> F ( C Func D ) G ) : No typesetting found for |- ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) -> F ( C Func D ) G ) with typecode |-
18		simprl	Could not format ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) -> x e. B ) : No typesetting found for |- ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) -> x e. B ) with typecode |-
19		simprr	Could not format ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) -> y e. B ) : No typesetting found for |- ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) -> y e. B ) with typecode |-
20	1 3 2 17 18 19	funcf2	Could not format ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) -> ( x G y ) : ( x H y ) --> ( ( F ` x ) J ( F ` y ) ) ) : No typesetting found for |- ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) -> ( x G y ) : ( x H y ) --> ( ( F ` x ) J ( F ` y ) ) ) with typecode |-
21	20	adantr	Could not format ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ -. ( x H y ) = (/) ) -> ( x G y ) : ( x H y ) --> ( ( F ` x ) J ( F ` y ) ) ) : No typesetting found for |- ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ -. ( x H y ) = (/) ) -> ( x G y ) : ( x H y ) --> ( ( F ` x ) J ( F ` y ) ) ) with typecode |-
22		simpr	Could not format ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ -. ( x H y ) = (/) ) -> -. ( x H y ) = (/) ) : No typesetting found for |- ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ -. ( x H y ) = (/) ) -> -. ( x H y ) = (/) ) with typecode |-
23	22	neqned	Could not format ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ -. ( x H y ) = (/) ) -> ( x H y ) =/= (/) ) : No typesetting found for |- ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ -. ( x H y ) = (/) ) -> ( x H y ) =/= (/) ) with typecode |-
24		fdomne0	$$⊢\left(\left(xGy\right):xHy⟶F\left(x\right)JF\left(y\right)\wedge xHy\ne \varnothing \right)\to \left(xGy\ne \varnothing \wedge F\left(x\right)JF\left(y\right)\ne \varnothing \right)$$
25	21 23 24	syl2anc	Could not format ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ -. ( x H y ) = (/) ) -> ( ( x G y ) =/= (/) /\ ( ( F ` x ) J ( F ` y ) ) =/= (/) ) ) : No typesetting found for |- ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ -. ( x H y ) = (/) ) -> ( ( x G y ) =/= (/) /\ ( ( F ` x ) J ( F ` y ) ) =/= (/) ) ) with typecode |-
26	25	simprd	Could not format ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ -. ( x H y ) = (/) ) -> ( ( F ` x ) J ( F ` y ) ) =/= (/) ) : No typesetting found for |- ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ -. ( x H y ) = (/) ) -> ( ( F ` x ) J ( F ` y ) ) =/= (/) ) with typecode |-
27		simplll	Could not format ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ -. ( x H y ) = (/) ) -> D e. ThinCat ) : No typesetting found for |- ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ -. ( x H y ) = (/) ) -> D e. ThinCat ) with typecode |-
28		eqid	$$⊢{\mathrm{Base}}_D={\mathrm{Base}}_D$$
29	17	adantr	Could not format ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ -. ( x H y ) = (/) ) -> F ( C Func D ) G ) : No typesetting found for |- ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ -. ( x H y ) = (/) ) -> F ( C Func D ) G ) with typecode |-
30	1 28 29	funcf1	Could not format ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ -. ( x H y ) = (/) ) -> F : B --> ( Base ` D ) ) : No typesetting found for |- ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ -. ( x H y ) = (/) ) -> F : B --> ( Base ` D ) ) with typecode |-
31	18	adantr	Could not format ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ -. ( x H y ) = (/) ) -> x e. B ) : No typesetting found for |- ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ -. ( x H y ) = (/) ) -> x e. B ) with typecode |-
32	30 31	ffvelcdmd	Could not format ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ -. ( x H y ) = (/) ) -> ( F ` x ) e. ( Base ` D ) ) : No typesetting found for |- ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ -. ( x H y ) = (/) ) -> ( F ` x ) e. ( Base ` D ) ) with typecode |-
33	19	adantr	Could not format ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ -. ( x H y ) = (/) ) -> y e. B ) : No typesetting found for |- ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ -. ( x H y ) = (/) ) -> y e. B ) with typecode |-
34	30 33	ffvelcdmd	Could not format ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ -. ( x H y ) = (/) ) -> ( F ` y ) e. ( Base ` D ) ) : No typesetting found for |- ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ -. ( x H y ) = (/) ) -> ( F ` y ) e. ( Base ` D ) ) with typecode |-
35		eqidd	Could not format ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ -. ( x H y ) = (/) ) -> ( Base ` D ) = ( Base ` D ) ) : No typesetting found for |- ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ -. ( x H y ) = (/) ) -> ( Base ` D ) = ( Base ` D ) ) with typecode |-
36	2	a1i	Could not format ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ -. ( x H y ) = (/) ) -> J = ( Hom ` D ) ) : No typesetting found for |- ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ -. ( x H y ) = (/) ) -> J = ( Hom ` D ) ) with typecode |-
37	27 32 34 35 36	thincn0eu	Could not format ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ -. ( x H y ) = (/) ) -> ( ( ( F ` x ) J ( F ` y ) ) =/= (/) <-> E! f f e. ( ( F ` x ) J ( F ` y ) ) ) ) : No typesetting found for |- ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ -. ( x H y ) = (/) ) -> ( ( ( F ` x ) J ( F ` y ) ) =/= (/) <-> E! f f e. ( ( F ` x ) J ( F ` y ) ) ) ) with typecode |-
38	26 37	mpbid	Could not format ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ -. ( x H y ) = (/) ) -> E! f f e. ( ( F ` x ) J ( F ` y ) ) ) : No typesetting found for |- ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ -. ( x H y ) = (/) ) -> E! f f e. ( ( F ` x ) J ( F ` y ) ) ) with typecode |-
39		eusn	$$⊢\exists !ff\in \left(F\left(x\right)JF\left(y\right)\right)\leftrightarrow \exists fF\left(x\right)JF\left(y\right)=\left\{f\right\}$$
40	38 39	sylib	Could not format ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ -. ( x H y ) = (/) ) -> E. f ( ( F ` x ) J ( F ` y ) ) = { f } ) : No typesetting found for |- ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ -. ( x H y ) = (/) ) -> E. f ( ( F ` x ) J ( F ` y ) ) = { f } ) with typecode |-
41	25	simpld	Could not format ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ -. ( x H y ) = (/) ) -> ( x G y ) =/= (/) ) : No typesetting found for |- ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ -. ( x H y ) = (/) ) -> ( x G y ) =/= (/) ) with typecode |-
42		foconst	$$⊢\left(\left(xGy\right):xHy⟶\left\{f\right\}\wedge xGy\ne \varnothing \right)\to \left(xGy\right):xHy\underset{onto}{⟶}\left\{f\right\}$$
43		feq3	$$⊢F\left(x\right)JF\left(y\right)=\left\{f\right\}\to \left(\left(xGy\right):xHy⟶F\left(x\right)JF\left(y\right)\leftrightarrow \left(xGy\right):xHy⟶\left\{f\right\}\right)$$
44	43	anbi1d	$$⊢F\left(x\right)JF\left(y\right)=\left\{f\right\}\to \left(\left(\left(xGy\right):xHy⟶F\left(x\right)JF\left(y\right)\wedge xGy\ne \varnothing \right)\leftrightarrow \left(\left(xGy\right):xHy⟶\left\{f\right\}\wedge xGy\ne \varnothing \right)\right)$$
45		foeq3	$$⊢F\left(x\right)JF\left(y\right)=\left\{f\right\}\to \left(\left(xGy\right):xHy\underset{onto}{⟶}F\left(x\right)JF\left(y\right)\leftrightarrow \left(xGy\right):xHy\underset{onto}{⟶}\left\{f\right\}\right)$$
46	44 45	imbi12d	$$⊢F\left(x\right)JF\left(y\right)=\left\{f\right\}\to \left(\left(\left(\left(xGy\right):xHy⟶F\left(x\right)JF\left(y\right)\wedge xGy\ne \varnothing \right)\to \left(xGy\right):xHy\underset{onto}{⟶}F\left(x\right)JF\left(y\right)\right)\leftrightarrow \left(\left(\left(xGy\right):xHy⟶\left\{f\right\}\wedge xGy\ne \varnothing \right)\to \left(xGy\right):xHy\underset{onto}{⟶}\left\{f\right\}\right)\right)$$
47	42 46	mpbiri	$$⊢F\left(x\right)JF\left(y\right)=\left\{f\right\}\to \left(\left(\left(xGy\right):xHy⟶F\left(x\right)JF\left(y\right)\wedge xGy\ne \varnothing \right)\to \left(xGy\right):xHy\underset{onto}{⟶}F\left(x\right)JF\left(y\right)\right)$$
48	47	exlimiv	$$⊢\exists fF\left(x\right)JF\left(y\right)=\left\{f\right\}\to \left(\left(\left(xGy\right):xHy⟶F\left(x\right)JF\left(y\right)\wedge xGy\ne \varnothing \right)\to \left(xGy\right):xHy\underset{onto}{⟶}F\left(x\right)JF\left(y\right)\right)$$
49	48	imp	$$⊢\left(\exists fF\left(x\right)JF\left(y\right)=\left\{f\right\}\wedge \left(\left(xGy\right):xHy⟶F\left(x\right)JF\left(y\right)\wedge xGy\ne \varnothing \right)\right)\to \left(xGy\right):xHy\underset{onto}{⟶}F\left(x\right)JF\left(y\right)$$
50	40 21 41 49	syl12anc	Could not format ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ -. ( x H y ) = (/) ) -> ( x G y ) : ( x H y ) -onto-> ( ( F ` x ) J ( F ` y ) ) ) : No typesetting found for |- ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ -. ( x H y ) = (/) ) -> ( x G y ) : ( x H y ) -onto-> ( ( F ` x ) J ( F ` y ) ) ) with typecode |-
51	20	adantr	Could not format ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ ( ( F ` x ) J ( F ` y ) ) = (/) ) -> ( x G y ) : ( x H y ) --> ( ( F ` x ) J ( F ` y ) ) ) : No typesetting found for |- ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ ( ( F ` x ) J ( F ` y ) ) = (/) ) -> ( x G y ) : ( x H y ) --> ( ( F ` x ) J ( F ` y ) ) ) with typecode |-
52		feq3	$$⊢F\left(x\right)JF\left(y\right)=\varnothing \to \left(\left(xGy\right):xHy⟶F\left(x\right)JF\left(y\right)\leftrightarrow \left(xGy\right):xHy⟶\varnothing \right)$$
53	52	adantl	Could not format ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ ( ( F ` x ) J ( F ` y ) ) = (/) ) -> ( ( x G y ) : ( x H y ) --> ( ( F ` x ) J ( F ` y ) ) <-> ( x G y ) : ( x H y ) --> (/) ) ) : No typesetting found for |- ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ ( ( F ` x ) J ( F ` y ) ) = (/) ) -> ( ( x G y ) : ( x H y ) --> ( ( F ` x ) J ( F ` y ) ) <-> ( x G y ) : ( x H y ) --> (/) ) ) with typecode |-
54	51 53	mpbid	Could not format ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ ( ( F ` x ) J ( F ` y ) ) = (/) ) -> ( x G y ) : ( x H y ) --> (/) ) : No typesetting found for |- ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ ( ( F ` x ) J ( F ` y ) ) = (/) ) -> ( x G y ) : ( x H y ) --> (/) ) with typecode |-
55		f00	$$⊢\left(xGy\right):xHy⟶\varnothing \leftrightarrow \left(xGy=\varnothing \wedge xHy=\varnothing \right)$$
56	54 55	sylib	Could not format ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ ( ( F ` x ) J ( F ` y ) ) = (/) ) -> ( ( x G y ) = (/) /\ ( x H y ) = (/) ) ) : No typesetting found for |- ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ ( ( F ` x ) J ( F ` y ) ) = (/) ) -> ( ( x G y ) = (/) /\ ( x H y ) = (/) ) ) with typecode |-
57	56	simprd	Could not format ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ ( ( F ` x ) J ( F ` y ) ) = (/) ) -> ( x H y ) = (/) ) : No typesetting found for |- ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ ( ( F ` x ) J ( F ` y ) ) = (/) ) -> ( x H y ) = (/) ) with typecode |-
58	56	simpld	Could not format ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ ( ( F ` x ) J ( F ` y ) ) = (/) ) -> ( x G y ) = (/) ) : No typesetting found for |- ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ ( ( F ` x ) J ( F ` y ) ) = (/) ) -> ( x G y ) = (/) ) with typecode |-
59		simpr	Could not format ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ ( ( F ` x ) J ( F ` y ) ) = (/) ) -> ( ( F ` x ) J ( F ` y ) ) = (/) ) : No typesetting found for |- ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ ( ( F ` x ) J ( F ` y ) ) = (/) ) -> ( ( F ` x ) J ( F ` y ) ) = (/) ) with typecode |-
60	8	biimpri	$$⊢\left(xGy=\varnothing \wedge F\left(x\right)JF\left(y\right)=\varnothing \right)\to \left(xGy\right):\varnothing \underset{onto}{⟶}F\left(x\right)JF\left(y\right)$$
61	60 7	imbitrrid	$$⊢xHy=\varnothing \to \left(\left(xGy=\varnothing \wedge F\left(x\right)JF\left(y\right)=\varnothing \right)\to \left(xGy\right):xHy\underset{onto}{⟶}F\left(x\right)JF\left(y\right)\right)$$
62	61	imp	$$⊢\left(xHy=\varnothing \wedge \left(xGy=\varnothing \wedge F\left(x\right)JF\left(y\right)=\varnothing \right)\right)\to \left(xGy\right):xHy\underset{onto}{⟶}F\left(x\right)JF\left(y\right)$$
63	57 58 59 62	syl12anc	Could not format ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ ( ( F ` x ) J ( F ` y ) ) = (/) ) -> ( x G y ) : ( x H y ) -onto-> ( ( F ` x ) J ( F ` y ) ) ) : No typesetting found for |- ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ ( ( F ` x ) J ( F ` y ) ) = (/) ) -> ( x G y ) : ( x H y ) -onto-> ( ( F ` x ) J ( F ` y ) ) ) with typecode |-
64	50 63	jaodan	Could not format ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ ( -. ( x H y ) = (/) \/ ( ( F ` x ) J ( F ` y ) ) = (/) ) ) -> ( x G y ) : ( x H y ) -onto-> ( ( F ` x ) J ( F ` y ) ) ) : No typesetting found for |- ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ ( -. ( x H y ) = (/) \/ ( ( F ` x ) J ( F ` y ) ) = (/) ) ) -> ( x G y ) : ( x H y ) -onto-> ( ( F ` x ) J ( F ` y ) ) ) with typecode |-
65	16 64	sylan2b	Could not format ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ ( ( x H y ) = (/) -> ( ( F ` x ) J ( F ` y ) ) = (/) ) ) -> ( x G y ) : ( x H y ) -onto-> ( ( F ` x ) J ( F ` y ) ) ) : No typesetting found for |- ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ ( ( x H y ) = (/) -> ( ( F ` x ) J ( F ` y ) ) = (/) ) ) -> ( x G y ) : ( x H y ) -onto-> ( ( F ` x ) J ( F ` y ) ) ) with typecode |-
66	65	ex	Could not format ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) -> ( ( ( x H y ) = (/) -> ( ( F ` x ) J ( F ` y ) ) = (/) ) -> ( x G y ) : ( x H y ) -onto-> ( ( F ` x ) J ( F ` y ) ) ) ) : No typesetting found for |- ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) -> ( ( ( x H y ) = (/) -> ( ( F ` x ) J ( F ` y ) ) = (/) ) -> ( x G y ) : ( x H y ) -onto-> ( ( F ` x ) J ( F ` y ) ) ) ) with typecode |-
67	66	ralimdvva	Could not format ( ( D e. ThinCat /\ F ( C Func D ) G ) -> ( A. x e. B A. y e. B ( ( x H y ) = (/) -> ( ( F ` x ) J ( F ` y ) ) = (/) ) -> A. x e. B A. y e. B ( x G y ) : ( x H y ) -onto-> ( ( F ` x ) J ( F ` y ) ) ) ) : No typesetting found for |- ( ( D e. ThinCat /\ F ( C Func D ) G ) -> ( A. x e. B A. y e. B ( ( x H y ) = (/) -> ( ( F ` x ) J ( F ` y ) ) = (/) ) -> A. x e. B A. y e. B ( x G y ) : ( x H y ) -onto-> ( ( F ` x ) J ( F ` y ) ) ) ) with typecode |-
68	67	imp	Could not format ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ A. x e. B A. y e. B ( ( x H y ) = (/) -> ( ( F ` x ) J ( F ` y ) ) = (/) ) ) -> A. x e. B A. y e. B ( x G y ) : ( x H y ) -onto-> ( ( F ` x ) J ( F ` y ) ) ) : No typesetting found for |- ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ A. x e. B A. y e. B ( ( x H y ) = (/) -> ( ( F ` x ) J ( F ` y ) ) = (/) ) ) -> A. x e. B A. y e. B ( x G y ) : ( x H y ) -onto-> ( ( F ` x ) J ( F ` y ) ) ) with typecode |-
69	15 68 6	sylanbrc	Could not format ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ A. x e. B A. y e. B ( ( x H y ) = (/) -> ( ( F ` x ) J ( F ` y ) ) = (/) ) ) -> F ( C Full D ) G ) : No typesetting found for |- ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ A. x e. B A. y e. B ( ( x H y ) = (/) -> ( ( F ` x ) J ( F ` y ) ) = (/) ) ) -> F ( C Full D ) G ) with typecode |-
70	14 69	impbida	Could not format ( ( D e. ThinCat /\ F ( C Func D ) G ) -> ( F ( C Full D ) G <-> A. x e. B A. y e. B ( ( x H y ) = (/) -> ( ( F ` x ) J ( F ` y ) ) = (/) ) ) ) : No typesetting found for |- ( ( D e. ThinCat /\ F ( C Func D ) G ) -> ( F ( C Full D ) G <-> A. x e. B A. y e. B ( ( x H y ) = (/) -> ( ( F ` x ) J ( F ` y ) ) = (/) ) ) ) with typecode |-
71	4 5 70	syl2anc	$$⊢\phi \to \left(F\left(C\mathrm{Full}D\right)G\leftrightarrow \forall x\in B\forall y\in B\left(xHy=\varnothing \to F\left(x\right)JF\left(y\right)=\varnothing \right)\right)$$