Theorem ex-rn

Description: Example for df-rn . Example by David A. Wheeler. (Contributed by Mario Carneiro, 7-May-2015)

	Ref	Expression
Assertion	ex-rn	⊢ ( 𝐹 = { ⟨ 2 , 6 ⟩ , ⟨ 3 , 9 ⟩ } → ran 𝐹 = { 6 , 9 } )

Proof

Step	Hyp	Ref	Expression
1		rneq	⊢ ( 𝐹 = { ⟨ 2 , 6 ⟩ , ⟨ 3 , 9 ⟩ } → ran 𝐹 = ran { ⟨ 2 , 6 ⟩ , ⟨ 3 , 9 ⟩ } )
2		df-pr	⊢ { ⟨ 2 , 6 ⟩ , ⟨ 3 , 9 ⟩ } = ( { ⟨ 2 , 6 ⟩ } ∪ { ⟨ 3 , 9 ⟩ } )
3	2	rneqi	⊢ ran { ⟨ 2 , 6 ⟩ , ⟨ 3 , 9 ⟩ } = ran ( { ⟨ 2 , 6 ⟩ } ∪ { ⟨ 3 , 9 ⟩ } )
4		rnun	⊢ ran ( { ⟨ 2 , 6 ⟩ } ∪ { ⟨ 3 , 9 ⟩ } ) = ( ran { ⟨ 2 , 6 ⟩ } ∪ ran { ⟨ 3 , 9 ⟩ } )
5		2nn	⊢ 2 ∈ ℕ
6	5	elexi	⊢ 2 ∈ V
7	6	rnsnop	⊢ ran { ⟨ 2 , 6 ⟩ } = { 6 }
8		3nn	⊢ 3 ∈ ℕ
9	8	elexi	⊢ 3 ∈ V
10	9	rnsnop	⊢ ran { ⟨ 3 , 9 ⟩ } = { 9 }
11	7 10	uneq12i	⊢ ( ran { ⟨ 2 , 6 ⟩ } ∪ ran { ⟨ 3 , 9 ⟩ } ) = ( { 6 } ∪ { 9 } )
12		df-pr	⊢ { 6 , 9 } = ( { 6 } ∪ { 9 } )
13	11 12	eqtr4i	⊢ ( ran { ⟨ 2 , 6 ⟩ } ∪ ran { ⟨ 3 , 9 ⟩ } ) = { 6 , 9 }
14	3 4 13	3eqtri	⊢ ran { ⟨ 2 , 6 ⟩ , ⟨ 3 , 9 ⟩ } = { 6 , 9 }
15	1 14	eqtrdi	⊢ ( 𝐹 = { ⟨ 2 , 6 ⟩ , ⟨ 3 , 9 ⟩ } → ran 𝐹 = { 6 , 9 } )