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 ⊢ 𝑆 = ( 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 ⊢ ( 𝜑 → 𝐹 : 𝐶 ⟶ 𝐵 )