Metamath Proof Explorer

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

Proof

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