Metamath Proof Explorer


Theorem funcestrcsetclem8

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

Ref Expression
Hypotheses funcestrcsetc.e E = ExtStrCat U
funcestrcsetc.s S = SetCat U
funcestrcsetc.b B = Base E
funcestrcsetc.c C = Base S
funcestrcsetc.u φ U WUni
funcestrcsetc.f φ F = x B Base x
funcestrcsetc.g φ G = x B , y B I Base y Base x
Assertion funcestrcsetclem8 φ X B Y B X G Y : X Hom E Y F X Hom S F Y

Proof

Step Hyp Ref Expression
1 funcestrcsetc.e E = ExtStrCat U
2 funcestrcsetc.s S = SetCat U
3 funcestrcsetc.b B = Base E
4 funcestrcsetc.c C = Base S
5 funcestrcsetc.u φ U WUni
6 funcestrcsetc.f φ F = x B Base x
7 funcestrcsetc.g φ G = x B , y B I Base y Base x
8 f1oi I Base Y Base X : Base Y Base X 1-1 onto Base Y Base X
9 f1of I Base Y Base X : Base Y Base X 1-1 onto Base Y Base X I Base Y Base X : Base Y Base X Base Y Base X
10 8 9 mp1i φ X B Y B I Base Y Base X : Base Y Base X Base Y Base X
11 elmapi f Base Y Base X f : Base X Base Y
12 fvex Base Y V
13 fvex Base X V
14 12 13 pm3.2i Base Y V Base X V
15 elmapg Base Y V Base X V f Base Y Base X f : Base X Base Y
16 15 bicomd Base Y V Base X V f : Base X Base Y f Base Y Base X
17 14 16 mp1i φ X B Y B f : Base X Base Y f Base Y Base X
18 17 biimpa φ X B Y B f : Base X Base Y f Base Y Base X
19 1 2 3 4 5 6 funcestrcsetclem1 φ Y B F Y = Base Y
20 19 adantrl φ X B Y B F Y = Base Y
21 1 2 3 4 5 6 funcestrcsetclem1 φ X B F X = Base X
22 21 adantrr φ X B Y B F X = Base X
23 20 22 oveq12d φ X B Y B F Y F X = Base Y Base X
24 23 adantr φ X B Y B f : Base X Base Y F Y F X = Base Y Base X
25 18 24 eleqtrrd φ X B Y B f : Base X Base Y f F Y F X
26 25 ex φ X B Y B f : Base X Base Y f F Y F X
27 11 26 syl5 φ X B Y B f Base Y Base X f F Y F X
28 27 ssrdv φ X B Y B Base Y Base X F Y F X
29 10 28 fssd φ X B Y B I Base Y Base X : Base Y Base X F Y F X
30 eqid Base X = Base X
31 eqid Base Y = Base Y
32 1 2 3 4 5 6 7 30 31 funcestrcsetclem5 φ X B Y B X G Y = I Base Y Base X
33 5 adantr φ X B Y B U WUni
34 eqid Hom E = Hom E
35 1 5 estrcbas φ U = Base E
36 3 35 eqtr4id φ B = U
37 36 eleq2d φ X B X U
38 37 biimpcd X B φ X U
39 38 adantr X B Y B φ X U
40 39 impcom φ X B Y B X U
41 36 eleq2d φ Y B Y U
42 41 biimpd φ Y B Y U
43 42 adantld φ X B Y B Y U
44 43 imp φ X B Y B Y U
45 1 33 34 40 44 30 31 estrchom φ X B Y B X Hom E Y = Base Y Base X
46 eqid Hom S = Hom S
47 1 2 3 4 5 6 funcestrcsetclem2 φ X B F X U
48 47 adantrr φ X B Y B F X U
49 1 2 3 4 5 6 funcestrcsetclem2 φ Y B F Y U
50 49 adantrl φ X B Y B F Y U
51 2 33 46 48 50 setchom φ X B Y B F X Hom S F Y = F Y F X
52 32 45 51 feq123d φ X B Y B X G Y : X Hom E Y F X Hom S F Y I Base Y Base X : Base Y Base X F Y F X
53 29 52 mpbird φ X B Y B X G Y : X Hom E Y F X Hom S F Y