This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐹 = { 𝐷 , 𝐸 } )