Theorem fmpo

Description: Functionality, domain and range of a class given by the maps-to notation. (Contributed by FL, 17-May-2010)

	Ref	Expression
Hypothesis	fmpo.1	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 )
Assertion	fmpo	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 ↔ 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐷 )

Proof

Step	Hyp	Ref	Expression
1		fmpo.1	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 )
2	1	fmpox	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 ↔ 𝐹 : ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ⟶ 𝐷 )
3		iunxpconst	⊢ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) = ( 𝐴 × 𝐵 )
4	3	feq2i	⊢ ( 𝐹 : ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ⟶ 𝐷 ↔ 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐷 )
5	2 4	bitri	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 ↔ 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐷 )