Metamath Proof Explorer

Theorem funcestrcsetclem6

Description: Lemma 6 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
funcestrcsetc.m ⊢ M = Base X
funcestrcsetc.n ⊢ N = Base Y
Assertion funcestrcsetclem6 ⊢ φ ∧ X ∈ B ∧ Y ∈ B ∧ H ∈ N M → X G Y ⁡ H = H

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 funcestrcsetc.m ⊢ M = Base X
9 funcestrcsetc.n ⊢ N = Base Y
10 1 2 3 4 5 6 7 8 9 funcestrcsetclem5 ⊢ φ ∧ X ∈ B ∧ Y ∈ B → X G Y = I ↾ N M
11 10 3adant3 ⊢ φ ∧ X ∈ B ∧ Y ∈ B ∧ H ∈ N M → X G Y = I ↾ N M
12 11 fveq1d ⊢ φ ∧ X ∈ B ∧ Y ∈ B ∧ H ∈ N M → X G Y ⁡ H = I ↾ N M ⁡ H
13 fvresi ⊢ H ∈ N M → I ↾ N M ⁡ H = H
14 13 3ad2ant3 ⊢ φ ∧ X ∈ B ∧ Y ∈ B ∧ H ∈ N M → I ↾ N M ⁡ H = H
15 12 14 eqtrd ⊢ φ ∧ X ∈ B ∧ Y ∈ B ∧ H ∈ N M → X G Y ⁡ H = H