Metamath Proof Explorer

Theorem imasncls

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
Hypotheses imasnopn.1 ⊢ 𝑋 = ∪ 𝐽
imasnopn.2 ⊢ 𝑌 = ∪ 𝐾
Assertion imasncls ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝑅 ⊆ ( 𝑋 × 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ) → ( ( cls ‘ 𝐾 ) ‘ ( 𝑅 “ { 𝐴 } ) ) ⊆ ( ( ( cls ‘ ( 𝐽 ×t 𝐾 ) ) ‘ 𝑅 ) “ { 𝐴 } ) )

Proof

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