Theorem mapfienlem3

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

	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	⊢ ( 𝜑 → 𝐴 ∈ V )
	mapfien.b	⊢ ( 𝜑 → 𝐵 ∈ V )
	mapfien.c	⊢ ( 𝜑 → 𝐶 ∈ V )
	mapfien.d	⊢ ( 𝜑 → 𝐷 ∈ V )
	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	⊢ ( 𝜑 → 𝐴 ∈ V )
7		mapfien.b	⊢ ( 𝜑 → 𝐵 ∈ V )
8		mapfien.c	⊢ ( 𝜑 → 𝐶 ∈ V )
9		mapfien.d	⊢ ( 𝜑 → 𝐷 ∈ V )
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		fco	⊢ ( ( ◡ 𝐺 : 𝐷 ⟶ 𝐵 ∧ 𝑔 : 𝐶 ⟶ 𝐷 ) → ( ◡ 𝐺 ∘ 𝑔 ) : 𝐶 ⟶ 𝐵 )
21	14 19 20	syl2anc	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑇 ) → ( ◡ 𝐺 ∘ 𝑔 ) : 𝐶 ⟶ 𝐵 )
22		f1ocnv	⊢ ( 𝐹 : 𝐶 –1-1-onto→ 𝐴 → ◡ 𝐹 : 𝐴 –1-1-onto→ 𝐶 )
23		f1of	⊢ ( ◡ 𝐹 : 𝐴 –1-1-onto→ 𝐶 → ◡ 𝐹 : 𝐴 ⟶ 𝐶 )
24	4 22 23	3syl	⊢ ( 𝜑 → ◡ 𝐹 : 𝐴 ⟶ 𝐶 )
25	24	adantr	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑇 ) → ◡ 𝐹 : 𝐴 ⟶ 𝐶 )
26		fco	⊢ ( ( ( ◡ 𝐺 ∘ 𝑔 ) : 𝐶 ⟶ 𝐵 ∧ ◡ 𝐹 : 𝐴 ⟶ 𝐶 ) → ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ◡ 𝐹 ) : 𝐴 ⟶ 𝐵 )
27	21 25 26	syl2anc	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑇 ) → ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ◡ 𝐹 ) : 𝐴 ⟶ 𝐵 )
28	7 6	elmapd	⊢ ( 𝜑 → ( ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ◡ 𝐹 ) ∈ ( 𝐵 ↑m 𝐴 ) ↔ ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ◡ 𝐹 ) : 𝐴 ⟶ 𝐵 ) )
29	28	adantr	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑇 ) → ( ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ◡ 𝐹 ) ∈ ( 𝐵 ↑m 𝐴 ) ↔ ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ◡ 𝐹 ) : 𝐴 ⟶ 𝐵 ) )
30	27 29	mpbird	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑇 ) → ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ◡ 𝐹 ) ∈ ( 𝐵 ↑m 𝐴 ) )
31	1 2 3 4 5 6 7 8 9 10	mapfienlem2	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑇 ) → ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ◡ 𝐹 ) finSupp 𝑍 )
32		breq1	⊢ ( 𝑥 = ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ◡ 𝐹 ) → ( 𝑥 finSupp 𝑍 ↔ ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ◡ 𝐹 ) finSupp 𝑍 ) )
33	32 1	elrab2	⊢ ( ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ◡ 𝐹 ) ∈ 𝑆 ↔ ( ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ◡ 𝐹 ) ∈ ( 𝐵 ↑m 𝐴 ) ∧ ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ◡ 𝐹 ) finSupp 𝑍 ) )
34	30 31 33	sylanbrc	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑇 ) → ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ◡ 𝐹 ) ∈ 𝑆 )