Theorem rnmptpr

Description: Range of a function defined on an unordered pair. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	rnmptpr.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	rnmptpr.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
	rnmptpr.f	⊢ 𝐹 = ( 𝑥 ∈ { 𝐴 , 𝐵 } ↦ 𝐶 )
	rnmptpr.d	⊢ ( 𝑥 = 𝐴 → 𝐶 = 𝐷 )
	rnmptpr.e	⊢ ( 𝑥 = 𝐵 → 𝐶 = 𝐸 )
Assertion	rnmptpr	⊢ ( 𝜑 → ran 𝐹 = { 𝐷 , 𝐸 } )

Proof

Step	Hyp	Ref	Expression
1		rnmptpr.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		rnmptpr.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
3		rnmptpr.f	⊢ 𝐹 = ( 𝑥 ∈ { 𝐴 , 𝐵 } ↦ 𝐶 )
4		rnmptpr.d	⊢ ( 𝑥 = 𝐴 → 𝐶 = 𝐷 )
5		rnmptpr.e	⊢ ( 𝑥 = 𝐵 → 𝐶 = 𝐸 )
6	4	eqeq2d	⊢ ( 𝑥 = 𝐴 → ( 𝑦 = 𝐶 ↔ 𝑦 = 𝐷 ) )
7	5	eqeq2d	⊢ ( 𝑥 = 𝐵 → ( 𝑦 = 𝐶 ↔ 𝑦 = 𝐸 ) )
8	6 7	rexprg	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ∃ 𝑥 ∈ { 𝐴 , 𝐵 } 𝑦 = 𝐶 ↔ ( 𝑦 = 𝐷 ∨ 𝑦 = 𝐸 ) ) )
9	1 2 8	syl2anc	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ { 𝐴 , 𝐵 } 𝑦 = 𝐶 ↔ ( 𝑦 = 𝐷 ∨ 𝑦 = 𝐸 ) ) )
10	3	elrnmpt	⊢ ( 𝑦 ∈ V → ( 𝑦 ∈ ran 𝐹 ↔ ∃ 𝑥 ∈ { 𝐴 , 𝐵 } 𝑦 = 𝐶 ) )
11	10	elv	⊢ ( 𝑦 ∈ ran 𝐹 ↔ ∃ 𝑥 ∈ { 𝐴 , 𝐵 } 𝑦 = 𝐶 )
12		vex	⊢ 𝑦 ∈ V
13	12	elpr	⊢ ( 𝑦 ∈ { 𝐷 , 𝐸 } ↔ ( 𝑦 = 𝐷 ∨ 𝑦 = 𝐸 ) )
14	9 11 13	3bitr4g	⊢ ( 𝜑 → ( 𝑦 ∈ ran 𝐹 ↔ 𝑦 ∈ { 𝐷 , 𝐸 } ) )
15	14	eqrdv	⊢ ( 𝜑 → ran 𝐹 = { 𝐷 , 𝐸 } )