This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem imasubclem2

Description: Lemma for imasubc . (Contributed by Zhi Wang, 7-Nov-2025)

Ref Expression
Hypotheses imasubclem1.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
imasubclem1.g ⊢ ( 𝜑 → 𝐺 ∈ 𝑊 )
imasubclem2.k ⊢ 𝐾 = ( 𝑦 ∈ 𝑋 , 𝑧 ∈ 𝑌 ↦ ∪ 𝑥 ∈ ( ( ◡ 𝐹 “ 𝐴 ) × ( ◡ 𝐺 “ 𝐵 ) ) ( ( 𝐻 ‘ 𝐶 ) “ 𝐷 ) )
Assertion imasubclem2 ( 𝜑 → 𝐾 Fn ( 𝑋 × 𝑌 ) )

Proof

Step Hyp Ref Expression
1 imasubclem1.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
2 imasubclem1.g ⊢ ( 𝜑 → 𝐺 ∈ 𝑊 )
3 imasubclem2.k ⊢ 𝐾 = ( 𝑦 ∈ 𝑋 , 𝑧 ∈ 𝑌 ↦ ∪ 𝑥 ∈ ( ( ◡ 𝐹 “ 𝐴 ) × ( ◡ 𝐺 “ 𝐵 ) ) ( ( 𝐻 ‘ 𝐶 ) “ 𝐷 ) )
4 1 2 imasubclem1 ⊢ ( 𝜑 → ∪ 𝑥 ∈ ( ( ◡ 𝐹 “ 𝐴 ) × ( ◡ 𝐺 “ 𝐵 ) ) ( ( 𝐻 ‘ 𝐶 ) “ 𝐷 ) ∈ V )
5 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌 ) ) → ∪ 𝑥 ∈ ( ( ◡ 𝐹 “ 𝐴 ) × ( ◡ 𝐺 “ 𝐵 ) ) ( ( 𝐻 ‘ 𝐶 ) “ 𝐷 ) ∈ V )
6 5 ralrimivva ⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑌 ∪ 𝑥 ∈ ( ( ◡ 𝐹 “ 𝐴 ) × ( ◡ 𝐺 “ 𝐵 ) ) ( ( 𝐻 ‘ 𝐶 ) “ 𝐷 ) ∈ V )
7 3 fnmpo ⊢ ( ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑌 ∪ 𝑥 ∈ ( ( ◡ 𝐹 “ 𝐴 ) × ( ◡ 𝐺 “ 𝐵 ) ) ( ( 𝐻 ‘ 𝐶 ) “ 𝐷 ) ∈ V → 𝐾 Fn ( 𝑋 × 𝑌 ) )
8 6 7 syl ⊢ ( 𝜑 → 𝐾 Fn ( 𝑋 × 𝑌 ) )