Metamath Proof Explorer


Theorem funcestrcsetclem7

Description: Lemma 7 for funcestrcsetc . (Contributed by AV, 23-Mar-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 funcestrcsetclem7 φ X B X G X Id E X = Id S F X

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 eqid Base X = Base X
9 1 2 3 4 5 6 7 8 8 funcestrcsetclem5 φ X B X B X G X = I Base X Base X
10 9 anabsan2 φ X B X G X = I Base X Base X
11 eqid Id E = Id E
12 5 adantr φ X B U WUni
13 1 5 estrcbas φ U = Base E
14 3 13 eqtr4id φ B = U
15 14 eleq2d φ X B X U
16 15 biimpa φ X B X U
17 1 11 12 16 estrcid φ X B Id E X = I Base X
18 10 17 fveq12d φ X B X G X Id E X = I Base X Base X I Base X
19 fvex Base X V
20 19 19 pm3.2i Base X V Base X V
21 20 a1i φ X B Base X V Base X V
22 f1oi I Base X : Base X 1-1 onto Base X
23 f1of I Base X : Base X 1-1 onto Base X I Base X : Base X Base X
24 22 23 ax-mp I Base X : Base X Base X
25 elmapg Base X V Base X V I Base X Base X Base X I Base X : Base X Base X
26 24 25 mpbiri Base X V Base X V I Base X Base X Base X
27 fvresi I Base X Base X Base X I Base X Base X I Base X = I Base X
28 21 26 27 3syl φ X B I Base X Base X I Base X = I Base X
29 1 2 3 4 5 6 funcestrcsetclem1 φ X B F X = Base X
30 29 fveq2d φ X B Id S F X = Id S Base X
31 eqid Id S = Id S
32 1 3 5 estrcbasbas φ X B Base X U
33 2 31 12 32 setcid φ X B Id S Base X = I Base X
34 30 33 eqtr2d φ X B I Base X = Id S F X
35 18 28 34 3eqtrd φ X B X G X Id E X = Id S F X