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 = ⋃ J$
	Assertion	imasncld	$⊢ ((J \in Top \land K \in Top) \land (R \in Clsd (J \times_{t} K) \land A \in X)) \to R [\{A\}] \in Clsd (K)$

Proof

Step	Hyp	Ref	Expression
1		imasnopn.1	$⊢ X = ⋃ J$
2		nfv	$⊢ Ⅎ y ((J \in Top \land K \in Top) \land (R \in Clsd (J \times_{t} K) \land A \in X))$
3		nfcv	$⊢ \underline{Ⅎ} y R [\{A\}]$
4		nfrab1	$⊢ \underline{Ⅎ} y \{y \in ⋃ K \| ⟨A, y⟩ \in R\}$
5		simprl	$⊢ ((J \in Top \land K \in Top) \land (R \in Clsd (J \times_{t} K) \land A \in X)) \to R \in Clsd (J \times_{t} K)$
6		eqid	$⊢ ⋃ (J \times_{t} K) = ⋃ (J \times_{t} K)$
7	6	cldss	$⊢ R \in Clsd (J \times_{t} K) \to R \subseteq ⋃ (J \times_{t} K)$
8	5 7	syl	$⊢ ((J \in Top \land K \in Top) \land (R \in Clsd (J \times_{t} K) \land A \in X)) \to R \subseteq ⋃ (J \times_{t} K)$
9		eqid	$⊢ ⋃ K = ⋃ K$
10	1 9	txuni	$⊢ (J \in Top \land K \in Top) \to X \times ⋃ K = ⋃ (J \times_{t} K)$
11	10	adantr	$⊢ ((J \in Top \land K \in Top) \land (R \in Clsd (J \times_{t} K) \land A \in X)) \to X \times ⋃ K = ⋃ (J \times_{t} K)$
12	8 11	sseqtrrd	$⊢ ((J \in Top \land K \in Top) \land (R \in Clsd (J \times_{t} K) \land A \in X)) \to R \subseteq X \times ⋃ K$
13		imass1	$⊢ R \subseteq X \times ⋃ K \to R [\{A\}] \subseteq (X \times ⋃ K) [\{A\}]$
14	12 13	syl	$⊢ ((J \in Top \land K \in Top) \land (R \in Clsd (J \times_{t} K) \land A \in X)) \to R [\{A\}] \subseteq (X \times ⋃ K) [\{A\}]$
15		xpimasn	$⊢ A \in X \to (X \times ⋃ K) [\{A\}] = ⋃ K$
16	15	ad2antll	$⊢ ((J \in Top \land K \in Top) \land (R \in Clsd (J \times_{t} K) \land A \in X)) \to (X \times ⋃ K) [\{A\}] = ⋃ K$
17	14 16	sseqtrd	$⊢ ((J \in Top \land K \in Top) \land (R \in Clsd (J \times_{t} K) \land A \in X)) \to R [\{A\}] \subseteq ⋃ K$
18	17	sseld	$⊢ ((J \in Top \land K \in Top) \land (R \in Clsd (J \times_{t} K) \land A \in X)) \to (y \in R [\{A\}] \to y \in ⋃ K)$
19	18	pm4.71rd	$⊢ ((J \in Top \land K \in Top) \land (R \in Clsd (J \times_{t} K) \land A \in X)) \to (y \in R [\{A\}] \leftrightarrow (y \in ⋃ K \land y \in R [\{A\}]))$
20		elimasng	$⊢ (A \in X \land y \in V) \to (y \in R [\{A\}] \leftrightarrow ⟨A, y⟩ \in R)$
21	20	elvd	$⊢ A \in X \to (y \in R [\{A\}] \leftrightarrow ⟨A, y⟩ \in R)$
22	21	ad2antll	$⊢ ((J \in Top \land K \in Top) \land (R \in Clsd (J \times_{t} K) \land A \in X)) \to (y \in R [\{A\}] \leftrightarrow ⟨A, y⟩ \in R)$
23	22	anbi2d	$⊢ ((J \in Top \land K \in Top) \land (R \in Clsd (J \times_{t} K) \land A \in X)) \to ((y \in ⋃ K \land y \in R [\{A\}]) \leftrightarrow (y \in ⋃ K \land ⟨A, y⟩ \in R))$
24	19 23	bitrd	$⊢ ((J \in Top \land K \in Top) \land (R \in Clsd (J \times_{t} K) \land A \in X)) \to (y \in R [\{A\}] \leftrightarrow (y \in ⋃ K \land ⟨A, y⟩ \in R))$
25		rabid	$⊢ y \in \{y \in ⋃ K \| ⟨A, y⟩ \in R\} \leftrightarrow (y \in ⋃ K \land ⟨A, y⟩ \in R)$
26	24 25	bitr4di	$⊢ ((J \in Top \land K \in Top) \land (R \in Clsd (J \times_{t} K) \land A \in X)) \to (y \in R [\{A\}] \leftrightarrow y \in \{y \in ⋃ K \| ⟨A, y⟩ \in R\})$
27	2 3 4 26	eqrd	$⊢ ((J \in Top \land K \in Top) \land (R \in Clsd (J \times_{t} K) \land A \in X)) \to R [\{A\}] = \{y \in ⋃ K \| ⟨A, y⟩ \in R\}$
28		eqid	$⊢ (y \in ⋃ K ⟼ ⟨A, y⟩) = (y \in ⋃ K ⟼ ⟨A, y⟩)$
29	28	mptpreima	$⊢ {(y \in ⋃ K ⟼ ⟨A, y⟩)}^{-1} [R] = \{y \in ⋃ K \| ⟨A, y⟩ \in R\}$
30	27 29	eqtr4di	$⊢ ((J \in Top \land K \in Top) \land (R \in Clsd (J \times_{t} K) \land A \in X)) \to R [\{A\}] = {(y \in ⋃ K ⟼ ⟨A, y⟩)}^{-1} [R]$
31	9	toptopon	$⊢ K \in Top \leftrightarrow K \in TopOn (⋃ K)$
32	31	biimpi	$⊢ K \in Top \to K \in TopOn (⋃ K)$
33	32	ad2antlr	$⊢ ((J \in Top \land K \in Top) \land (R \in Clsd (J \times_{t} K) \land A \in X)) \to K \in TopOn (⋃ K)$
34	1	toptopon	$⊢ J \in Top \leftrightarrow J \in TopOn (X)$
35	34	biimpi	$⊢ J \in Top \to J \in TopOn (X)$
36	35	ad2antrr	$⊢ ((J \in Top \land K \in Top) \land (R \in Clsd (J \times_{t} K) \land A \in X)) \to J \in TopOn (X)$
37		simprr	$⊢ ((J \in Top \land K \in Top) \land (R \in Clsd (J \times_{t} K) \land A \in X)) \to A \in X$
38	33 36 37	cnmptc	$⊢ ((J \in Top \land K \in Top) \land (R \in Clsd (J \times_{t} K) \land A \in X)) \to (y \in ⋃ K ⟼ A) \in (K Cn J)$
39	33	cnmptid	$⊢ ((J \in Top \land K \in Top) \land (R \in Clsd (J \times_{t} K) \land A \in X)) \to (y \in ⋃ K ⟼ y) \in (K Cn K)$
40	33 38 39	cnmpt1t	$⊢ ((J \in Top \land K \in Top) \land (R \in Clsd (J \times_{t} K) \land A \in X)) \to (y \in ⋃ K ⟼ ⟨A, y⟩) \in (K Cn (J \times_{t} K))$
41		cnclima	$⊢ ((y \in ⋃ K ⟼ ⟨A, y⟩) \in (K Cn (J \times_{t} K)) \land R \in Clsd (J \times_{t} K)) \to {(y \in ⋃ K ⟼ ⟨A, y⟩)}^{-1} [R] \in Clsd (K)$
42	40 5 41	syl2anc	$⊢ ((J \in Top \land K \in Top) \land (R \in Clsd (J \times_{t} K) \land A \in X)) \to {(y \in ⋃ K ⟼ ⟨A, y⟩)}^{-1} [R] \in Clsd (K)$
43	30 42	eqeltrd	$⊢ ((J \in Top \land K \in Top) \land (R \in Clsd (J \times_{t} K) \land A \in X)) \to R [\{A\}] \in Clsd (K)$

Metamath Proof Explorer

Theorem imasncld

Proof