Metamath Proof Explorer

Theorem imasubc

Description: An image of a full functor is a full subcategory. Remark 4.2(3) of Adamek p. 48. (Contributed by Zhi Wang, 7-Nov-2025)

Ref Expression
Hypotheses imasubc.s ⊢ 𝑆 = ( 𝐹 “ 𝐴 )
imasubc.h ⊢ 𝐻 = ( Hom ‘ 𝐷 )
imasubc.k ⊢ 𝐾 = ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑆 ↦ ∪ 𝑝 ∈ ( ( ◡ 𝐹 “ { 𝑥 } ) × ( ◡ 𝐹 “ { 𝑦 } ) ) ( ( 𝐺 ‘ 𝑝 ) “ ( 𝐻 ‘ 𝑝 ) ) )
imasubc.f ⊢ ( 𝜑 → 𝐹 ( 𝐷 Full 𝐸 ) 𝐺 )
imasubc.c ⊢ 𝐶 = ( Base ‘ 𝐸 )
imasubc.j ⊢ 𝐽 = ( Homf ‘ 𝐸 )
Assertion imasubc ( 𝜑 → ( 𝐾 Fn ( 𝑆 × 𝑆 ) ∧ 𝑆 ⊆ 𝐶 ∧ ( 𝐽 ↾ ( 𝑆 × 𝑆 ) ) = 𝐾 ) )

Proof

Step Hyp Ref Expression
1 imasubc.s ⊢ 𝑆 = ( 𝐹 “ 𝐴 )
2 imasubc.h ⊢ 𝐻 = ( Hom ‘ 𝐷 )
3 imasubc.k ⊢ 𝐾 = ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑆 ↦ ∪ 𝑝 ∈ ( ( ◡ 𝐹 “ { 𝑥 } ) × ( ◡ 𝐹 “ { 𝑦 } ) ) ( ( 𝐺 ‘ 𝑝 ) “ ( 𝐻 ‘ 𝑝 ) ) )
4 imasubc.f ⊢ ( 𝜑 → 𝐹 ( 𝐷 Full 𝐸 ) 𝐺 )
5 imasubc.c ⊢ 𝐶 = ( Base ‘ 𝐸 )
6 imasubc.j ⊢ 𝐽 = ( Homf ‘ 𝐸 )
7 relfull ⊢ Rel ( 𝐷 Full 𝐸 )
8 7 brrelex1i ⊢ ( 𝐹 ( 𝐷 Full 𝐸 ) 𝐺 → 𝐹 ∈ V )
9 4 8 syl ⊢ ( 𝜑 → 𝐹 ∈ V )
10 9 9 3 imasubclem2 ⊢ ( 𝜑 → 𝐾 Fn ( 𝑆 × 𝑆 ) )
11 eqid ⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
12 fullfunc ⊢ ( 𝐷 Full 𝐸 ) ⊆ ( 𝐷 Func 𝐸 )
13 12 ssbri ⊢ ( 𝐹 ( 𝐷 Full 𝐸 ) 𝐺 → 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 )
14 4 13 syl ⊢ ( 𝜑 → 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 )
15 11 5 14 funcf1 ⊢ ( 𝜑 → 𝐹 : ( Base ‘ 𝐷 ) ⟶ 𝐶 )
16 15 fimassd ⊢ ( 𝜑 → ( 𝐹 “ 𝐴 ) ⊆ 𝐶 )
17 1 16 eqsstrid ⊢ ( 𝜑 → 𝑆 ⊆ 𝐶 )
18 simprl ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) → 𝑧 ∈ 𝑆 )
19 18 1 eleqtrdi ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) → 𝑧 ∈ ( 𝐹 “ 𝐴 ) )
20 inisegn0a ⊢ ( 𝑧 ∈ ( 𝐹 “ 𝐴 ) → ( ◡ 𝐹 “ { 𝑧 } ) ≠ ∅ )
21 19 20 syl ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) → ( ◡ 𝐹 “ { 𝑧 } ) ≠ ∅ )
22 simprr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) → 𝑤 ∈ 𝑆 )
23 22 1 eleqtrdi ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) → 𝑤 ∈ ( 𝐹 “ 𝐴 ) )
24 inisegn0a ⊢ ( 𝑤 ∈ ( 𝐹 “ 𝐴 ) → ( ◡ 𝐹 “ { 𝑤 } ) ≠ ∅ )
25 23 24 syl ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) → ( ◡ 𝐹 “ { 𝑤 } ) ≠ ∅ )
26 21 25 jca ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) → ( ( ◡ 𝐹 “ { 𝑧 } ) ≠ ∅ ∧ ( ◡ 𝐹 “ { 𝑤 } ) ≠ ∅ ) )
27 xpnz ⊢ ( ( ( ◡ 𝐹 “ { 𝑧 } ) ≠ ∅ ∧ ( ◡ 𝐹 “ { 𝑤 } ) ≠ ∅ ) ↔ ( ( ◡ 𝐹 “ { 𝑧 } ) × ( ◡ 𝐹 “ { 𝑤 } ) ) ≠ ∅ )
28 26 27 sylib ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) → ( ( ◡ 𝐹 “ { 𝑧 } ) × ( ◡ 𝐹 “ { 𝑤 } ) ) ≠ ∅ )
29 15 ffnd ⊢ ( 𝜑 → 𝐹 Fn ( Base ‘ 𝐷 ) )
30 29 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) ∧ ( 𝑚 ∈ ( ◡ 𝐹 “ { 𝑧 } ) ∧ 𝑛 ∈ ( ◡ 𝐹 “ { 𝑤 } ) ) ) → 𝐹 Fn ( Base ‘ 𝐷 ) )
31 simprl ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) ∧ ( 𝑚 ∈ ( ◡ 𝐹 “ { 𝑧 } ) ∧ 𝑛 ∈ ( ◡ 𝐹 “ { 𝑤 } ) ) ) → 𝑚 ∈ ( ◡ 𝐹 “ { 𝑧 } ) )
32 fniniseg ⊢ ( 𝐹 Fn ( Base ‘ 𝐷 ) → ( 𝑚 ∈ ( ◡ 𝐹 “ { 𝑧 } ) ↔ ( 𝑚 ∈ ( Base ‘ 𝐷 ) ∧ ( 𝐹 ‘ 𝑚 ) = 𝑧 ) ) )
33 32 biimpa ⊢ ( ( 𝐹 Fn ( Base ‘ 𝐷 ) ∧ 𝑚 ∈ ( ◡ 𝐹 “ { 𝑧 } ) ) → ( 𝑚 ∈ ( Base ‘ 𝐷 ) ∧ ( 𝐹 ‘ 𝑚 ) = 𝑧 ) )
34 30 31 33 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) ∧ ( 𝑚 ∈ ( ◡ 𝐹 “ { 𝑧 } ) ∧ 𝑛 ∈ ( ◡ 𝐹 “ { 𝑤 } ) ) ) → ( 𝑚 ∈ ( Base ‘ 𝐷 ) ∧ ( 𝐹 ‘ 𝑚 ) = 𝑧 ) )
35 34 simprd ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) ∧ ( 𝑚 ∈ ( ◡ 𝐹 “ { 𝑧 } ) ∧ 𝑛 ∈ ( ◡ 𝐹 “ { 𝑤 } ) ) ) → ( 𝐹 ‘ 𝑚 ) = 𝑧 )
36 simprr ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) ∧ ( 𝑚 ∈ ( ◡ 𝐹 “ { 𝑧 } ) ∧ 𝑛 ∈ ( ◡ 𝐹 “ { 𝑤 } ) ) ) → 𝑛 ∈ ( ◡ 𝐹 “ { 𝑤 } ) )
37 fniniseg ⊢ ( 𝐹 Fn ( Base ‘ 𝐷 ) → ( 𝑛 ∈ ( ◡ 𝐹 “ { 𝑤 } ) ↔ ( 𝑛 ∈ ( Base ‘ 𝐷 ) ∧ ( 𝐹 ‘ 𝑛 ) = 𝑤 ) ) )
38 37 biimpa ⊢ ( ( 𝐹 Fn ( Base ‘ 𝐷 ) ∧ 𝑛 ∈ ( ◡ 𝐹 “ { 𝑤 } ) ) → ( 𝑛 ∈ ( Base ‘ 𝐷 ) ∧ ( 𝐹 ‘ 𝑛 ) = 𝑤 ) )
39 30 36 38 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) ∧ ( 𝑚 ∈ ( ◡ 𝐹 “ { 𝑧 } ) ∧ 𝑛 ∈ ( ◡ 𝐹 “ { 𝑤 } ) ) ) → ( 𝑛 ∈ ( Base ‘ 𝐷 ) ∧ ( 𝐹 ‘ 𝑛 ) = 𝑤 ) )
40 39 simprd ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) ∧ ( 𝑚 ∈ ( ◡ 𝐹 “ { 𝑧 } ) ∧ 𝑛 ∈ ( ◡ 𝐹 “ { 𝑤 } ) ) ) → ( 𝐹 ‘ 𝑛 ) = 𝑤 )
41 35 40 oveq12d ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) ∧ ( 𝑚 ∈ ( ◡ 𝐹 “ { 𝑧 } ) ∧ 𝑛 ∈ ( ◡ 𝐹 “ { 𝑤 } ) ) ) → ( ( 𝐹 ‘ 𝑚 ) ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑛 ) ) = ( 𝑧 ( Hom ‘ 𝐸 ) 𝑤 ) )
42 eqid ⊢ ( Hom ‘ 𝐸 ) = ( Hom ‘ 𝐸 )
43 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) ∧ ( 𝑚 ∈ ( ◡ 𝐹 “ { 𝑧 } ) ∧ 𝑛 ∈ ( ◡ 𝐹 “ { 𝑤 } ) ) ) → 𝐹 ( 𝐷 Full 𝐸 ) 𝐺 )
44 34 simpld ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) ∧ ( 𝑚 ∈ ( ◡ 𝐹 “ { 𝑧 } ) ∧ 𝑛 ∈ ( ◡ 𝐹 “ { 𝑤 } ) ) ) → 𝑚 ∈ ( Base ‘ 𝐷 ) )
45 39 simpld ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) ∧ ( 𝑚 ∈ ( ◡ 𝐹 “ { 𝑧 } ) ∧ 𝑛 ∈ ( ◡ 𝐹 “ { 𝑤 } ) ) ) → 𝑛 ∈ ( Base ‘ 𝐷 ) )
46 11 42 2 43 44 45 fullfo ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) ∧ ( 𝑚 ∈ ( ◡ 𝐹 “ { 𝑧 } ) ∧ 𝑛 ∈ ( ◡ 𝐹 “ { 𝑤 } ) ) ) → ( 𝑚 𝐺 𝑛 ) : ( 𝑚 𝐻 𝑛 ) –onto→ ( ( 𝐹 ‘ 𝑚 ) ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑛 ) ) )
47 foeq3 ⊢ ( ( ( 𝐹 ‘ 𝑚 ) ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑛 ) ) = ( 𝑧 ( Hom ‘ 𝐸 ) 𝑤 ) → ( ( 𝑚 𝐺 𝑛 ) : ( 𝑚 𝐻 𝑛 ) –onto→ ( ( 𝐹 ‘ 𝑚 ) ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑛 ) ) ↔ ( 𝑚 𝐺 𝑛 ) : ( 𝑚 𝐻 𝑛 ) –onto→ ( 𝑧 ( Hom ‘ 𝐸 ) 𝑤 ) ) )
48 47 biimpa ⊢ ( ( ( ( 𝐹 ‘ 𝑚 ) ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑛 ) ) = ( 𝑧 ( Hom ‘ 𝐸 ) 𝑤 ) ∧ ( 𝑚 𝐺 𝑛 ) : ( 𝑚 𝐻 𝑛 ) –onto→ ( ( 𝐹 ‘ 𝑚 ) ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑛 ) ) ) → ( 𝑚 𝐺 𝑛 ) : ( 𝑚 𝐻 𝑛 ) –onto→ ( 𝑧 ( Hom ‘ 𝐸 ) 𝑤 ) )
49 41 46 48 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) ∧ ( 𝑚 ∈ ( ◡ 𝐹 “ { 𝑧 } ) ∧ 𝑛 ∈ ( ◡ 𝐹 “ { 𝑤 } ) ) ) → ( 𝑚 𝐺 𝑛 ) : ( 𝑚 𝐻 𝑛 ) –onto→ ( 𝑧 ( Hom ‘ 𝐸 ) 𝑤 ) )
50 foima ⊢ ( ( 𝑚 𝐺 𝑛 ) : ( 𝑚 𝐻 𝑛 ) –onto→ ( 𝑧 ( Hom ‘ 𝐸 ) 𝑤 ) → ( ( 𝑚 𝐺 𝑛 ) “ ( 𝑚 𝐻 𝑛 ) ) = ( 𝑧 ( Hom ‘ 𝐸 ) 𝑤 ) )
51 49 50 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) ∧ ( 𝑚 ∈ ( ◡ 𝐹 “ { 𝑧 } ) ∧ 𝑛 ∈ ( ◡ 𝐹 “ { 𝑤 } ) ) ) → ( ( 𝑚 𝐺 𝑛 ) “ ( 𝑚 𝐻 𝑛 ) ) = ( 𝑧 ( Hom ‘ 𝐸 ) 𝑤 ) )
52 51 ralrimivva ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) → ∀ 𝑚 ∈ ( ◡ 𝐹 “ { 𝑧 } ) ∀ 𝑛 ∈ ( ◡ 𝐹 “ { 𝑤 } ) ( ( 𝑚 𝐺 𝑛 ) “ ( 𝑚 𝐻 𝑛 ) ) = ( 𝑧 ( Hom ‘ 𝐸 ) 𝑤 ) )
53 fveq2 ⊢ ( 𝑝 = ⟨ 𝑚 , 𝑛 ⟩ → ( 𝐺 ‘ 𝑝 ) = ( 𝐺 ‘ ⟨ 𝑚 , 𝑛 ⟩ ) )
54 df-ov ⊢ ( 𝑚 𝐺 𝑛 ) = ( 𝐺 ‘ ⟨ 𝑚 , 𝑛 ⟩ )
55 53 54 eqtr4di ⊢ ( 𝑝 = ⟨ 𝑚 , 𝑛 ⟩ → ( 𝐺 ‘ 𝑝 ) = ( 𝑚 𝐺 𝑛 ) )
56 fveq2 ⊢ ( 𝑝 = ⟨ 𝑚 , 𝑛 ⟩ → ( 𝐻 ‘ 𝑝 ) = ( 𝐻 ‘ ⟨ 𝑚 , 𝑛 ⟩ ) )
57 df-ov ⊢ ( 𝑚 𝐻 𝑛 ) = ( 𝐻 ‘ ⟨ 𝑚 , 𝑛 ⟩ )
58 56 57 eqtr4di ⊢ ( 𝑝 = ⟨ 𝑚 , 𝑛 ⟩ → ( 𝐻 ‘ 𝑝 ) = ( 𝑚 𝐻 𝑛 ) )
59 55 58 imaeq12d ⊢ ( 𝑝 = ⟨ 𝑚 , 𝑛 ⟩ → ( ( 𝐺 ‘ 𝑝 ) “ ( 𝐻 ‘ 𝑝 ) ) = ( ( 𝑚 𝐺 𝑛 ) “ ( 𝑚 𝐻 𝑛 ) ) )
60 59 eqeq1d ⊢ ( 𝑝 = ⟨ 𝑚 , 𝑛 ⟩ → ( ( ( 𝐺 ‘ 𝑝 ) “ ( 𝐻 ‘ 𝑝 ) ) = ( 𝑧 ( Hom ‘ 𝐸 ) 𝑤 ) ↔ ( ( 𝑚 𝐺 𝑛 ) “ ( 𝑚 𝐻 𝑛 ) ) = ( 𝑧 ( Hom ‘ 𝐸 ) 𝑤 ) ) )
61 60 ralxp ⊢ ( ∀ 𝑝 ∈ ( ( ◡ 𝐹 “ { 𝑧 } ) × ( ◡ 𝐹 “ { 𝑤 } ) ) ( ( 𝐺 ‘ 𝑝 ) “ ( 𝐻 ‘ 𝑝 ) ) = ( 𝑧 ( Hom ‘ 𝐸 ) 𝑤 ) ↔ ∀ 𝑚 ∈ ( ◡ 𝐹 “ { 𝑧 } ) ∀ 𝑛 ∈ ( ◡ 𝐹 “ { 𝑤 } ) ( ( 𝑚 𝐺 𝑛 ) “ ( 𝑚 𝐻 𝑛 ) ) = ( 𝑧 ( Hom ‘ 𝐸 ) 𝑤 ) )
62 52 61 sylibr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) → ∀ 𝑝 ∈ ( ( ◡ 𝐹 “ { 𝑧 } ) × ( ◡ 𝐹 “ { 𝑤 } ) ) ( ( 𝐺 ‘ 𝑝 ) “ ( 𝐻 ‘ 𝑝 ) ) = ( 𝑧 ( Hom ‘ 𝐸 ) 𝑤 ) )
63 iuneqconst2 ⊢ ( ( ( ( ◡ 𝐹 “ { 𝑧 } ) × ( ◡ 𝐹 “ { 𝑤 } ) ) ≠ ∅ ∧ ∀ 𝑝 ∈ ( ( ◡ 𝐹 “ { 𝑧 } ) × ( ◡ 𝐹 “ { 𝑤 } ) ) ( ( 𝐺 ‘ 𝑝 ) “ ( 𝐻 ‘ 𝑝 ) ) = ( 𝑧 ( Hom ‘ 𝐸 ) 𝑤 ) ) → ∪ 𝑝 ∈ ( ( ◡ 𝐹 “ { 𝑧 } ) × ( ◡ 𝐹 “ { 𝑤 } ) ) ( ( 𝐺 ‘ 𝑝 ) “ ( 𝐻 ‘ 𝑝 ) ) = ( 𝑧 ( Hom ‘ 𝐸 ) 𝑤 ) )
64 28 62 63 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) → ∪ 𝑝 ∈ ( ( ◡ 𝐹 “ { 𝑧 } ) × ( ◡ 𝐹 “ { 𝑤 } ) ) ( ( 𝐺 ‘ 𝑝 ) “ ( 𝐻 ‘ 𝑝 ) ) = ( 𝑧 ( Hom ‘ 𝐸 ) 𝑤 ) )
65 9 adantr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) → 𝐹 ∈ V )
66 65 65 18 22 3 imasubclem3 ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) → ( 𝑧 𝐾 𝑤 ) = ∪ 𝑝 ∈ ( ( ◡ 𝐹 “ { 𝑧 } ) × ( ◡ 𝐹 “ { 𝑤 } ) ) ( ( 𝐺 ‘ 𝑝 ) “ ( 𝐻 ‘ 𝑝 ) ) )
67 17 adantr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) → 𝑆 ⊆ 𝐶 )
68 67 18 sseldd ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) → 𝑧 ∈ 𝐶 )
69 67 22 sseldd ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) → 𝑤 ∈ 𝐶 )
70 6 5 42 68 69 homfval ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) → ( 𝑧 𝐽 𝑤 ) = ( 𝑧 ( Hom ‘ 𝐸 ) 𝑤 ) )
71 64 66 70 3eqtr4rd ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) → ( 𝑧 𝐽 𝑤 ) = ( 𝑧 𝐾 𝑤 ) )
72 71 ralrimivva ⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝑆 ∀ 𝑤 ∈ 𝑆 ( 𝑧 𝐽 𝑤 ) = ( 𝑧 𝐾 𝑤 ) )
73 fveq2 ⊢ ( 𝑞 = ⟨ 𝑧 , 𝑤 ⟩ → ( 𝐽 ‘ 𝑞 ) = ( 𝐽 ‘ ⟨ 𝑧 , 𝑤 ⟩ ) )
74 df-ov ⊢ ( 𝑧 𝐽 𝑤 ) = ( 𝐽 ‘ ⟨ 𝑧 , 𝑤 ⟩ )
75 73 74 eqtr4di ⊢ ( 𝑞 = ⟨ 𝑧 , 𝑤 ⟩ → ( 𝐽 ‘ 𝑞 ) = ( 𝑧 𝐽 𝑤 ) )
76 fveq2 ⊢ ( 𝑞 = ⟨ 𝑧 , 𝑤 ⟩ → ( 𝐾 ‘ 𝑞 ) = ( 𝐾 ‘ ⟨ 𝑧 , 𝑤 ⟩ ) )
77 df-ov ⊢ ( 𝑧 𝐾 𝑤 ) = ( 𝐾 ‘ ⟨ 𝑧 , 𝑤 ⟩ )
78 76 77 eqtr4di ⊢ ( 𝑞 = ⟨ 𝑧 , 𝑤 ⟩ → ( 𝐾 ‘ 𝑞 ) = ( 𝑧 𝐾 𝑤 ) )
79 75 78 eqeq12d ⊢ ( 𝑞 = ⟨ 𝑧 , 𝑤 ⟩ → ( ( 𝐽 ‘ 𝑞 ) = ( 𝐾 ‘ 𝑞 ) ↔ ( 𝑧 𝐽 𝑤 ) = ( 𝑧 𝐾 𝑤 ) ) )
80 79 ralxp ⊢ ( ∀ 𝑞 ∈ ( 𝑆 × 𝑆 ) ( 𝐽 ‘ 𝑞 ) = ( 𝐾 ‘ 𝑞 ) ↔ ∀ 𝑧 ∈ 𝑆 ∀ 𝑤 ∈ 𝑆 ( 𝑧 𝐽 𝑤 ) = ( 𝑧 𝐾 𝑤 ) )
81 72 80 sylibr ⊢ ( 𝜑 → ∀ 𝑞 ∈ ( 𝑆 × 𝑆 ) ( 𝐽 ‘ 𝑞 ) = ( 𝐾 ‘ 𝑞 ) )
82 6 5 homffn ⊢ 𝐽 Fn ( 𝐶 × 𝐶 )
83 82 a1i ⊢ ( 𝜑 → 𝐽 Fn ( 𝐶 × 𝐶 ) )
84 xpss12 ⊢ ( ( 𝑆 ⊆ 𝐶 ∧ 𝑆 ⊆ 𝐶 ) → ( 𝑆 × 𝑆 ) ⊆ ( 𝐶 × 𝐶 ) )
85 17 17 84 syl2anc ⊢ ( 𝜑 → ( 𝑆 × 𝑆 ) ⊆ ( 𝐶 × 𝐶 ) )
86 fvreseq1 ⊢ ( ( ( 𝐽 Fn ( 𝐶 × 𝐶 ) ∧ 𝐾 Fn ( 𝑆 × 𝑆 ) ) ∧ ( 𝑆 × 𝑆 ) ⊆ ( 𝐶 × 𝐶 ) ) → ( ( 𝐽 ↾ ( 𝑆 × 𝑆 ) ) = 𝐾 ↔ ∀ 𝑞 ∈ ( 𝑆 × 𝑆 ) ( 𝐽 ‘ 𝑞 ) = ( 𝐾 ‘ 𝑞 ) ) )
87 83 10 85 86 syl21anc ⊢ ( 𝜑 → ( ( 𝐽 ↾ ( 𝑆 × 𝑆 ) ) = 𝐾 ↔ ∀ 𝑞 ∈ ( 𝑆 × 𝑆 ) ( 𝐽 ‘ 𝑞 ) = ( 𝐾 ‘ 𝑞 ) ) )
88 81 87 mpbird ⊢ ( 𝜑 → ( 𝐽 ↾ ( 𝑆 × 𝑆 ) ) = 𝐾 )
89 10 17 88 3jca ⊢ ( 𝜑 → ( 𝐾 Fn ( 𝑆 × 𝑆 ) ∧ 𝑆 ⊆ 𝐶 ∧ ( 𝐽 ↾ ( 𝑆 × 𝑆 ) ) = 𝐾 ) )