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

Metamath Proof Explorer

Theorem rnmposs

Description: The range of an operation given by the maps-to notation as a subset. (Contributed by Thierry Arnoux, 23-May-2017)

Ref Expression
Hypothesis rnmposs.1 ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 )
Assertion rnmposs ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 → ran 𝐹 ⊆ 𝐷 )

Proof

Step Hyp Ref Expression
1 rnmposs.1 ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 )
2 1 rnmpo ⊢ ran 𝐹 = { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑧 = 𝐶 }
3 2 eqabri ⊢ ( 𝑧 ∈ ran 𝐹 ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑧 = 𝐶 )
4 2r19.29 ⊢ ( ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 ∧ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑧 = 𝐶 ) → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝐶 ∈ 𝐷 ∧ 𝑧 = 𝐶 ) )
5 eleq1 ⊢ ( 𝑧 = 𝐶 → ( 𝑧 ∈ 𝐷 ↔ 𝐶 ∈ 𝐷 ) )
6 5 biimparc ⊢ ( ( 𝐶 ∈ 𝐷 ∧ 𝑧 = 𝐶 ) → 𝑧 ∈ 𝐷 )
7 6 a1i ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝐶 ∈ 𝐷 ∧ 𝑧 = 𝐶 ) → 𝑧 ∈ 𝐷 ) )
8 7 rexlimivv ⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝐶 ∈ 𝐷 ∧ 𝑧 = 𝐶 ) → 𝑧 ∈ 𝐷 )
9 4 8 syl ⊢ ( ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 ∧ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑧 = 𝐶 ) → 𝑧 ∈ 𝐷 )
10 9 ex ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 → ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑧 = 𝐶 → 𝑧 ∈ 𝐷 ) )
11 3 10 biimtrid ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 → ( 𝑧 ∈ ran 𝐹 → 𝑧 ∈ 𝐷 ) )
12 11 ssrdv ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 → ran 𝐹 ⊆ 𝐷 )