Metamath Proof Explorer

Theorem imasaddflem

Description: The image set operations are closed if the original operation is. (Contributed by Mario Carneiro, 23-Feb-2015)

Ref Expression
Hypotheses imasaddf.f ⊢ ( 𝜑 → 𝐹 : 𝑉 –onto→ 𝐵 )
imasaddf.e ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) ) → ( ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( 𝐹 ‘ ( 𝑎 · 𝑏 ) ) = ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) )
imasaddflem.a ⊢ ( 𝜑 → ∙ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ⟩ } )
imasaddflem.c ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) ) → ( 𝑝 · 𝑞 ) ∈ 𝑉 )
Assertion imasaddflem ( 𝜑 → ∙ : ( 𝐵 × 𝐵 ) ⟶ 𝐵 )

Proof

Step Hyp Ref Expression
1 imasaddf.f ⊢ ( 𝜑 → 𝐹 : 𝑉 –onto→ 𝐵 )
2 imasaddf.e ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) ) → ( ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( 𝐹 ‘ ( 𝑎 · 𝑏 ) ) = ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) )
3 imasaddflem.a ⊢ ( 𝜑 → ∙ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ⟩ } )
4 imasaddflem.c ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) ) → ( 𝑝 · 𝑞 ) ∈ 𝑉 )
5 1 2 3 imasaddfnlem ⊢ ( 𝜑 → ∙ Fn ( 𝐵 × 𝐵 ) )
6 fof ⊢ ( 𝐹 : 𝑉 –onto→ 𝐵 → 𝐹 : 𝑉 ⟶ 𝐵 )
7 1 6 syl ⊢ ( 𝜑 → 𝐹 : 𝑉 ⟶ 𝐵 )
8 ffvelrn ⊢ ( ( 𝐹 : 𝑉 ⟶ 𝐵 ∧ 𝑝 ∈ 𝑉 ) → ( 𝐹 ‘ 𝑝 ) ∈ 𝐵 )
9 ffvelrn ⊢ ( ( 𝐹 : 𝑉 ⟶ 𝐵 ∧ 𝑞 ∈ 𝑉 ) → ( 𝐹 ‘ 𝑞 ) ∈ 𝐵 )
10 8 9 anim12dan ⊢ ( ( 𝐹 : 𝑉 ⟶ 𝐵 ∧ ( 𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) ) → ( ( 𝐹 ‘ 𝑝 ) ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑞 ) ∈ 𝐵 ) )
11 opelxpi ⊢ ( ( ( 𝐹 ‘ 𝑝 ) ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑞 ) ∈ 𝐵 ) → ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ ∈ ( 𝐵 × 𝐵 ) )
12 10 11 syl ⊢ ( ( 𝐹 : 𝑉 ⟶ 𝐵 ∧ ( 𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) ) → ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ ∈ ( 𝐵 × 𝐵 ) )
13 7 12 sylan ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) ) → ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ ∈ ( 𝐵 × 𝐵 ) )
14 ffvelrn ⊢ ( ( 𝐹 : 𝑉 ⟶ 𝐵 ∧ ( 𝑝 · 𝑞 ) ∈ 𝑉 ) → ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ∈ 𝐵 )
15 7 4 14 syl2an2r ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) ) → ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ∈ 𝐵 )
16 13 15 opelxpd ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) ) → ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ⟩ ∈ ( ( 𝐵 × 𝐵 ) × 𝐵 ) )
17 16 snssd ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) ) → { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ⟩ } ⊆ ( ( 𝐵 × 𝐵 ) × 𝐵 ) )
18 17 anassrs ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑉 ) ∧ 𝑞 ∈ 𝑉 ) → { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ⟩ } ⊆ ( ( 𝐵 × 𝐵 ) × 𝐵 ) )
19 18 iunssd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑉 ) → ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ⟩ } ⊆ ( ( 𝐵 × 𝐵 ) × 𝐵 ) )
20 19 iunssd ⊢ ( 𝜑 → ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ⟩ } ⊆ ( ( 𝐵 × 𝐵 ) × 𝐵 ) )
21 3 20 eqsstrd ⊢ ( 𝜑 → ∙ ⊆ ( ( 𝐵 × 𝐵 ) × 𝐵 ) )
22 dff2 ⊢ ( ∙ : ( 𝐵 × 𝐵 ) ⟶ 𝐵 ↔ ( ∙ Fn ( 𝐵 × 𝐵 ) ∧ ∙ ⊆ ( ( 𝐵 × 𝐵 ) × 𝐵 ) ) )
23 5 21 22 sylanbrc ⊢ ( 𝜑 → ∙ : ( 𝐵 × 𝐵 ) ⟶ 𝐵 )