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	⊢ 𝑋 = ∪ 𝐽
Assertion	imasnopn	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝑅 ∈ ( 𝐽 ×t 𝐾 ) ∧ 𝐴 ∈ 𝑋 ) ) → ( 𝑅 “ { 𝐴 } ) ∈ 𝐾 )

Proof

Step	Hyp	Ref	Expression
1		imasnopn.1	⊢ 𝑋 = ∪ 𝐽
2		nfv	⊢ Ⅎ 𝑦 ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝑅 ∈ ( 𝐽 ×t 𝐾 ) ∧ 𝐴 ∈ 𝑋 ) )
3		nfcv	⊢ Ⅎ 𝑦 ( 𝑅 “ { 𝐴 } )
4		nfrab1	⊢ Ⅎ 𝑦 { 𝑦 ∈ ∪ 𝐾 ∣ ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝑅 }
5		txtop	⊢ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) → ( 𝐽 ×t 𝐾 ) ∈ Top )
6	5	adantr	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝑅 ∈ ( 𝐽 ×t 𝐾 ) ∧ 𝐴 ∈ 𝑋 ) ) → ( 𝐽 ×t 𝐾 ) ∈ Top )
7		simprl	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝑅 ∈ ( 𝐽 ×t 𝐾 ) ∧ 𝐴 ∈ 𝑋 ) ) → 𝑅 ∈ ( 𝐽 ×t 𝐾 ) )
8		eqid	⊢ ∪ ( 𝐽 ×t 𝐾 ) = ∪ ( 𝐽 ×t 𝐾 )
9	8	eltopss	⊢ ( ( ( 𝐽 ×t 𝐾 ) ∈ Top ∧ 𝑅 ∈ ( 𝐽 ×t 𝐾 ) ) → 𝑅 ⊆ ∪ ( 𝐽 ×t 𝐾 ) )
10	6 7 9	syl2anc	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝑅 ∈ ( 𝐽 ×t 𝐾 ) ∧ 𝐴 ∈ 𝑋 ) ) → 𝑅 ⊆ ∪ ( 𝐽 ×t 𝐾 ) )
11		eqid	⊢ ∪ 𝐾 = ∪ 𝐾
12	1 11	txuni	⊢ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) → ( 𝑋 × ∪ 𝐾 ) = ∪ ( 𝐽 ×t 𝐾 ) )
13	12	adantr	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝑅 ∈ ( 𝐽 ×t 𝐾 ) ∧ 𝐴 ∈ 𝑋 ) ) → ( 𝑋 × ∪ 𝐾 ) = ∪ ( 𝐽 ×t 𝐾 ) )
14	10 13	sseqtrrd	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝑅 ∈ ( 𝐽 ×t 𝐾 ) ∧ 𝐴 ∈ 𝑋 ) ) → 𝑅 ⊆ ( 𝑋 × ∪ 𝐾 ) )
15		imass1	⊢ ( 𝑅 ⊆ ( 𝑋 × ∪ 𝐾 ) → ( 𝑅 “ { 𝐴 } ) ⊆ ( ( 𝑋 × ∪ 𝐾 ) “ { 𝐴 } ) )
16	14 15	syl	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝑅 ∈ ( 𝐽 ×t 𝐾 ) ∧ 𝐴 ∈ 𝑋 ) ) → ( 𝑅 “ { 𝐴 } ) ⊆ ( ( 𝑋 × ∪ 𝐾 ) “ { 𝐴 } ) )
17		xpimasn	⊢ ( 𝐴 ∈ 𝑋 → ( ( 𝑋 × ∪ 𝐾 ) “ { 𝐴 } ) = ∪ 𝐾 )
18	17	ad2antll	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝑅 ∈ ( 𝐽 ×t 𝐾 ) ∧ 𝐴 ∈ 𝑋 ) ) → ( ( 𝑋 × ∪ 𝐾 ) “ { 𝐴 } ) = ∪ 𝐾 )
19	16 18	sseqtrd	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝑅 ∈ ( 𝐽 ×t 𝐾 ) ∧ 𝐴 ∈ 𝑋 ) ) → ( 𝑅 “ { 𝐴 } ) ⊆ ∪ 𝐾 )
20	19	sseld	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝑅 ∈ ( 𝐽 ×t 𝐾 ) ∧ 𝐴 ∈ 𝑋 ) ) → ( 𝑦 ∈ ( 𝑅 “ { 𝐴 } ) → 𝑦 ∈ ∪ 𝐾 ) )
21	20	pm4.71rd	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝑅 ∈ ( 𝐽 ×t 𝐾 ) ∧ 𝐴 ∈ 𝑋 ) ) → ( 𝑦 ∈ ( 𝑅 “ { 𝐴 } ) ↔ ( 𝑦 ∈ ∪ 𝐾 ∧ 𝑦 ∈ ( 𝑅 “ { 𝐴 } ) ) ) )
22		elimasng	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ V ) → ( 𝑦 ∈ ( 𝑅 “ { 𝐴 } ) ↔ ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝑅 ) )
23	22	elvd	⊢ ( 𝐴 ∈ 𝑋 → ( 𝑦 ∈ ( 𝑅 “ { 𝐴 } ) ↔ ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝑅 ) )
24	23	ad2antll	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝑅 ∈ ( 𝐽 ×t 𝐾 ) ∧ 𝐴 ∈ 𝑋 ) ) → ( 𝑦 ∈ ( 𝑅 “ { 𝐴 } ) ↔ ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝑅 ) )
25	24	anbi2d	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝑅 ∈ ( 𝐽 ×t 𝐾 ) ∧ 𝐴 ∈ 𝑋 ) ) → ( ( 𝑦 ∈ ∪ 𝐾 ∧ 𝑦 ∈ ( 𝑅 “ { 𝐴 } ) ) ↔ ( 𝑦 ∈ ∪ 𝐾 ∧ ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝑅 ) ) )
26	21 25	bitrd	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝑅 ∈ ( 𝐽 ×t 𝐾 ) ∧ 𝐴 ∈ 𝑋 ) ) → ( 𝑦 ∈ ( 𝑅 “ { 𝐴 } ) ↔ ( 𝑦 ∈ ∪ 𝐾 ∧ ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝑅 ) ) )
27		rabid	⊢ ( 𝑦 ∈ { 𝑦 ∈ ∪ 𝐾 ∣ ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝑅 } ↔ ( 𝑦 ∈ ∪ 𝐾 ∧ ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝑅 ) )
28	26 27	bitr4di	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝑅 ∈ ( 𝐽 ×t 𝐾 ) ∧ 𝐴 ∈ 𝑋 ) ) → ( 𝑦 ∈ ( 𝑅 “ { 𝐴 } ) ↔ 𝑦 ∈ { 𝑦 ∈ ∪ 𝐾 ∣ ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝑅 } ) )
29	2 3 4 28	eqrd	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝑅 ∈ ( 𝐽 ×t 𝐾 ) ∧ 𝐴 ∈ 𝑋 ) ) → ( 𝑅 “ { 𝐴 } ) = { 𝑦 ∈ ∪ 𝐾 ∣ ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝑅 } )
30		eqid	⊢ ( 𝑦 ∈ ∪ 𝐾 ↦ ⟨ 𝐴 , 𝑦 ⟩ ) = ( 𝑦 ∈ ∪ 𝐾 ↦ ⟨ 𝐴 , 𝑦 ⟩ )
31	30	mptpreima	⊢ ( ◡ ( 𝑦 ∈ ∪ 𝐾 ↦ ⟨ 𝐴 , 𝑦 ⟩ ) “ 𝑅 ) = { 𝑦 ∈ ∪ 𝐾 ∣ ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝑅 }
32	29 31	eqtr4di	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝑅 ∈ ( 𝐽 ×t 𝐾 ) ∧ 𝐴 ∈ 𝑋 ) ) → ( 𝑅 “ { 𝐴 } ) = ( ◡ ( 𝑦 ∈ ∪ 𝐾 ↦ ⟨ 𝐴 , 𝑦 ⟩ ) “ 𝑅 ) )
33	11	toptopon	⊢ ( 𝐾 ∈ Top ↔ 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) )
34	33	biimpi	⊢ ( 𝐾 ∈ Top → 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) )
35	34	ad2antlr	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝑅 ∈ ( 𝐽 ×t 𝐾 ) ∧ 𝐴 ∈ 𝑋 ) ) → 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) )
36	1	toptopon	⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
37	36	biimpi	⊢ ( 𝐽 ∈ Top → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
38	37	ad2antrr	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝑅 ∈ ( 𝐽 ×t 𝐾 ) ∧ 𝐴 ∈ 𝑋 ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
39		simprr	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝑅 ∈ ( 𝐽 ×t 𝐾 ) ∧ 𝐴 ∈ 𝑋 ) ) → 𝐴 ∈ 𝑋 )
40	35 38 39	cnmptc	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝑅 ∈ ( 𝐽 ×t 𝐾 ) ∧ 𝐴 ∈ 𝑋 ) ) → ( 𝑦 ∈ ∪ 𝐾 ↦ 𝐴 ) ∈ ( 𝐾 Cn 𝐽 ) )
41	35	cnmptid	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝑅 ∈ ( 𝐽 ×t 𝐾 ) ∧ 𝐴 ∈ 𝑋 ) ) → ( 𝑦 ∈ ∪ 𝐾 ↦ 𝑦 ) ∈ ( 𝐾 Cn 𝐾 ) )
42	35 40 41	cnmpt1t	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝑅 ∈ ( 𝐽 ×t 𝐾 ) ∧ 𝐴 ∈ 𝑋 ) ) → ( 𝑦 ∈ ∪ 𝐾 ↦ ⟨ 𝐴 , 𝑦 ⟩ ) ∈ ( 𝐾 Cn ( 𝐽 ×t 𝐾 ) ) )
43		cnima	⊢ ( ( ( 𝑦 ∈ ∪ 𝐾 ↦ ⟨ 𝐴 , 𝑦 ⟩ ) ∈ ( 𝐾 Cn ( 𝐽 ×t 𝐾 ) ) ∧ 𝑅 ∈ ( 𝐽 ×t 𝐾 ) ) → ( ◡ ( 𝑦 ∈ ∪ 𝐾 ↦ ⟨ 𝐴 , 𝑦 ⟩ ) “ 𝑅 ) ∈ 𝐾 )
44	42 7 43	syl2anc	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝑅 ∈ ( 𝐽 ×t 𝐾 ) ∧ 𝐴 ∈ 𝑋 ) ) → ( ◡ ( 𝑦 ∈ ∪ 𝐾 ↦ ⟨ 𝐴 , 𝑦 ⟩ ) “ 𝑅 ) ∈ 𝐾 )
45	32 44	eqeltrd	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝑅 ∈ ( 𝐽 ×t 𝐾 ) ∧ 𝐴 ∈ 𝑋 ) ) → ( 𝑅 “ { 𝐴 } ) ∈ 𝐾 )