Metamath Proof Explorer


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 ( ( 𝜑𝑔𝑇 ) → ( ( 𝐺𝑔 ) ∘ 𝐹 ) ∈ 𝑆 )