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 ( 𝑋 × 𝑌 ) )