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

Metamath Proof Explorer

Theorem imasncls

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
Hypotheses imasnopn.1 
|- X = U. J
imasnopn.2 
|- Y = U. K
Assertion imasncls 
|- ( ( ( J e. Top /\ K e. Top ) /\ ( R C_ ( X X. Y ) /\ A e. X ) ) -> ( ( cls ` K ) ` ( R " { A } ) ) C_ ( ( ( cls ` ( J tX K ) ) ` R ) " { A } ) )

Proof

Step Hyp Ref Expression
1 imasnopn.1 
 |-  X = U. J
2 imasnopn.2 
 |-  Y = U. K
3 2 toptopon 
 |-  ( K e. Top <-> K e. ( TopOn ` Y ) )
4 3 biimpi 
 |-  ( K e. Top -> K e. ( TopOn ` Y ) )
5 4 ad2antlr 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( R C_ ( X X. Y ) /\ A e. X ) ) -> K e. ( TopOn ` Y ) )
6 1 toptopon 
 |-  ( J e. Top <-> J e. ( TopOn ` X ) )
7 6 biimpi 
 |-  ( J e. Top -> J e. ( TopOn ` X ) )
8 7 ad2antrr 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( R C_ ( X X. Y ) /\ A e. X ) ) -> J e. ( TopOn ` X ) )
9 simprr 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( R C_ ( X X. Y ) /\ A e. X ) ) -> A e. X )
10 5 8 9 cnmptc 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( R C_ ( X X. Y ) /\ A e. X ) ) -> ( y e. Y |-> A ) e. ( K Cn J ) )
11 5 cnmptid 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( R C_ ( X X. Y ) /\ A e. X ) ) -> ( y e. Y |-> y ) e. ( K Cn K ) )
12 5 10 11 cnmpt1t 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( R C_ ( X X. Y ) /\ A e. X ) ) -> ( y e. Y |-> <. A , y >. ) e. ( K Cn ( J tX K ) ) )
13 simprl 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( R C_ ( X X. Y ) /\ A e. X ) ) -> R C_ ( X X. Y ) )
14 1 2 txuni 
 |-  ( ( J e. Top /\ K e. Top ) -> ( X X. Y ) = U. ( J tX K ) )
15 14 adantr 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( R C_ ( X X. Y ) /\ A e. X ) ) -> ( X X. Y ) = U. ( J tX K ) )
16 13 15 sseqtrd 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( R C_ ( X X. Y ) /\ A e. X ) ) -> R C_ U. ( J tX K ) )
17 eqid 
 |-  U. ( J tX K ) = U. ( J tX K )
18 17 cncls2i 
 |-  ( ( ( y e. Y |-> <. A , y >. ) e. ( K Cn ( J tX K ) ) /\ R C_ U. ( J tX K ) ) -> ( ( cls ` K ) ` ( `' ( y e. Y |-> <. A , y >. ) " R ) ) C_ ( `' ( y e. Y |-> <. A , y >. ) " ( ( cls ` ( J tX K ) ) ` R ) ) )
19 12 16 18 syl2anc 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( R C_ ( X X. Y ) /\ A e. X ) ) -> ( ( cls ` K ) ` ( `' ( y e. Y |-> <. A , y >. ) " R ) ) C_ ( `' ( y e. Y |-> <. A , y >. ) " ( ( cls ` ( J tX K ) ) ` R ) ) )
20 nfv 
 |-  F/ y ( ( J e. Top /\ K e. Top ) /\ ( R C_ ( X X. Y ) /\ A e. X ) )
21 nfcv 
 |-  F/_ y ( R " { A } )
22 nfrab1 
 |-  F/_ y { y e. Y | <. A , y >. e. R }
23 imass1 
 |-  ( R C_ ( X X. Y ) -> ( R " { A } ) C_ ( ( X X. Y ) " { A } ) )
24 13 23 syl 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( R C_ ( X X. Y ) /\ A e. X ) ) -> ( R " { A } ) C_ ( ( X X. Y ) " { A } ) )
25 xpimasn 
 |-  ( A e. X -> ( ( X X. Y ) " { A } ) = Y )
26 25 ad2antll 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( R C_ ( X X. Y ) /\ A e. X ) ) -> ( ( X X. Y ) " { A } ) = Y )
27 24 26 sseqtrd 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( R C_ ( X X. Y ) /\ A e. X ) ) -> ( R " { A } ) C_ Y )
28 27 sseld 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( R C_ ( X X. Y ) /\ A e. X ) ) -> ( y e. ( R " { A } ) -> y e. Y ) )
29 28 pm4.71rd 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( R C_ ( X X. Y ) /\ A e. X ) ) -> ( y e. ( R " { A } ) <-> ( y e. Y /\ y e. ( R " { A } ) ) ) )
30 elimasng 
 |-  ( ( A e. X /\ y e. _V ) -> ( y e. ( R " { A } ) <-> <. A , y >. e. R ) )
31 30 elvd 
 |-  ( A e. X -> ( y e. ( R " { A } ) <-> <. A , y >. e. R ) )
32 31 ad2antll 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( R C_ ( X X. Y ) /\ A e. X ) ) -> ( y e. ( R " { A } ) <-> <. A , y >. e. R ) )
33 32 anbi2d 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( R C_ ( X X. Y ) /\ A e. X ) ) -> ( ( y e. Y /\ y e. ( R " { A } ) ) <-> ( y e. Y /\ <. A , y >. e. R ) ) )
34 29 33 bitrd 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( R C_ ( X X. Y ) /\ A e. X ) ) -> ( y e. ( R " { A } ) <-> ( y e. Y /\ <. A , y >. e. R ) ) )
35 rabid 
 |-  ( y e. { y e. Y | <. A , y >. e. R } <-> ( y e. Y /\ <. A , y >. e. R ) )
36 34 35 bitr4di 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( R C_ ( X X. Y ) /\ A e. X ) ) -> ( y e. ( R " { A } ) <-> y e. { y e. Y | <. A , y >. e. R } ) )
37 20 21 22 36 eqrd 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( R C_ ( X X. Y ) /\ A e. X ) ) -> ( R " { A } ) = { y e. Y | <. A , y >. e. R } )
38 eqid 
 |-  ( y e. Y |-> <. A , y >. ) = ( y e. Y |-> <. A , y >. )
39 38 mptpreima 
 |-  ( `' ( y e. Y |-> <. A , y >. ) " R ) = { y e. Y | <. A , y >. e. R }
40 37 39 eqtr4di 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( R C_ ( X X. Y ) /\ A e. X ) ) -> ( R " { A } ) = ( `' ( y e. Y |-> <. A , y >. ) " R ) )
41 40 fveq2d 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( R C_ ( X X. Y ) /\ A e. X ) ) -> ( ( cls ` K ) ` ( R " { A } ) ) = ( ( cls ` K ) ` ( `' ( y e. Y |-> <. A , y >. ) " R ) ) )
42 nfcv 
 |-  F/_ y ( ( ( cls ` ( J tX K ) ) ` R ) " { A } )
43 nfrab1 
 |-  F/_ y { y e. Y | <. A , y >. e. ( ( cls ` ( J tX K ) ) ` R ) }
44 txtop 
 |-  ( ( J e. Top /\ K e. Top ) -> ( J tX K ) e. Top )
45 44 adantr 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( R C_ ( X X. Y ) /\ A e. X ) ) -> ( J tX K ) e. Top )
46 17 clsss3 
 |-  ( ( ( J tX K ) e. Top /\ R C_ U. ( J tX K ) ) -> ( ( cls ` ( J tX K ) ) ` R ) C_ U. ( J tX K ) )
47 45 16 46 syl2anc 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( R C_ ( X X. Y ) /\ A e. X ) ) -> ( ( cls ` ( J tX K ) ) ` R ) C_ U. ( J tX K ) )
48 47 15 sseqtrrd 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( R C_ ( X X. Y ) /\ A e. X ) ) -> ( ( cls ` ( J tX K ) ) ` R ) C_ ( X X. Y ) )
49 imass1 
 |-  ( ( ( cls ` ( J tX K ) ) ` R ) C_ ( X X. Y ) -> ( ( ( cls ` ( J tX K ) ) ` R ) " { A } ) C_ ( ( X X. Y ) " { A } ) )
50 48 49 syl 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( R C_ ( X X. Y ) /\ A e. X ) ) -> ( ( ( cls ` ( J tX K ) ) ` R ) " { A } ) C_ ( ( X X. Y ) " { A } ) )
51 50 26 sseqtrd 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( R C_ ( X X. Y ) /\ A e. X ) ) -> ( ( ( cls ` ( J tX K ) ) ` R ) " { A } ) C_ Y )
52 51 sseld 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( R C_ ( X X. Y ) /\ A e. X ) ) -> ( y e. ( ( ( cls ` ( J tX K ) ) ` R ) " { A } ) -> y e. Y ) )
53 52 pm4.71rd 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( R C_ ( X X. Y ) /\ A e. X ) ) -> ( y e. ( ( ( cls ` ( J tX K ) ) ` R ) " { A } ) <-> ( y e. Y /\ y e. ( ( ( cls ` ( J tX K ) ) ` R ) " { A } ) ) ) )
54 elimasng 
 |-  ( ( A e. X /\ y e. _V ) -> ( y e. ( ( ( cls ` ( J tX K ) ) ` R ) " { A } ) <-> <. A , y >. e. ( ( cls ` ( J tX K ) ) ` R ) ) )
55 54 elvd 
 |-  ( A e. X -> ( y e. ( ( ( cls ` ( J tX K ) ) ` R ) " { A } ) <-> <. A , y >. e. ( ( cls ` ( J tX K ) ) ` R ) ) )
56 55 ad2antll 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( R C_ ( X X. Y ) /\ A e. X ) ) -> ( y e. ( ( ( cls ` ( J tX K ) ) ` R ) " { A } ) <-> <. A , y >. e. ( ( cls ` ( J tX K ) ) ` R ) ) )
57 56 anbi2d 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( R C_ ( X X. Y ) /\ A e. X ) ) -> ( ( y e. Y /\ y e. ( ( ( cls ` ( J tX K ) ) ` R ) " { A } ) ) <-> ( y e. Y /\ <. A , y >. e. ( ( cls ` ( J tX K ) ) ` R ) ) ) )
58 53 57 bitrd 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( R C_ ( X X. Y ) /\ A e. X ) ) -> ( y e. ( ( ( cls ` ( J tX K ) ) ` R ) " { A } ) <-> ( y e. Y /\ <. A , y >. e. ( ( cls ` ( J tX K ) ) ` R ) ) ) )
59 rabid 
 |-  ( y e. { y e. Y | <. A , y >. e. ( ( cls ` ( J tX K ) ) ` R ) } <-> ( y e. Y /\ <. A , y >. e. ( ( cls ` ( J tX K ) ) ` R ) ) )
60 58 59 bitr4di 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( R C_ ( X X. Y ) /\ A e. X ) ) -> ( y e. ( ( ( cls ` ( J tX K ) ) ` R ) " { A } ) <-> y e. { y e. Y | <. A , y >. e. ( ( cls ` ( J tX K ) ) ` R ) } ) )
61 20 42 43 60 eqrd 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( R C_ ( X X. Y ) /\ A e. X ) ) -> ( ( ( cls ` ( J tX K ) ) ` R ) " { A } ) = { y e. Y | <. A , y >. e. ( ( cls ` ( J tX K ) ) ` R ) } )
62 38 mptpreima 
 |-  ( `' ( y e. Y |-> <. A , y >. ) " ( ( cls ` ( J tX K ) ) ` R ) ) = { y e. Y | <. A , y >. e. ( ( cls ` ( J tX K ) ) ` R ) }
63 61 62 eqtr4di 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( R C_ ( X X. Y ) /\ A e. X ) ) -> ( ( ( cls ` ( J tX K ) ) ` R ) " { A } ) = ( `' ( y e. Y |-> <. A , y >. ) " ( ( cls ` ( J tX K ) ) ` R ) ) )
64 19 41 63 3sstr4d 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( R C_ ( X X. Y ) /\ A e. X ) ) -> ( ( cls ` K ) ` ( R " { A } ) ) C_ ( ( ( cls ` ( J tX K ) ) ` R ) " { A } ) )