Theorem rexunirn

Description: Restricted existential quantification over the union of the range of a function. Cf. rexrn and eluni2 . (Contributed by Thierry Arnoux, 19-Sep-2017)

	Ref	Expression
Hypotheses	rexunirn.1	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
	rexunirn.2	⊢ ( 𝑥 ∈ 𝐴 → 𝐵 ∈ 𝑉 )
Assertion	rexunirn	⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 → ∃ 𝑦 ∈ ∪ ran 𝐹 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		rexunirn.1	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
2		rexunirn.2	⊢ ( 𝑥 ∈ 𝐴 → 𝐵 ∈ 𝑉 )
3		df-rex	⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 ∈ 𝐵 𝜑 ) )
4		19.42v	⊢ ( ∃ 𝑦 ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) )
5		df-rex	⊢ ( ∃ 𝑦 ∈ 𝐵 𝜑 ↔ ∃ 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) )
6	5	anbi2i	⊢ ( ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 ∈ 𝐵 𝜑 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) )
7	4 6	bitr4i	⊢ ( ∃ 𝑦 ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 ∈ 𝐵 𝜑 ) )
8	7	exbii	⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 ∈ 𝐵 𝜑 ) )
9	3 8	bitr4i	⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) )
10	1	elrnmpt1	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉 ) → 𝐵 ∈ ran 𝐹 )
11	2 10	mpdan	⊢ ( 𝑥 ∈ 𝐴 → 𝐵 ∈ ran 𝐹 )
12		eleq2	⊢ ( 𝑏 = 𝐵 → ( 𝑦 ∈ 𝑏 ↔ 𝑦 ∈ 𝐵 ) )
13	12	anbi1d	⊢ ( 𝑏 = 𝐵 → ( ( 𝑦 ∈ 𝑏 ∧ 𝜑 ) ↔ ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) )
14	13	rspcev	⊢ ( ( 𝐵 ∈ ran 𝐹 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) → ∃ 𝑏 ∈ ran 𝐹 ( 𝑦 ∈ 𝑏 ∧ 𝜑 ) )
15	11 14	sylan	⊢ ( ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) → ∃ 𝑏 ∈ ran 𝐹 ( 𝑦 ∈ 𝑏 ∧ 𝜑 ) )
16		r19.41v	⊢ ( ∃ 𝑏 ∈ ran 𝐹 ( 𝑦 ∈ 𝑏 ∧ 𝜑 ) ↔ ( ∃ 𝑏 ∈ ran 𝐹 𝑦 ∈ 𝑏 ∧ 𝜑 ) )
17	15 16	sylib	⊢ ( ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) → ( ∃ 𝑏 ∈ ran 𝐹 𝑦 ∈ 𝑏 ∧ 𝜑 ) )
18	17	eximi	⊢ ( ∃ 𝑦 ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) → ∃ 𝑦 ( ∃ 𝑏 ∈ ran 𝐹 𝑦 ∈ 𝑏 ∧ 𝜑 ) )
19		df-rex	⊢ ( ∃ 𝑦 ∈ ∪ ran 𝐹 𝜑 ↔ ∃ 𝑦 ( 𝑦 ∈ ∪ ran 𝐹 ∧ 𝜑 ) )
20		eluni2	⊢ ( 𝑦 ∈ ∪ ran 𝐹 ↔ ∃ 𝑏 ∈ ran 𝐹 𝑦 ∈ 𝑏 )
21	20	anbi1i	⊢ ( ( 𝑦 ∈ ∪ ran 𝐹 ∧ 𝜑 ) ↔ ( ∃ 𝑏 ∈ ran 𝐹 𝑦 ∈ 𝑏 ∧ 𝜑 ) )
22	21	exbii	⊢ ( ∃ 𝑦 ( 𝑦 ∈ ∪ ran 𝐹 ∧ 𝜑 ) ↔ ∃ 𝑦 ( ∃ 𝑏 ∈ ran 𝐹 𝑦 ∈ 𝑏 ∧ 𝜑 ) )
23	19 22	bitri	⊢ ( ∃ 𝑦 ∈ ∪ ran 𝐹 𝜑 ↔ ∃ 𝑦 ( ∃ 𝑏 ∈ ran 𝐹 𝑦 ∈ 𝑏 ∧ 𝜑 ) )
24	18 23	sylibr	⊢ ( ∃ 𝑦 ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) → ∃ 𝑦 ∈ ∪ ran 𝐹 𝜑 )
25	24	exlimiv	⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) → ∃ 𝑦 ∈ ∪ ran 𝐹 𝜑 )
26	9 25	sylbi	⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 → ∃ 𝑦 ∈ ∪ ran 𝐹 𝜑 )