fcobijfs2

Description: Composing finitely supported functions with a bijection yields a bijection between sets of finitely supported functions. See also fcobijfs and mapfien . (Contributed by Thierry Arnoux, 10-Jan-2026)

	Ref	Expression
Hypotheses	fcobijfs2.1	⊢ ( 𝜑 → 𝐺 : 𝑅 –1-1-onto→ 𝑆 )
	fcobijfs2.2	⊢ ( 𝜑 → 𝑅 ∈ 𝑈 )
	fcobijfs2.3	⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
	fcobijfs2.4	⊢ ( 𝜑 → 𝑇 ∈ 𝑊 )
	fcobijfs2.5	⊢ ( 𝜑 → 𝑂 ∈ 𝑇 )
	fcobijfs2.7	⊢ 𝑋 = { 𝑔 ∈ ( 𝑇 ↑_m 𝑆 ) ∣ 𝑔 finSupp 𝑂 }
	fcobijfs2.8	⊢ 𝑌 = { ℎ ∈ ( 𝑇 ↑_m 𝑅 ) ∣ ℎ finSupp 𝑂 }
Assertion	fcobijfs2	⊢ ( 𝜑 → ( 𝑓 ∈ 𝑋 ↦ ( 𝑓 ∘ 𝐺 ) ) : 𝑋 –1-1-onto→ 𝑌 )

Proof

Step	Hyp	Ref	Expression
1		fcobijfs2.1	⊢ ( 𝜑 → 𝐺 : 𝑅 –1-1-onto→ 𝑆 )
2		fcobijfs2.2	⊢ ( 𝜑 → 𝑅 ∈ 𝑈 )
3		fcobijfs2.3	⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
4		fcobijfs2.4	⊢ ( 𝜑 → 𝑇 ∈ 𝑊 )
5		fcobijfs2.5	⊢ ( 𝜑 → 𝑂 ∈ 𝑇 )
6		fcobijfs2.7	⊢ 𝑋 = { 𝑔 ∈ ( 𝑇 ↑_m 𝑆 ) ∣ 𝑔 finSupp 𝑂 }
7		fcobijfs2.8	⊢ 𝑌 = { ℎ ∈ ( 𝑇 ↑_m 𝑅 ) ∣ ℎ finSupp 𝑂 }
8		breq1	⊢ ( ℎ = 𝑔 → ( ℎ finSupp 𝑂 ↔ 𝑔 finSupp 𝑂 ) )
9	8	cbvrabv	⊢ { ℎ ∈ ( 𝑇 ↑_m 𝑆 ) ∣ ℎ finSupp 𝑂 } = { 𝑔 ∈ ( 𝑇 ↑_m 𝑆 ) ∣ 𝑔 finSupp 𝑂 }
10	6 9	eqtr4i	⊢ 𝑋 = { ℎ ∈ ( 𝑇 ↑_m 𝑆 ) ∣ ℎ finSupp 𝑂 }
11		eqid	⊢ { ℎ ∈ ( 𝑇 ↑_m 𝑅 ) ∣ ℎ finSupp ( ( I ↾ 𝑇 ) ‘ 𝑂 ) } = { ℎ ∈ ( 𝑇 ↑_m 𝑅 ) ∣ ℎ finSupp ( ( I ↾ 𝑇 ) ‘ 𝑂 ) }
12		eqid	⊢ ( ( I ↾ 𝑇 ) ‘ 𝑂 ) = ( ( I ↾ 𝑇 ) ‘ 𝑂 )
13		f1oi	⊢ ( I ↾ 𝑇 ) : 𝑇 –1-1-onto→ 𝑇
14	13	a1i	⊢ ( 𝜑 → ( I ↾ 𝑇 ) : 𝑇 –1-1-onto→ 𝑇 )
15	10 11 12 1 14 3 4 2 4 5	mapfien	⊢ ( 𝜑 → ( 𝑓 ∈ 𝑋 ↦ ( ( I ↾ 𝑇 ) ∘ ( 𝑓 ∘ 𝐺 ) ) ) : 𝑋 –1-1-onto→ { ℎ ∈ ( 𝑇 ↑_m 𝑅 ) ∣ ℎ finSupp ( ( I ↾ 𝑇 ) ‘ 𝑂 ) } )
16		fvresi	⊢ ( 𝑂 ∈ 𝑇 → ( ( I ↾ 𝑇 ) ‘ 𝑂 ) = 𝑂 )
17	5 16	syl	⊢ ( 𝜑 → ( ( I ↾ 𝑇 ) ‘ 𝑂 ) = 𝑂 )
18	17	breq2d	⊢ ( 𝜑 → ( ℎ finSupp ( ( I ↾ 𝑇 ) ‘ 𝑂 ) ↔ ℎ finSupp 𝑂 ) )
19	18	rabbidv	⊢ ( 𝜑 → { ℎ ∈ ( 𝑇 ↑_m 𝑅 ) ∣ ℎ finSupp ( ( I ↾ 𝑇 ) ‘ 𝑂 ) } = { ℎ ∈ ( 𝑇 ↑_m 𝑅 ) ∣ ℎ finSupp 𝑂 } )
20	19 7	eqtr4di	⊢ ( 𝜑 → { ℎ ∈ ( 𝑇 ↑_m 𝑅 ) ∣ ℎ finSupp ( ( I ↾ 𝑇 ) ‘ 𝑂 ) } = 𝑌 )
21	15 20	f1oeq3dd	⊢ ( 𝜑 → ( 𝑓 ∈ 𝑋 ↦ ( ( I ↾ 𝑇 ) ∘ ( 𝑓 ∘ 𝐺 ) ) ) : 𝑋 –1-1-onto→ 𝑌 )
22	6	ssrab3	⊢ 𝑋 ⊆ ( 𝑇 ↑_m 𝑆 )
23	22	sseli	⊢ ( 𝑓 ∈ 𝑋 → 𝑓 ∈ ( 𝑇 ↑_m 𝑆 ) )
24		elmapi	⊢ ( 𝑓 ∈ ( 𝑇 ↑_m 𝑆 ) → 𝑓 : 𝑆 ⟶ 𝑇 )
25		f1of	⊢ ( 𝐺 : 𝑅 –1-1-onto→ 𝑆 → 𝐺 : 𝑅 ⟶ 𝑆 )
26	1 25	syl	⊢ ( 𝜑 → 𝐺 : 𝑅 ⟶ 𝑆 )
27		fco	⊢ ( ( 𝑓 : 𝑆 ⟶ 𝑇 ∧ 𝐺 : 𝑅 ⟶ 𝑆 ) → ( 𝑓 ∘ 𝐺 ) : 𝑅 ⟶ 𝑇 )
28	24 26 27	syl2anr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑇 ↑_m 𝑆 ) ) → ( 𝑓 ∘ 𝐺 ) : 𝑅 ⟶ 𝑇 )
29		fcoi2	⊢ ( ( 𝑓 ∘ 𝐺 ) : 𝑅 ⟶ 𝑇 → ( ( I ↾ 𝑇 ) ∘ ( 𝑓 ∘ 𝐺 ) ) = ( 𝑓 ∘ 𝐺 ) )
30	28 29	syl	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑇 ↑_m 𝑆 ) ) → ( ( I ↾ 𝑇 ) ∘ ( 𝑓 ∘ 𝐺 ) ) = ( 𝑓 ∘ 𝐺 ) )
31	23 30	sylan2	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → ( ( I ↾ 𝑇 ) ∘ ( 𝑓 ∘ 𝐺 ) ) = ( 𝑓 ∘ 𝐺 ) )
32	31	mpteq2dva	⊢ ( 𝜑 → ( 𝑓 ∈ 𝑋 ↦ ( ( I ↾ 𝑇 ) ∘ ( 𝑓 ∘ 𝐺 ) ) ) = ( 𝑓 ∈ 𝑋 ↦ ( 𝑓 ∘ 𝐺 ) ) )
33	32	f1oeq1d	⊢ ( 𝜑 → ( ( 𝑓 ∈ 𝑋 ↦ ( ( I ↾ 𝑇 ) ∘ ( 𝑓 ∘ 𝐺 ) ) ) : 𝑋 –1-1-onto→ 𝑌 ↔ ( 𝑓 ∈ 𝑋 ↦ ( 𝑓 ∘ 𝐺 ) ) : 𝑋 –1-1-onto→ 𝑌 ) )
34	21 33	mpbid	⊢ ( 𝜑 → ( 𝑓 ∈ 𝑋 ↦ ( 𝑓 ∘ 𝐺 ) ) : 𝑋 –1-1-onto→ 𝑌 )

Metamath Proof Explorer

Theorem fcobijfs2

Proof