Metamath Proof Explorer

Theorem imasnopn

Description: If a relation graph is open, then an image set of a singleton is also open. 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 imasnopn 
|- ( ( ( J e. Top /\ K e. Top ) /\ ( R e. ( J tX K ) /\ A e. X ) ) -> ( R " { A } ) e. K )

Proof

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