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

Metamath Proof Explorer

Theorem fnasrn

Description: A function expressed as the range of another function. (Contributed by Mario Carneiro, 22-Jun-2013) (Proof shortened by Mario Carneiro, 31-Aug-2015)

Ref Expression
Hypothesis dfmpt.1 ⊢ 𝐵 ∈ V
Assertion fnasrn ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ran ( 𝑥 ∈ 𝐴 ↦ ⟨ 𝑥 , 𝐵 ⟩ )

Proof

Step Hyp Ref Expression
1 dfmpt.1 ⊢ 𝐵 ∈ V
2 1 dfmpt ⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ∪ 𝑥 ∈ 𝐴 { ⟨ 𝑥 , 𝐵 ⟩ }
3 eqid ⊢ ( 𝑥 ∈ 𝐴 ↦ ⟨ 𝑥 , 𝐵 ⟩ ) = ( 𝑥 ∈ 𝐴 ↦ ⟨ 𝑥 , 𝐵 ⟩ )
4 3 rnmpt ⊢ ran ( 𝑥 ∈ 𝐴 ↦ ⟨ 𝑥 , 𝐵 ⟩ ) = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ⟨ 𝑥 , 𝐵 ⟩ }
5 velsn ⊢ ( 𝑦 ∈ { ⟨ 𝑥 , 𝐵 ⟩ } ↔ 𝑦 = ⟨ 𝑥 , 𝐵 ⟩ )
6 5 rexbii ⊢ ( ∃ 𝑥 ∈ 𝐴 𝑦 ∈ { ⟨ 𝑥 , 𝐵 ⟩ } ↔ ∃ 𝑥 ∈ 𝐴 𝑦 = ⟨ 𝑥 , 𝐵 ⟩ )
7 6 abbii ⊢ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ { ⟨ 𝑥 , 𝐵 ⟩ } } = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ⟨ 𝑥 , 𝐵 ⟩ }
8 4 7 eqtr4i ⊢ ran ( 𝑥 ∈ 𝐴 ↦ ⟨ 𝑥 , 𝐵 ⟩ ) = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ { ⟨ 𝑥 , 𝐵 ⟩ } }
9 df-iun ⊢ ∪ 𝑥 ∈ 𝐴 { ⟨ 𝑥 , 𝐵 ⟩ } = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ { ⟨ 𝑥 , 𝐵 ⟩ } }
10 8 9 eqtr4i ⊢ ran ( 𝑥 ∈ 𝐴 ↦ ⟨ 𝑥 , 𝐵 ⟩ ) = ∪ 𝑥 ∈ 𝐴 { ⟨ 𝑥 , 𝐵 ⟩ }
11 2 10 eqtr4i ⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ran ( 𝑥 ∈ 𝐴 ↦ ⟨ 𝑥 , 𝐵 ⟩ )