Theorem funcsetcestrclem3

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

	Ref	Expression
Hypotheses	funcsetcestrc.s	⊢ 𝑆 = ( SetCat ‘ 𝑈 )
	funcsetcestrc.c	⊢ 𝐶 = ( Base ‘ 𝑆 )
	funcsetcestrc.f	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐶 ↦ { ⟨ ( Base ‘ ndx ) , 𝑥 ⟩ } ) )
	funcsetcestrc.u	⊢ ( 𝜑 → 𝑈 ∈ WUni )
	funcsetcestrc.o	⊢ ( 𝜑 → ω ∈ 𝑈 )
	funcsetcestrclem3.e	⊢ 𝐸 = ( ExtStrCat ‘ 𝑈 )
	funcsetcestrclem3.b	⊢ 𝐵 = ( Base ‘ 𝐸 )
Assertion	funcsetcestrclem3	⊢ ( 𝜑 → 𝐹 : 𝐶 ⟶ 𝐵 )

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		funcsetcestrclem3.e	⊢ 𝐸 = ( ExtStrCat ‘ 𝑈 )
7		funcsetcestrclem3.b	⊢ 𝐵 = ( Base ‘ 𝐸 )
8	1 2 4 5	setc1strwun	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → { ⟨ ( Base ‘ ndx ) , 𝑥 ⟩ } ∈ 𝑈 )
9	6 4	estrcbas	⊢ ( 𝜑 → 𝑈 = ( Base ‘ 𝐸 ) )
10	9	eqcomd	⊢ ( 𝜑 → ( Base ‘ 𝐸 ) = 𝑈 )
11	10	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( Base ‘ 𝐸 ) = 𝑈 )
12	8 11	eleqtrrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → { ⟨ ( Base ‘ ndx ) , 𝑥 ⟩ } ∈ ( Base ‘ 𝐸 ) )
13	12 7	eleqtrrdi	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → { ⟨ ( Base ‘ ndx ) , 𝑥 ⟩ } ∈ 𝐵 )
14	3 13	fmpt3d	⊢ ( 𝜑 → 𝐹 : 𝐶 ⟶ 𝐵 )