Metamath Proof Explorer


Theorem mapfienlem2

Description: Lemma 2 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 mapfienlem2 ( ( 𝜑𝑔𝑇 ) → ( ( 𝐺𝑔 ) ∘ 𝐹 ) finSupp 𝑍 )

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 10 adantr ( ( 𝜑𝑔𝑇 ) → 𝑍𝐵 )
12 f1of ( 𝐺 : 𝐵1-1-onto𝐷𝐺 : 𝐵𝐷 )
13 5 12 syl ( 𝜑𝐺 : 𝐵𝐷 )
14 13 10 ffvelrnd ( 𝜑 → ( 𝐺𝑍 ) ∈ 𝐷 )
15 3 14 eqeltrid ( 𝜑𝑊𝐷 )
16 15 adantr ( ( 𝜑𝑔𝑇 ) → 𝑊𝐷 )
17 elrabi ( 𝑔 ∈ { 𝑥 ∈ ( 𝐷m 𝐶 ) ∣ 𝑥 finSupp 𝑊 } → 𝑔 ∈ ( 𝐷m 𝐶 ) )
18 elmapi ( 𝑔 ∈ ( 𝐷m 𝐶 ) → 𝑔 : 𝐶𝐷 )
19 17 18 syl ( 𝑔 ∈ { 𝑥 ∈ ( 𝐷m 𝐶 ) ∣ 𝑥 finSupp 𝑊 } → 𝑔 : 𝐶𝐷 )
20 19 2 eleq2s ( 𝑔𝑇𝑔 : 𝐶𝐷 )
21 20 adantl ( ( 𝜑𝑔𝑇 ) → 𝑔 : 𝐶𝐷 )
22 f1ocnv ( 𝐺 : 𝐵1-1-onto𝐷 𝐺 : 𝐷1-1-onto𝐵 )
23 f1of ( 𝐺 : 𝐷1-1-onto𝐵 𝐺 : 𝐷𝐵 )
24 5 22 23 3syl ( 𝜑 𝐺 : 𝐷𝐵 )
25 24 adantr ( ( 𝜑𝑔𝑇 ) → 𝐺 : 𝐷𝐵 )
26 ssidd ( ( 𝜑𝑔𝑇 ) → 𝐷𝐷 )
27 8 adantr ( ( 𝜑𝑔𝑇 ) → 𝐶𝑋 )
28 9 adantr ( ( 𝜑𝑔𝑇 ) → 𝐷𝑌 )
29 breq1 ( 𝑥 = 𝑔 → ( 𝑥 finSupp 𝑊𝑔 finSupp 𝑊 ) )
30 29 elrab ( 𝑔 ∈ { 𝑥 ∈ ( 𝐷m 𝐶 ) ∣ 𝑥 finSupp 𝑊 } ↔ ( 𝑔 ∈ ( 𝐷m 𝐶 ) ∧ 𝑔 finSupp 𝑊 ) )
31 30 simprbi ( 𝑔 ∈ { 𝑥 ∈ ( 𝐷m 𝐶 ) ∣ 𝑥 finSupp 𝑊 } → 𝑔 finSupp 𝑊 )
32 31 2 eleq2s ( 𝑔𝑇𝑔 finSupp 𝑊 )
33 32 adantl ( ( 𝜑𝑔𝑇 ) → 𝑔 finSupp 𝑊 )
34 5 10 jca ( 𝜑 → ( 𝐺 : 𝐵1-1-onto𝐷𝑍𝐵 ) )
35 3 eqcomi ( 𝐺𝑍 ) = 𝑊
36 34 35 jctir ( 𝜑 → ( ( 𝐺 : 𝐵1-1-onto𝐷𝑍𝐵 ) ∧ ( 𝐺𝑍 ) = 𝑊 ) )
37 36 adantr ( ( 𝜑𝑔𝑇 ) → ( ( 𝐺 : 𝐵1-1-onto𝐷𝑍𝐵 ) ∧ ( 𝐺𝑍 ) = 𝑊 ) )
38 f1ocnvfv ( ( 𝐺 : 𝐵1-1-onto𝐷𝑍𝐵 ) → ( ( 𝐺𝑍 ) = 𝑊 → ( 𝐺𝑊 ) = 𝑍 ) )
39 38 imp ( ( ( 𝐺 : 𝐵1-1-onto𝐷𝑍𝐵 ) ∧ ( 𝐺𝑍 ) = 𝑊 ) → ( 𝐺𝑊 ) = 𝑍 )
40 37 39 syl ( ( 𝜑𝑔𝑇 ) → ( 𝐺𝑊 ) = 𝑍 )
41 11 16 21 25 26 27 28 33 40 fsuppcor ( ( 𝜑𝑔𝑇 ) → ( 𝐺𝑔 ) finSupp 𝑍 )
42 f1ocnv ( 𝐹 : 𝐶1-1-onto𝐴 𝐹 : 𝐴1-1-onto𝐶 )
43 f1of1 ( 𝐹 : 𝐴1-1-onto𝐶 𝐹 : 𝐴1-1𝐶 )
44 4 42 43 3syl ( 𝜑 𝐹 : 𝐴1-1𝐶 )
45 44 adantr ( ( 𝜑𝑔𝑇 ) → 𝐹 : 𝐴1-1𝐶 )
46 13 7 jca ( 𝜑 → ( 𝐺 : 𝐵𝐷𝐵𝑉 ) )
47 fex ( ( 𝐺 : 𝐵𝐷𝐵𝑉 ) → 𝐺 ∈ V )
48 cnvexg ( 𝐺 ∈ V → 𝐺 ∈ V )
49 46 47 48 3syl ( 𝜑 𝐺 ∈ V )
50 coexg ( ( 𝐺 ∈ V ∧ 𝑔𝑇 ) → ( 𝐺𝑔 ) ∈ V )
51 49 50 sylan ( ( 𝜑𝑔𝑇 ) → ( 𝐺𝑔 ) ∈ V )
52 41 45 11 51 fsuppco ( ( 𝜑𝑔𝑇 ) → ( ( 𝐺𝑔 ) ∘ 𝐹 ) finSupp 𝑍 )