Theorem cnextrel

Description: In the general case, a continuous extension is a relation. (Contributed by Thierry Arnoux, 20-Dec-2017)

	Ref	Expression
Hypotheses	cnextfrel.1	|- C = U. J
	cnextfrel.2	|- B = U. K
Assertion	cnextrel	|- ( ( ( J e. Top /\ K e. Top ) /\ ( F : A --> B /\ A C_ C ) ) -> Rel ( ( J CnExt K ) ` F ) )

Proof

Step	Hyp	Ref	Expression
1		cnextfrel.1	|- C = U. J
2		cnextfrel.2	|- B = U. K
3		relxp	|- Rel ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) )
4	3	rgenw	|- A. x e. ( ( cls ` J ) ` A ) Rel ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) )
5		reliun	|- ( Rel U_ x e. ( ( cls ` J ) ` A ) ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) <-> A. x e. ( ( cls ` J ) ` A ) Rel ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) )
6	4 5	mpbir	|- Rel U_ x e. ( ( cls ` J ) ` A ) ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) )
7	1 2	cnextfval	|- ( ( ( J e. Top /\ K e. Top ) /\ ( F : A --> B /\ A C_ C ) ) -> ( ( J CnExt K ) ` F ) = U_ x e. ( ( cls ` J ) ` A ) ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) )
8	7	releqd	|- ( ( ( J e. Top /\ K e. Top ) /\ ( F : A --> B /\ A C_ C ) ) -> ( Rel ( ( J CnExt K ) ` F ) <-> Rel U_ x e. ( ( cls ` J ) ` A ) ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) ) )
9	6 8	mpbiri	|- ( ( ( J e. Top /\ K e. Top ) /\ ( F : A --> B /\ A C_ C ) ) -> Rel ( ( J CnExt K ) ` F ) )