Metamath Proof Explorer

Theorem funcsetcestrclem8

Description: Lemma 8 for funcsetcestrc . (Contributed by AV, 28-Mar-2020)

Ref Expression
Hypotheses funcsetcestrc.s ⊢ 𝑆 = ( SetCat ‘ 𝑈 )
funcsetcestrc.c ⊢ 𝐶 = ( Base ‘ 𝑆 )
funcsetcestrc.f ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐶 ↦ { ⟨ ( Base ‘ ndx ) , 𝑥 ⟩ } ) )
funcsetcestrc.u ⊢ ( 𝜑 → 𝑈 ∈ WUni )
funcsetcestrc.o ⊢ ( 𝜑 → ω ∈ 𝑈 )
funcsetcestrc.g ⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐶 ↦ ( I ↾ ( 𝑦 ↑m 𝑥 ) ) ) )
funcsetcestrc.e ⊢ 𝐸 = ( ExtStrCat ‘ 𝑈 )
Assertion funcsetcestrclem8 ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ) → ( 𝑋 𝐺 𝑌 ) : ( 𝑋 ( Hom ‘ 𝑆 ) 𝑌 ) ⟶ ( ( 𝐹 ‘ 𝑋 ) ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 funcsetcestrc.s ⊢ 𝑆 = ( SetCat ‘ 𝑈 )
2 funcsetcestrc.c ⊢ 𝐶 = ( Base ‘ 𝑆 )
3 funcsetcestrc.f ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐶 ↦ { ⟨ ( Base ‘ ndx ) , 𝑥 ⟩ } ) )
4 funcsetcestrc.u ⊢ ( 𝜑 → 𝑈 ∈ WUni )
5 funcsetcestrc.o ⊢ ( 𝜑 → ω ∈ 𝑈 )
6 funcsetcestrc.g ⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐶 ↦ ( I ↾ ( 𝑦 ↑m 𝑥 ) ) ) )
7 funcsetcestrc.e ⊢ 𝐸 = ( ExtStrCat ‘ 𝑈 )
8 f1oi ⊢ ( I ↾ ( 𝑌 ↑m 𝑋 ) ) : ( 𝑌 ↑m 𝑋 ) –1-1-onto→ ( 𝑌 ↑m 𝑋 )
9 f1of ⊢ ( ( I ↾ ( 𝑌 ↑m 𝑋 ) ) : ( 𝑌 ↑m 𝑋 ) –1-1-onto→ ( 𝑌 ↑m 𝑋 ) → ( I ↾ ( 𝑌 ↑m 𝑋 ) ) : ( 𝑌 ↑m 𝑋 ) ⟶ ( 𝑌 ↑m 𝑋 ) )
10 8 9 mp1i ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ) → ( I ↾ ( 𝑌 ↑m 𝑋 ) ) : ( 𝑌 ↑m 𝑋 ) ⟶ ( 𝑌 ↑m 𝑋 ) )
11 elmapi ⊢ ( 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) → 𝑓 : 𝑋 ⟶ 𝑌 )
12 simpr ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ) → ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) )
13 12 ancomd ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ) → ( 𝑌 ∈ 𝐶 ∧ 𝑋 ∈ 𝐶 ) )
14 elmapg ⊢ ( ( 𝑌 ∈ 𝐶 ∧ 𝑋 ∈ 𝐶 ) → ( 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ↔ 𝑓 : 𝑋 ⟶ 𝑌 ) )
15 13 14 syl ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ) → ( 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ↔ 𝑓 : 𝑋 ⟶ 𝑌 ) )
16 15 biimpar ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ) ∧ 𝑓 : 𝑋 ⟶ 𝑌 ) → 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) )
17 1 2 3 funcsetcestrclem1 ⊢ ( ( 𝜑 ∧ 𝑌 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑌 ) = { ⟨ ( Base ‘ ndx ) , 𝑌 ⟩ } )
18 17 fveq2d ⊢ ( ( 𝜑 ∧ 𝑌 ∈ 𝐶 ) → ( Base ‘ ( 𝐹 ‘ 𝑌 ) ) = ( Base ‘ { ⟨ ( Base ‘ ndx ) , 𝑌 ⟩ } ) )
19 eqid ⊢ { ⟨ ( Base ‘ ndx ) , 𝑌 ⟩ } = { ⟨ ( Base ‘ ndx ) , 𝑌 ⟩ }
20 19 1strbas ⊢ ( 𝑌 ∈ 𝐶 → 𝑌 = ( Base ‘ { ⟨ ( Base ‘ ndx ) , 𝑌 ⟩ } ) )
21 20 eqcomd ⊢ ( 𝑌 ∈ 𝐶 → ( Base ‘ { ⟨ ( Base ‘ ndx ) , 𝑌 ⟩ } ) = 𝑌 )
22 21 adantl ⊢ ( ( 𝜑 ∧ 𝑌 ∈ 𝐶 ) → ( Base ‘ { ⟨ ( Base ‘ ndx ) , 𝑌 ⟩ } ) = 𝑌 )
23 18 22 eqtrd ⊢ ( ( 𝜑 ∧ 𝑌 ∈ 𝐶 ) → ( Base ‘ ( 𝐹 ‘ 𝑌 ) ) = 𝑌 )
24 23 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ) → ( Base ‘ ( 𝐹 ‘ 𝑌 ) ) = 𝑌 )
25 1 2 3 funcsetcestrclem1 ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑋 ) = { ⟨ ( Base ‘ ndx ) , 𝑋 ⟩ } )
26 25 fveq2d ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐶 ) → ( Base ‘ ( 𝐹 ‘ 𝑋 ) ) = ( Base ‘ { ⟨ ( Base ‘ ndx ) , 𝑋 ⟩ } ) )
27 eqid ⊢ { ⟨ ( Base ‘ ndx ) , 𝑋 ⟩ } = { ⟨ ( Base ‘ ndx ) , 𝑋 ⟩ }
28 27 1strbas ⊢ ( 𝑋 ∈ 𝐶 → 𝑋 = ( Base ‘ { ⟨ ( Base ‘ ndx ) , 𝑋 ⟩ } ) )
29 28 adantl ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐶 ) → 𝑋 = ( Base ‘ { ⟨ ( Base ‘ ndx ) , 𝑋 ⟩ } ) )
30 26 29 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐶 ) → ( Base ‘ ( 𝐹 ‘ 𝑋 ) ) = 𝑋 )
31 30 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ) → ( Base ‘ ( 𝐹 ‘ 𝑋 ) ) = 𝑋 )
32 24 31 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ) → ( ( Base ‘ ( 𝐹 ‘ 𝑌 ) ) ↑m ( Base ‘ ( 𝐹 ‘ 𝑋 ) ) ) = ( 𝑌 ↑m 𝑋 ) )
33 32 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ) ∧ 𝑓 : 𝑋 ⟶ 𝑌 ) → ( ( Base ‘ ( 𝐹 ‘ 𝑌 ) ) ↑m ( Base ‘ ( 𝐹 ‘ 𝑋 ) ) ) = ( 𝑌 ↑m 𝑋 ) )
34 16 33 eleqtrrd ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ) ∧ 𝑓 : 𝑋 ⟶ 𝑌 ) → 𝑓 ∈ ( ( Base ‘ ( 𝐹 ‘ 𝑌 ) ) ↑m ( Base ‘ ( 𝐹 ‘ 𝑋 ) ) ) )
35 34 ex ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ) → ( 𝑓 : 𝑋 ⟶ 𝑌 → 𝑓 ∈ ( ( Base ‘ ( 𝐹 ‘ 𝑌 ) ) ↑m ( Base ‘ ( 𝐹 ‘ 𝑋 ) ) ) ) )
36 11 35 syl5 ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ) → ( 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) → 𝑓 ∈ ( ( Base ‘ ( 𝐹 ‘ 𝑌 ) ) ↑m ( Base ‘ ( 𝐹 ‘ 𝑋 ) ) ) ) )
37 36 ssrdv ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ) → ( 𝑌 ↑m 𝑋 ) ⊆ ( ( Base ‘ ( 𝐹 ‘ 𝑌 ) ) ↑m ( Base ‘ ( 𝐹 ‘ 𝑋 ) ) ) )
38 10 37 fssd ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ) → ( I ↾ ( 𝑌 ↑m 𝑋 ) ) : ( 𝑌 ↑m 𝑋 ) ⟶ ( ( Base ‘ ( 𝐹 ‘ 𝑌 ) ) ↑m ( Base ‘ ( 𝐹 ‘ 𝑋 ) ) ) )
39 1 2 3 4 5 6 funcsetcestrclem5 ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ) → ( 𝑋 𝐺 𝑌 ) = ( I ↾ ( 𝑌 ↑m 𝑋 ) ) )
40 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ) → 𝑈 ∈ WUni )
41 eqid ⊢ ( Hom ‘ 𝑆 ) = ( Hom ‘ 𝑆 )
42 1 4 setcbas ⊢ ( 𝜑 → 𝑈 = ( Base ‘ 𝑆 ) )
43 2 42 eqtr4id ⊢ ( 𝜑 → 𝐶 = 𝑈 )
44 43 eleq2d ⊢ ( 𝜑 → ( 𝑋 ∈ 𝐶 ↔ 𝑋 ∈ 𝑈 ) )
45 44 biimpd ⊢ ( 𝜑 → ( 𝑋 ∈ 𝐶 → 𝑋 ∈ 𝑈 ) )
46 45 adantrd ⊢ ( 𝜑 → ( ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) → 𝑋 ∈ 𝑈 ) )
47 46 imp ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ) → 𝑋 ∈ 𝑈 )
48 43 eleq2d ⊢ ( 𝜑 → ( 𝑌 ∈ 𝐶 ↔ 𝑌 ∈ 𝑈 ) )
49 48 biimpd ⊢ ( 𝜑 → ( 𝑌 ∈ 𝐶 → 𝑌 ∈ 𝑈 ) )
50 49 adantld ⊢ ( 𝜑 → ( ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) → 𝑌 ∈ 𝑈 ) )
51 50 imp ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ) → 𝑌 ∈ 𝑈 )
52 1 40 41 47 51 setchom ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ) → ( 𝑋 ( Hom ‘ 𝑆 ) 𝑌 ) = ( 𝑌 ↑m 𝑋 ) )
53 eqid ⊢ ( Hom ‘ 𝐸 ) = ( Hom ‘ 𝐸 )
54 1 2 3 4 5 funcsetcestrclem2 ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 )
55 54 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ) → ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 )
56 1 2 3 4 5 funcsetcestrclem2 ⊢ ( ( 𝜑 ∧ 𝑌 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑌 ) ∈ 𝑈 )
57 56 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ) → ( 𝐹 ‘ 𝑌 ) ∈ 𝑈 )
58 eqid ⊢ ( Base ‘ ( 𝐹 ‘ 𝑋 ) ) = ( Base ‘ ( 𝐹 ‘ 𝑋 ) )
59 eqid ⊢ ( Base ‘ ( 𝐹 ‘ 𝑌 ) ) = ( Base ‘ ( 𝐹 ‘ 𝑌 ) )
60 7 40 53 55 57 58 59 estrchom ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ) → ( ( 𝐹 ‘ 𝑋 ) ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑌 ) ) = ( ( Base ‘ ( 𝐹 ‘ 𝑌 ) ) ↑m ( Base ‘ ( 𝐹 ‘ 𝑋 ) ) ) )
61 39 52 60 feq123d ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ) → ( ( 𝑋 𝐺 𝑌 ) : ( 𝑋 ( Hom ‘ 𝑆 ) 𝑌 ) ⟶ ( ( 𝐹 ‘ 𝑋 ) ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑌 ) ) ↔ ( I ↾ ( 𝑌 ↑m 𝑋 ) ) : ( 𝑌 ↑m 𝑋 ) ⟶ ( ( Base ‘ ( 𝐹 ‘ 𝑌 ) ) ↑m ( Base ‘ ( 𝐹 ‘ 𝑋 ) ) ) ) )
62 38 61 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ) → ( 𝑋 𝐺 𝑌 ) : ( 𝑋 ( Hom ‘ 𝑆 ) 𝑌 ) ⟶ ( ( 𝐹 ‘ 𝑋 ) ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑌 ) ) )