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

Proof

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

Metamath Proof Explorer

Theorem imasnopn

Proof