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 \in Top \land K \in Top) \land (R \subseteq X \times Y \land A \in X)) \to cls (K) (R [\{A\}]) \subseteq cls (J \times_{t} K) (R) [\{A\}]$

Proof

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

Metamath Proof Explorer

Theorem imasncls

Proof