Metamath Proof Explorer


Theorem imasncld

Description: If a relation graph is closed, then an image set of a singleton is also closed. Corollary of Proposition 4 of BourbakiTop1 p. I.26. (Contributed by Thierry Arnoux, 14-Jan-2018)

Ref Expression
Hypothesis imasnopn.1
|- X = U. J
Assertion imasncld
|- ( ( ( J e. Top /\ K e. Top ) /\ ( R e. ( Clsd ` ( J tX K ) ) /\ A e. X ) ) -> ( R " { A } ) e. ( Clsd ` K ) )

Proof

Step Hyp Ref Expression
1 imasnopn.1
 |-  X = U. J
2 nfv
 |-  F/ y ( ( J e. Top /\ K e. Top ) /\ ( R e. ( Clsd ` ( J tX K ) ) /\ A e. X ) )
3 nfcv
 |-  F/_ y ( R " { A } )
4 nfrab1
 |-  F/_ y { y e. U. K | <. A , y >. e. R }
5 simprl
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( R e. ( Clsd ` ( J tX K ) ) /\ A e. X ) ) -> R e. ( Clsd ` ( J tX K ) ) )
6 eqid
 |-  U. ( J tX K ) = U. ( J tX K )
7 6 cldss
 |-  ( R e. ( Clsd ` ( J tX K ) ) -> R C_ U. ( J tX K ) )
8 5 7 syl
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( R e. ( Clsd ` ( J tX K ) ) /\ A e. X ) ) -> R C_ U. ( J tX K ) )
9 eqid
 |-  U. K = U. K
10 1 9 txuni
 |-  ( ( J e. Top /\ K e. Top ) -> ( X X. U. K ) = U. ( J tX K ) )
11 10 adantr
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( R e. ( Clsd ` ( J tX K ) ) /\ A e. X ) ) -> ( X X. U. K ) = U. ( J tX K ) )
12 8 11 sseqtrrd
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( R e. ( Clsd ` ( J tX K ) ) /\ A e. X ) ) -> R C_ ( X X. U. K ) )
13 imass1
 |-  ( R C_ ( X X. U. K ) -> ( R " { A } ) C_ ( ( X X. U. K ) " { A } ) )
14 12 13 syl
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( R e. ( Clsd ` ( J tX K ) ) /\ A e. X ) ) -> ( R " { A } ) C_ ( ( X X. U. K ) " { A } ) )
15 xpimasn
 |-  ( A e. X -> ( ( X X. U. K ) " { A } ) = U. K )
16 15 ad2antll
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( R e. ( Clsd ` ( J tX K ) ) /\ A e. X ) ) -> ( ( X X. U. K ) " { A } ) = U. K )
17 14 16 sseqtrd
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( R e. ( Clsd ` ( J tX K ) ) /\ A e. X ) ) -> ( R " { A } ) C_ U. K )
18 17 sseld
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( R e. ( Clsd ` ( J tX K ) ) /\ A e. X ) ) -> ( y e. ( R " { A } ) -> y e. U. K ) )
19 18 pm4.71rd
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( R e. ( Clsd ` ( J tX K ) ) /\ A e. X ) ) -> ( y e. ( R " { A } ) <-> ( y e. U. K /\ y e. ( R " { A } ) ) ) )
20 elimasng
 |-  ( ( A e. X /\ y e. _V ) -> ( y e. ( R " { A } ) <-> <. A , y >. e. R ) )
21 20 elvd
 |-  ( A e. X -> ( y e. ( R " { A } ) <-> <. A , y >. e. R ) )
22 21 ad2antll
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( R e. ( Clsd ` ( J tX K ) ) /\ A e. X ) ) -> ( y e. ( R " { A } ) <-> <. A , y >. e. R ) )
23 22 anbi2d
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( R e. ( Clsd ` ( J tX K ) ) /\ A e. X ) ) -> ( ( y e. U. K /\ y e. ( R " { A } ) ) <-> ( y e. U. K /\ <. A , y >. e. R ) ) )
24 19 23 bitrd
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( R e. ( Clsd ` ( J tX K ) ) /\ A e. X ) ) -> ( y e. ( R " { A } ) <-> ( y e. U. K /\ <. A , y >. e. R ) ) )
25 rabid
 |-  ( y e. { y e. U. K | <. A , y >. e. R } <-> ( y e. U. K /\ <. A , y >. e. R ) )
26 24 25 bitr4di
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( R e. ( Clsd ` ( J tX K ) ) /\ A e. X ) ) -> ( y e. ( R " { A } ) <-> y e. { y e. U. K | <. A , y >. e. R } ) )
27 2 3 4 26 eqrd
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( R e. ( Clsd ` ( J tX K ) ) /\ A e. X ) ) -> ( R " { A } ) = { y e. U. K | <. A , y >. e. R } )
28 eqid
 |-  ( y e. U. K |-> <. A , y >. ) = ( y e. U. K |-> <. A , y >. )
29 28 mptpreima
 |-  ( `' ( y e. U. K |-> <. A , y >. ) " R ) = { y e. U. K | <. A , y >. e. R }
30 27 29 eqtr4di
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( R e. ( Clsd ` ( J tX K ) ) /\ A e. X ) ) -> ( R " { A } ) = ( `' ( y e. U. K |-> <. A , y >. ) " R ) )
31 9 toptopon
 |-  ( K e. Top <-> K e. ( TopOn ` U. K ) )
32 31 biimpi
 |-  ( K e. Top -> K e. ( TopOn ` U. K ) )
33 32 ad2antlr
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( R e. ( Clsd ` ( J tX K ) ) /\ A e. X ) ) -> K e. ( TopOn ` U. K ) )
34 1 toptopon
 |-  ( J e. Top <-> J e. ( TopOn ` X ) )
35 34 biimpi
 |-  ( J e. Top -> J e. ( TopOn ` X ) )
36 35 ad2antrr
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( R e. ( Clsd ` ( J tX K ) ) /\ A e. X ) ) -> J e. ( TopOn ` X ) )
37 simprr
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( R e. ( Clsd ` ( J tX K ) ) /\ A e. X ) ) -> A e. X )
38 33 36 37 cnmptc
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( R e. ( Clsd ` ( J tX K ) ) /\ A e. X ) ) -> ( y e. U. K |-> A ) e. ( K Cn J ) )
39 33 cnmptid
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( R e. ( Clsd ` ( J tX K ) ) /\ A e. X ) ) -> ( y e. U. K |-> y ) e. ( K Cn K ) )
40 33 38 39 cnmpt1t
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( R e. ( Clsd ` ( J tX K ) ) /\ A e. X ) ) -> ( y e. U. K |-> <. A , y >. ) e. ( K Cn ( J tX K ) ) )
41 cnclima
 |-  ( ( ( y e. U. K |-> <. A , y >. ) e. ( K Cn ( J tX K ) ) /\ R e. ( Clsd ` ( J tX K ) ) ) -> ( `' ( y e. U. K |-> <. A , y >. ) " R ) e. ( Clsd ` K ) )
42 40 5 41 syl2anc
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( R e. ( Clsd ` ( J tX K ) ) /\ A e. X ) ) -> ( `' ( y e. U. K |-> <. A , y >. ) " R ) e. ( Clsd ` K ) )
43 30 42 eqeltrd
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( R e. ( Clsd ` ( J tX K ) ) /\ A e. X ) ) -> ( R " { A } ) e. ( Clsd ` K ) )