This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐾 ) ∧ 𝐴 ∈ 𝑋 ) ) → ( 𝑅 “ { 𝐴 } ) ∈ 𝐾 )