This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem funcsetcestrclem3

Description: Lemma 3 for funcsetcestrc . (Contributed by AV, 27-Mar-2020)

Ref Expression
Hypotheses funcsetcestrc.s ⊢ S = SetCat ⁡ U
funcsetcestrc.c ⊢ C = Base S
funcsetcestrc.f ⊢ φ → F = x ∈ C ⟼ Base ndx x
funcsetcestrc.u ⊢ φ → U ∈ WUni
funcsetcestrc.o ⊢ φ → ω ∈ U
funcsetcestrclem3.e ⊢ E = ExtStrCat ⁡ U
funcsetcestrclem3.b ⊢ B = Base E
Assertion funcsetcestrclem3 ⊢ φ → F : C ⟶ B

Proof

Step Hyp Ref Expression
1 funcsetcestrc.s ⊢ S = SetCat ⁡ U
2 funcsetcestrc.c ⊢ C = Base S
3 funcsetcestrc.f ⊢ φ → F = x ∈ C ⟼ Base ndx x
4 funcsetcestrc.u ⊢ φ → U ∈ WUni
5 funcsetcestrc.o ⊢ φ → ω ∈ U
6 funcsetcestrclem3.e ⊢ E = ExtStrCat ⁡ U
7 funcsetcestrclem3.b ⊢ B = Base E
8 1 2 4 5 setc1strwun ⊢ φ ∧ x ∈ C → Base ndx x ∈ U
9 6 4 estrcbas ⊢ φ → U = Base E
10 9 eqcomd ⊢ φ → Base E = U
11 10 adantr ⊢ φ ∧ x ∈ C → Base E = U
12 8 11 eleqtrrd ⊢ φ ∧ x ∈ C → Base ndx x ∈ Base E
13 12 7 eleqtrrdi ⊢ φ ∧ x ∈ C → Base ndx x ∈ B
14 3 13 fmpt3d ⊢ φ → F : C ⟶ B