Metamath Proof Explorer

Theorem funcestrcsetclem8

Description: Lemma 8 for funcestrcsetc . (Contributed by AV, 15-Feb-2020)

Ref Expression
Hypotheses funcestrcsetc.e ⊢ 𝐸 = ( ExtStrCat ‘ 𝑈 )
funcestrcsetc.s ⊢ 𝑆 = ( SetCat ‘ 𝑈 )
funcestrcsetc.b ⊢ 𝐵 = ( Base ‘ 𝐸 )
funcestrcsetc.c ⊢ 𝐶 = ( Base ‘ 𝑆 )
funcestrcsetc.u ⊢ ( 𝜑 → 𝑈 ∈ WUni )
funcestrcsetc.f ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐵 ↦ ( Base ‘ 𝑥 ) ) )
funcestrcsetc.g ⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( I ↾ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) ) )
Assertion funcestrcsetclem8 ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 𝐺 𝑌 ) : ( 𝑋 ( Hom ‘ 𝐸 ) 𝑌 ) ⟶ ( ( 𝐹 ‘ 𝑋 ) ( Hom ‘ 𝑆 ) ( 𝐹 ‘ 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 funcestrcsetc.e ⊢ 𝐸 = ( ExtStrCat ‘ 𝑈 )
2 funcestrcsetc.s ⊢ 𝑆 = ( SetCat ‘ 𝑈 )
3 funcestrcsetc.b ⊢ 𝐵 = ( Base ‘ 𝐸 )
4 funcestrcsetc.c ⊢ 𝐶 = ( Base ‘ 𝑆 )
5 funcestrcsetc.u ⊢ ( 𝜑 → 𝑈 ∈ WUni )
6 funcestrcsetc.f ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐵 ↦ ( Base ‘ 𝑥 ) ) )
7 funcestrcsetc.g ⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( I ↾ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) ) )
8 f1oi ⊢ ( I ↾ ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ) : ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) –1-1-onto→ ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) )
9 f1of ⊢ ( ( I ↾ ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ) : ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) –1-1-onto→ ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) → ( I ↾ ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ) : ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ⟶ ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) )
10 8 9 mp1i ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( I ↾ ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ) : ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ⟶ ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) )
11 elmapi ⊢ ( 𝑓 ∈ ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) → 𝑓 : ( Base ‘ 𝑋 ) ⟶ ( Base ‘ 𝑌 ) )
12 fvex ⊢ ( Base ‘ 𝑌 ) ∈ V
13 fvex ⊢ ( Base ‘ 𝑋 ) ∈ V
14 12 13 pm3.2i ⊢ ( ( Base ‘ 𝑌 ) ∈ V ∧ ( Base ‘ 𝑋 ) ∈ V )
15 elmapg ⊢ ( ( ( Base ‘ 𝑌 ) ∈ V ∧ ( Base ‘ 𝑋 ) ∈ V ) → ( 𝑓 ∈ ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ↔ 𝑓 : ( Base ‘ 𝑋 ) ⟶ ( Base ‘ 𝑌 ) ) )
16 15 bicomd ⊢ ( ( ( Base ‘ 𝑌 ) ∈ V ∧ ( Base ‘ 𝑋 ) ∈ V ) → ( 𝑓 : ( Base ‘ 𝑋 ) ⟶ ( Base ‘ 𝑌 ) ↔ 𝑓 ∈ ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ) )
17 14 16 mp1i ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑓 : ( Base ‘ 𝑋 ) ⟶ ( Base ‘ 𝑌 ) ↔ 𝑓 ∈ ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ) )
18 17 biimpa ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑓 : ( Base ‘ 𝑋 ) ⟶ ( Base ‘ 𝑌 ) ) → 𝑓 ∈ ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) )
19 1 2 3 4 5 6 funcestrcsetclem1 ⊢ ( ( 𝜑 ∧ 𝑌 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑌 ) = ( Base ‘ 𝑌 ) )
20 19 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑌 ) = ( Base ‘ 𝑌 ) )
21 1 2 3 4 5 6 funcestrcsetclem1 ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑋 ) = ( Base ‘ 𝑋 ) )
22 21 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑋 ) = ( Base ‘ 𝑋 ) )
23 20 22 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( 𝐹 ‘ 𝑌 ) ↑m ( 𝐹 ‘ 𝑋 ) ) = ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) )
24 23 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑓 : ( Base ‘ 𝑋 ) ⟶ ( Base ‘ 𝑌 ) ) → ( ( 𝐹 ‘ 𝑌 ) ↑m ( 𝐹 ‘ 𝑋 ) ) = ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) )
25 18 24 eleqtrrd ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑓 : ( Base ‘ 𝑋 ) ⟶ ( Base ‘ 𝑌 ) ) → 𝑓 ∈ ( ( 𝐹 ‘ 𝑌 ) ↑m ( 𝐹 ‘ 𝑋 ) ) )
26 25 ex ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑓 : ( Base ‘ 𝑋 ) ⟶ ( Base ‘ 𝑌 ) → 𝑓 ∈ ( ( 𝐹 ‘ 𝑌 ) ↑m ( 𝐹 ‘ 𝑋 ) ) ) )
27 11 26 syl5 ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑓 ∈ ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) → 𝑓 ∈ ( ( 𝐹 ‘ 𝑌 ) ↑m ( 𝐹 ‘ 𝑋 ) ) ) )
28 27 ssrdv ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ⊆ ( ( 𝐹 ‘ 𝑌 ) ↑m ( 𝐹 ‘ 𝑋 ) ) )
29 10 28 fssd ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( I ↾ ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ) : ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ⟶ ( ( 𝐹 ‘ 𝑌 ) ↑m ( 𝐹 ‘ 𝑋 ) ) )
30 eqid ⊢ ( Base ‘ 𝑋 ) = ( Base ‘ 𝑋 )
31 eqid ⊢ ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 )
32 1 2 3 4 5 6 7 30 31 funcestrcsetclem5 ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 𝐺 𝑌 ) = ( I ↾ ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ) )
33 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑈 ∈ WUni )
34 eqid ⊢ ( Hom ‘ 𝐸 ) = ( Hom ‘ 𝐸 )
35 1 5 estrcbas ⊢ ( 𝜑 → 𝑈 = ( Base ‘ 𝐸 ) )
36 3 35 eqtr4id ⊢ ( 𝜑 → 𝐵 = 𝑈 )
37 36 eleq2d ⊢ ( 𝜑 → ( 𝑋 ∈ 𝐵 ↔ 𝑋 ∈ 𝑈 ) )
38 37 biimpcd ⊢ ( 𝑋 ∈ 𝐵 → ( 𝜑 → 𝑋 ∈ 𝑈 ) )
39 38 adantr ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝜑 → 𝑋 ∈ 𝑈 ) )
40 39 impcom ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑋 ∈ 𝑈 )
41 36 eleq2d ⊢ ( 𝜑 → ( 𝑌 ∈ 𝐵 ↔ 𝑌 ∈ 𝑈 ) )
42 41 biimpd ⊢ ( 𝜑 → ( 𝑌 ∈ 𝐵 → 𝑌 ∈ 𝑈 ) )
43 42 adantld ⊢ ( 𝜑 → ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑌 ∈ 𝑈 ) )
44 43 imp ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑌 ∈ 𝑈 )
45 1 33 34 40 44 30 31 estrchom ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 ( Hom ‘ 𝐸 ) 𝑌 ) = ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) )
46 eqid ⊢ ( Hom ‘ 𝑆 ) = ( Hom ‘ 𝑆 )
47 1 2 3 4 5 6 funcestrcsetclem2 ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 )
48 47 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 )
49 1 2 3 4 5 6 funcestrcsetclem2 ⊢ ( ( 𝜑 ∧ 𝑌 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑌 ) ∈ 𝑈 )
50 49 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑌 ) ∈ 𝑈 )
51 2 33 46 48 50 setchom ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( 𝐹 ‘ 𝑋 ) ( Hom ‘ 𝑆 ) ( 𝐹 ‘ 𝑌 ) ) = ( ( 𝐹 ‘ 𝑌 ) ↑m ( 𝐹 ‘ 𝑋 ) ) )
52 32 45 51 feq123d ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( 𝑋 𝐺 𝑌 ) : ( 𝑋 ( Hom ‘ 𝐸 ) 𝑌 ) ⟶ ( ( 𝐹 ‘ 𝑋 ) ( Hom ‘ 𝑆 ) ( 𝐹 ‘ 𝑌 ) ) ↔ ( I ↾ ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ) : ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ⟶ ( ( 𝐹 ‘ 𝑌 ) ↑m ( 𝐹 ‘ 𝑋 ) ) ) )
53 29 52 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 𝐺 𝑌 ) : ( 𝑋 ( Hom ‘ 𝐸 ) 𝑌 ) ⟶ ( ( 𝐹 ‘ 𝑋 ) ( Hom ‘ 𝑆 ) ( 𝐹 ‘ 𝑌 ) ) )