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