Theorem iunrnmptss

Description: A subset relation for an indexed union over the range of function expressed as a mapping. (Contributed by Thierry Arnoux, 27-Mar-2018)

	Ref	Expression
Hypotheses	iunrnmptss.1	⊢ ( 𝑦 = 𝐵 → 𝐶 = 𝐷 )
	iunrnmptss.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
Assertion	iunrnmptss	⊢ ( 𝜑 → ∪ 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐷 )

Proof

Step	Hyp	Ref	Expression
1		iunrnmptss.1	⊢ ( 𝑦 = 𝐵 → 𝐶 = 𝐷 )
2		iunrnmptss.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
3		df-rex	⊢ ( ∃ 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ∈ 𝐶 ↔ ∃ 𝑦 ( 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∧ 𝑧 ∈ 𝐶 ) )
4	2	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 )
5		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
6	5	elrnmptg	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ( 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 ) )
7	4 6	syl	⊢ ( 𝜑 → ( 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 ) )
8	7	anbi1d	⊢ ( 𝜑 → ( ( 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∧ 𝑧 ∈ 𝐶 ) ↔ ( ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 ∧ 𝑧 ∈ 𝐶 ) ) )
9	8	exbidv	⊢ ( 𝜑 → ( ∃ 𝑦 ( 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∧ 𝑧 ∈ 𝐶 ) ↔ ∃ 𝑦 ( ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 ∧ 𝑧 ∈ 𝐶 ) ) )
10		r19.41v	⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝑦 = 𝐵 ∧ 𝑧 ∈ 𝐶 ) ↔ ( ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 ∧ 𝑧 ∈ 𝐶 ) )
11	1	eleq2d	⊢ ( 𝑦 = 𝐵 → ( 𝑧 ∈ 𝐶 ↔ 𝑧 ∈ 𝐷 ) )
12	11	biimpa	⊢ ( ( 𝑦 = 𝐵 ∧ 𝑧 ∈ 𝐶 ) → 𝑧 ∈ 𝐷 )
13	12	reximi	⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝑦 = 𝐵 ∧ 𝑧 ∈ 𝐶 ) → ∃ 𝑥 ∈ 𝐴 𝑧 ∈ 𝐷 )
14	10 13	sylbir	⊢ ( ( ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 ∧ 𝑧 ∈ 𝐶 ) → ∃ 𝑥 ∈ 𝐴 𝑧 ∈ 𝐷 )
15	14	exlimiv	⊢ ( ∃ 𝑦 ( ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 ∧ 𝑧 ∈ 𝐶 ) → ∃ 𝑥 ∈ 𝐴 𝑧 ∈ 𝐷 )
16	9 15	syl6bi	⊢ ( 𝜑 → ( ∃ 𝑦 ( 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∧ 𝑧 ∈ 𝐶 ) → ∃ 𝑥 ∈ 𝐴 𝑧 ∈ 𝐷 ) )
17	3 16	syl5bi	⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ∈ 𝐶 → ∃ 𝑥 ∈ 𝐴 𝑧 ∈ 𝐷 ) )
18	17	ss2abdv	⊢ ( 𝜑 → { 𝑧 ∣ ∃ 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ∈ 𝐶 } ⊆ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 ∈ 𝐷 } )
19		df-iun	⊢ ∪ 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝐶 = { 𝑧 ∣ ∃ 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ∈ 𝐶 }
20		df-iun	⊢ ∪ 𝑥 ∈ 𝐴 𝐷 = { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 ∈ 𝐷 }
21	18 19 20	3sstr4g	⊢ ( 𝜑 → ∪ 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐷 )