Theorem mapfienlem3

Description: Lemma 3 for mapfien . (Contributed by AV, 3-Jul-2019) (Revised by AV, 28-Jul-2024)

	Ref	Expression
Hypotheses	mapfien.s	⊢ 𝑆 = { 𝑥 ∈ ( 𝐵 ↑m 𝐴 ) ∣ 𝑥 finSupp 𝑍 }
	mapfien.t	⊢ 𝑇 = { 𝑥 ∈ ( 𝐷 ↑m 𝐶 ) ∣ 𝑥 finSupp 𝑊 }
	mapfien.w	⊢ 𝑊 = ( 𝐺 ‘ 𝑍 )
	mapfien.f	⊢ ( 𝜑 → 𝐹 : 𝐶 –1-1-onto→ 𝐴 )
	mapfien.g	⊢ ( 𝜑 → 𝐺 : 𝐵 –1-1-onto→ 𝐷 )
	mapfien.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
	mapfien.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
	mapfien.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑋 )
	mapfien.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑌 )
	mapfien.z	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
Assertion	mapfienlem3	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑇 ) → ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ◡ 𝐹 ) ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		mapfien.s	⊢ 𝑆 = { 𝑥 ∈ ( 𝐵 ↑m 𝐴 ) ∣ 𝑥 finSupp 𝑍 }
2		mapfien.t	⊢ 𝑇 = { 𝑥 ∈ ( 𝐷 ↑m 𝐶 ) ∣ 𝑥 finSupp 𝑊 }
3		mapfien.w	⊢ 𝑊 = ( 𝐺 ‘ 𝑍 )
4		mapfien.f	⊢ ( 𝜑 → 𝐹 : 𝐶 –1-1-onto→ 𝐴 )
5		mapfien.g	⊢ ( 𝜑 → 𝐺 : 𝐵 –1-1-onto→ 𝐷 )
6		mapfien.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
7		mapfien.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
8		mapfien.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑋 )
9		mapfien.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑌 )
10		mapfien.z	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
11		f1ocnv	⊢ ( 𝐺 : 𝐵 –1-1-onto→ 𝐷 → ◡ 𝐺 : 𝐷 –1-1-onto→ 𝐵 )
12		f1of	⊢ ( ◡ 𝐺 : 𝐷 –1-1-onto→ 𝐵 → ◡ 𝐺 : 𝐷 ⟶ 𝐵 )
13	5 11 12	3syl	⊢ ( 𝜑 → ◡ 𝐺 : 𝐷 ⟶ 𝐵 )
14	13	adantr	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑇 ) → ◡ 𝐺 : 𝐷 ⟶ 𝐵 )
15		elrabi	⊢ ( 𝑔 ∈ { 𝑥 ∈ ( 𝐷 ↑m 𝐶 ) ∣ 𝑥 finSupp 𝑊 } → 𝑔 ∈ ( 𝐷 ↑m 𝐶 ) )
16	15 2	eleq2s	⊢ ( 𝑔 ∈ 𝑇 → 𝑔 ∈ ( 𝐷 ↑m 𝐶 ) )
17	16	adantl	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑇 ) → 𝑔 ∈ ( 𝐷 ↑m 𝐶 ) )
18		elmapi	⊢ ( 𝑔 ∈ ( 𝐷 ↑m 𝐶 ) → 𝑔 : 𝐶 ⟶ 𝐷 )
19	17 18	syl	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑇 ) → 𝑔 : 𝐶 ⟶ 𝐷 )
20	14 19	fcod	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑇 ) → ( ◡ 𝐺 ∘ 𝑔 ) : 𝐶 ⟶ 𝐵 )
21		f1ocnv	⊢ ( 𝐹 : 𝐶 –1-1-onto→ 𝐴 → ◡ 𝐹 : 𝐴 –1-1-onto→ 𝐶 )
22		f1of	⊢ ( ◡ 𝐹 : 𝐴 –1-1-onto→ 𝐶 → ◡ 𝐹 : 𝐴 ⟶ 𝐶 )
23	4 21 22	3syl	⊢ ( 𝜑 → ◡ 𝐹 : 𝐴 ⟶ 𝐶 )
24	23	adantr	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑇 ) → ◡ 𝐹 : 𝐴 ⟶ 𝐶 )
25	20 24	fcod	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑇 ) → ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ◡ 𝐹 ) : 𝐴 ⟶ 𝐵 )
26	7 6	elmapd	⊢ ( 𝜑 → ( ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ◡ 𝐹 ) ∈ ( 𝐵 ↑m 𝐴 ) ↔ ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ◡ 𝐹 ) : 𝐴 ⟶ 𝐵 ) )
27	26	adantr	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑇 ) → ( ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ◡ 𝐹 ) ∈ ( 𝐵 ↑m 𝐴 ) ↔ ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ◡ 𝐹 ) : 𝐴 ⟶ 𝐵 ) )
28	25 27	mpbird	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑇 ) → ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ◡ 𝐹 ) ∈ ( 𝐵 ↑m 𝐴 ) )
29	1 2 3 4 5 6 7 8 9 10	mapfienlem2	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑇 ) → ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ◡ 𝐹 ) finSupp 𝑍 )
30		breq1	⊢ ( 𝑥 = ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ◡ 𝐹 ) → ( 𝑥 finSupp 𝑍 ↔ ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ◡ 𝐹 ) finSupp 𝑍 ) )
31	30 1	elrab2	⊢ ( ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ◡ 𝐹 ) ∈ 𝑆 ↔ ( ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ◡ 𝐹 ) ∈ ( 𝐵 ↑m 𝐴 ) ∧ ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ◡ 𝐹 ) finSupp 𝑍 ) )
32	28 29 31	sylanbrc	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑇 ) → ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ◡ 𝐹 ) ∈ 𝑆 )