funciso

Description: The image of an isomorphism under a functor is an isomorphism. Proposition 3.21 of Adamek p. 32. (Contributed by Mario Carneiro, 3-Jan-2017)

	Ref	Expression
Hypotheses	funciso.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
	funciso.s	⊢ 𝐼 = ( Iso ‘ 𝐷 )
	funciso.t	⊢ 𝐽 = ( Iso ‘ 𝐸 )
	funciso.f	⊢ ( 𝜑 → 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 )
	funciso.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	funciso.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	funciso.m	⊢ ( 𝜑 → 𝑀 ∈ ( 𝑋 𝐼 𝑌 ) )
Assertion	funciso	⊢ ( 𝜑 → ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑀 ) ∈ ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) )

Proof

Step	Hyp	Ref	Expression
1		funciso.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
2		funciso.s	⊢ 𝐼 = ( Iso ‘ 𝐷 )
3		funciso.t	⊢ 𝐽 = ( Iso ‘ 𝐸 )
4		funciso.f	⊢ ( 𝜑 → 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 )
5		funciso.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6		funciso.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
7		funciso.m	⊢ ( 𝜑 → 𝑀 ∈ ( 𝑋 𝐼 𝑌 ) )
8		eqid	⊢ ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
9		eqid	⊢ ( Inv ‘ 𝐸 ) = ( Inv ‘ 𝐸 )
10		df-br	⊢ ( 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 ↔ ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐷 Func 𝐸 ) )
11	4 10	sylib	⊢ ( 𝜑 → ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐷 Func 𝐸 ) )
12		funcrcl	⊢ ( ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐷 Func 𝐸 ) → ( 𝐷 ∈ Cat ∧ 𝐸 ∈ Cat ) )
13	11 12	syl	⊢ ( 𝜑 → ( 𝐷 ∈ Cat ∧ 𝐸 ∈ Cat ) )
14	13	simprd	⊢ ( 𝜑 → 𝐸 ∈ Cat )
15	1 8 4	funcf1	⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ ( Base ‘ 𝐸 ) )
16	15 5	ffvelrnd	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) ∈ ( Base ‘ 𝐸 ) )
17	15 6	ffvelrnd	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑌 ) ∈ ( Base ‘ 𝐸 ) )
18		eqid	⊢ ( Inv ‘ 𝐷 ) = ( Inv ‘ 𝐷 )
19	13	simpld	⊢ ( 𝜑 → 𝐷 ∈ Cat )
20	1 2 18 19 5 6 7	invisoinvr	⊢ ( 𝜑 → 𝑀 ( 𝑋 ( Inv ‘ 𝐷 ) 𝑌 ) ( ( 𝑋 ( Inv ‘ 𝐷 ) 𝑌 ) ‘ 𝑀 ) )
21	1 18 9 4 5 6 20	funcinv	⊢ ( 𝜑 → ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑀 ) ( ( 𝐹 ‘ 𝑋 ) ( Inv ‘ 𝐸 ) ( 𝐹 ‘ 𝑌 ) ) ( ( 𝑌 𝐺 𝑋 ) ‘ ( ( 𝑋 ( Inv ‘ 𝐷 ) 𝑌 ) ‘ 𝑀 ) ) )
22	8 9 14 16 17 3 21	inviso1	⊢ ( 𝜑 → ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑀 ) ∈ ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) )

Metamath Proof Explorer

Theorem funciso

Proof