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 = J
imasnopn.2 Y = K
Assertion imasncls J Top K Top R X × Y A X cls K R A cls J × t K R A

Proof

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