Theorem rnmposs

Description: The range of an operation given by the maps-to notation as a subset. (Contributed by Thierry Arnoux, 23-May-2017)

	Ref	Expression
Hypothesis	rnmposs.1	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 )
Assertion	rnmposs	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 → ran 𝐹 ⊆ 𝐷 )

Proof

Step	Hyp	Ref	Expression
1		rnmposs.1	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 )
2	1	rnmpo	⊢ ran 𝐹 = { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑧 = 𝐶 }
3	2	eqabri	⊢ ( 𝑧 ∈ ran 𝐹 ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑧 = 𝐶 )
4		2r19.29	⊢ ( ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 ∧ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑧 = 𝐶 ) → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝐶 ∈ 𝐷 ∧ 𝑧 = 𝐶 ) )
5		eleq1	⊢ ( 𝑧 = 𝐶 → ( 𝑧 ∈ 𝐷 ↔ 𝐶 ∈ 𝐷 ) )
6	5	biimparc	⊢ ( ( 𝐶 ∈ 𝐷 ∧ 𝑧 = 𝐶 ) → 𝑧 ∈ 𝐷 )
7	6	a1i	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝐶 ∈ 𝐷 ∧ 𝑧 = 𝐶 ) → 𝑧 ∈ 𝐷 ) )
8	7	rexlimivv	⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝐶 ∈ 𝐷 ∧ 𝑧 = 𝐶 ) → 𝑧 ∈ 𝐷 )
9	4 8	syl	⊢ ( ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 ∧ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑧 = 𝐶 ) → 𝑧 ∈ 𝐷 )
10	9	ex	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 → ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑧 = 𝐶 → 𝑧 ∈ 𝐷 ) )
11	3 10	biimtrid	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 → ( 𝑧 ∈ ran 𝐹 → 𝑧 ∈ 𝐷 ) )
12	11	ssrdv	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 → ran 𝐹 ⊆ 𝐷 )