This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )