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

Metamath Proof Explorer

Theorem funcsetcestrclem7

Description: Lemma 7 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 ⊢ ( 𝜑 → ω ∈ 𝑈 )
funcsetcestrc.g ⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐶 ↦ ( I ↾ ( 𝑦 ↑m 𝑥 ) ) ) )
funcsetcestrc.e ⊢ 𝐸 = ( ExtStrCat ‘ 𝑈 )
Assertion funcsetcestrclem7 ( ( 𝜑 ∧ 𝑋 ∈ 𝐶 ) → ( ( 𝑋 𝐺 𝑋 ) ‘ ( ( Id ‘ 𝑆 ) ‘ 𝑋 ) ) = ( ( Id ‘ 𝐸 ) ‘ ( 𝐹 ‘ 𝑋 ) ) )

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 funcsetcestrc.g ⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐶 ↦ ( I ↾ ( 𝑦 ↑m 𝑥 ) ) ) )
7 funcsetcestrc.e ⊢ 𝐸 = ( ExtStrCat ‘ 𝑈 )
8 1 2 3 4 5 6 funcsetcestrclem5 ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑋 ∈ 𝐶 ) ) → ( 𝑋 𝐺 𝑋 ) = ( I ↾ ( 𝑋 ↑m 𝑋 ) ) )
9 8 anabsan2 ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐶 ) → ( 𝑋 𝐺 𝑋 ) = ( I ↾ ( 𝑋 ↑m 𝑋 ) ) )
10 eqid ⊢ ( Id ‘ 𝑆 ) = ( Id ‘ 𝑆 )
11 4 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐶 ) → 𝑈 ∈ WUni )
12 1 4 setcbas ⊢ ( 𝜑 → 𝑈 = ( Base ‘ 𝑆 ) )
13 2 12 eqtr4id ⊢ ( 𝜑 → 𝐶 = 𝑈 )
14 13 eleq2d ⊢ ( 𝜑 → ( 𝑋 ∈ 𝐶 ↔ 𝑋 ∈ 𝑈 ) )
15 14 biimpa ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐶 ) → 𝑋 ∈ 𝑈 )
16 1 10 11 15 setcid ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐶 ) → ( ( Id ‘ 𝑆 ) ‘ 𝑋 ) = ( I ↾ 𝑋 ) )
17 9 16 fveq12d ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐶 ) → ( ( 𝑋 𝐺 𝑋 ) ‘ ( ( Id ‘ 𝑆 ) ‘ 𝑋 ) ) = ( ( I ↾ ( 𝑋 ↑m 𝑋 ) ) ‘ ( I ↾ 𝑋 ) ) )
18 f1oi ⊢ ( I ↾ 𝑋 ) : 𝑋 –1-1-onto→ 𝑋
19 f1of ⊢ ( ( I ↾ 𝑋 ) : 𝑋 –1-1-onto→ 𝑋 → ( I ↾ 𝑋 ) : 𝑋 ⟶ 𝑋 )
20 18 19 ax-mp ⊢ ( I ↾ 𝑋 ) : 𝑋 ⟶ 𝑋
21 simpr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐶 ) → 𝑋 ∈ 𝐶 )
22 21 21 elmapd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐶 ) → ( ( I ↾ 𝑋 ) ∈ ( 𝑋 ↑m 𝑋 ) ↔ ( I ↾ 𝑋 ) : 𝑋 ⟶ 𝑋 ) )
23 20 22 mpbiri ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐶 ) → ( I ↾ 𝑋 ) ∈ ( 𝑋 ↑m 𝑋 ) )
24 fvresi ⊢ ( ( I ↾ 𝑋 ) ∈ ( 𝑋 ↑m 𝑋 ) → ( ( I ↾ ( 𝑋 ↑m 𝑋 ) ) ‘ ( I ↾ 𝑋 ) ) = ( I ↾ 𝑋 ) )
25 23 24 syl ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐶 ) → ( ( I ↾ ( 𝑋 ↑m 𝑋 ) ) ‘ ( I ↾ 𝑋 ) ) = ( I ↾ 𝑋 ) )
26 eqid ⊢ { ⟨ ( Base ‘ ndx ) , 𝑋 ⟩ } = { ⟨ ( Base ‘ ndx ) , 𝑋 ⟩ }
27 26 1strbas ⊢ ( 𝑋 ∈ 𝐶 → 𝑋 = ( Base ‘ { ⟨ ( Base ‘ ndx ) , 𝑋 ⟩ } ) )
28 21 27 syl ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐶 ) → 𝑋 = ( Base ‘ { ⟨ ( Base ‘ ndx ) , 𝑋 ⟩ } ) )
29 28 reseq2d ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐶 ) → ( I ↾ 𝑋 ) = ( I ↾ ( Base ‘ { ⟨ ( Base ‘ ndx ) , 𝑋 ⟩ } ) ) )
30 25 29 eqtrd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐶 ) → ( ( I ↾ ( 𝑋 ↑m 𝑋 ) ) ‘ ( I ↾ 𝑋 ) ) = ( I ↾ ( Base ‘ { ⟨ ( Base ‘ ndx ) , 𝑋 ⟩ } ) ) )
31 1 2 3 funcsetcestrclem1 ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑋 ) = { ⟨ ( Base ‘ ndx ) , 𝑋 ⟩ } )
32 31 fveq2d ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐶 ) → ( ( Id ‘ 𝐸 ) ‘ ( 𝐹 ‘ 𝑋 ) ) = ( ( Id ‘ 𝐸 ) ‘ { ⟨ ( Base ‘ ndx ) , 𝑋 ⟩ } ) )
33 eqid ⊢ ( Id ‘ 𝐸 ) = ( Id ‘ 𝐸 )
34 1 2 4 5 setc1strwun ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐶 ) → { ⟨ ( Base ‘ ndx ) , 𝑋 ⟩ } ∈ 𝑈 )
35 7 33 11 34 estrcid ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐶 ) → ( ( Id ‘ 𝐸 ) ‘ { ⟨ ( Base ‘ ndx ) , 𝑋 ⟩ } ) = ( I ↾ ( Base ‘ { ⟨ ( Base ‘ ndx ) , 𝑋 ⟩ } ) ) )
36 32 35 eqtr2d ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐶 ) → ( I ↾ ( Base ‘ { ⟨ ( Base ‘ ndx ) , 𝑋 ⟩ } ) ) = ( ( Id ‘ 𝐸 ) ‘ ( 𝐹 ‘ 𝑋 ) ) )
37 17 30 36 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐶 ) → ( ( 𝑋 𝐺 𝑋 ) ‘ ( ( Id ‘ 𝑆 ) ‘ 𝑋 ) ) = ( ( Id ‘ 𝐸 ) ‘ ( 𝐹 ‘ 𝑋 ) ) )