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 ‘ 𝐸 ) ‘ ( 𝐹 ‘ 𝑋 ) ) )