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

Metamath Proof Explorer

Theorem rnmptbd2lem

Description: Boundness below of the range of a function in maps-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses rnmptbd2lem.x ⊢ Ⅎ 𝑥 𝜑
rnmptbd2lem.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
Assertion rnmptbd2lem ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝑦 ≤ 𝐵 ↔ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑦 ≤ 𝑧 ) )

Proof

Step Hyp Ref Expression
1 rnmptbd2lem.x ⊢ Ⅎ 𝑥 𝜑
2 rnmptbd2lem.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
3 eqid ⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
4 3 elrnmpt ⊢ ( 𝑧 ∈ V → ( 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 ) )
5 4 elv ⊢ ( 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 )
6 nfra1 ⊢ Ⅎ 𝑥 ∀ 𝑥 ∈ 𝐴 𝑦 ≤ 𝐵
7 nfv ⊢ Ⅎ 𝑥 𝑦 ≤ 𝑧
8 rspa ⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝑦 ≤ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → 𝑦 ≤ 𝐵 )
9 simpl ⊢ ( ( 𝑦 ≤ 𝐵 ∧ 𝑧 = 𝐵 ) → 𝑦 ≤ 𝐵 )
10 id ⊢ ( 𝑧 = 𝐵 → 𝑧 = 𝐵 )
11 10 eqcomd ⊢ ( 𝑧 = 𝐵 → 𝐵 = 𝑧 )
12 11 adantl ⊢ ( ( 𝑦 ≤ 𝐵 ∧ 𝑧 = 𝐵 ) → 𝐵 = 𝑧 )
13 9 12 breqtrd ⊢ ( ( 𝑦 ≤ 𝐵 ∧ 𝑧 = 𝐵 ) → 𝑦 ≤ 𝑧 )
14 13 ex ⊢ ( 𝑦 ≤ 𝐵 → ( 𝑧 = 𝐵 → 𝑦 ≤ 𝑧 ) )
15 8 14 syl ⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝑦 ≤ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑧 = 𝐵 → 𝑦 ≤ 𝑧 ) )
16 15 ex ⊢ ( ∀ 𝑥 ∈ 𝐴 𝑦 ≤ 𝐵 → ( 𝑥 ∈ 𝐴 → ( 𝑧 = 𝐵 → 𝑦 ≤ 𝑧 ) ) )
17 6 7 16 rexlimd ⊢ ( ∀ 𝑥 ∈ 𝐴 𝑦 ≤ 𝐵 → ( ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 → 𝑦 ≤ 𝑧 ) )
18 17 imp ⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝑦 ≤ 𝐵 ∧ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 ) → 𝑦 ≤ 𝑧 )
19 18 adantll ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 𝑦 ≤ 𝐵 ) ∧ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 ) → 𝑦 ≤ 𝑧 )
20 5 19 sylan2b ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 𝑦 ≤ 𝐵 ) ∧ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) → 𝑦 ≤ 𝑧 )
21 20 ralrimiva ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 𝑦 ≤ 𝐵 ) → ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑦 ≤ 𝑧 )
22 21 ex ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐴 𝑦 ≤ 𝐵 → ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑦 ≤ 𝑧 ) )
23 22 reximdv ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝑦 ≤ 𝐵 → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑦 ≤ 𝑧 ) )
24 nfmpt1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
25 24 nfrn ⊢ Ⅎ 𝑥 ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
26 25 7 nfralw ⊢ Ⅎ 𝑥 ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑦 ≤ 𝑧
27 1 26 nfan ⊢ Ⅎ 𝑥 ( 𝜑 ∧ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑦 ≤ 𝑧 )
28 breq2 ⊢ ( 𝑧 = 𝐵 → ( 𝑦 ≤ 𝑧 ↔ 𝑦 ≤ 𝐵 ) )
29 simplr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑦 ≤ 𝑧 ) ∧ 𝑥 ∈ 𝐴 ) → ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑦 ≤ 𝑧 )
30 simpr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑦 ≤ 𝑧 ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
31 2 adantlr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑦 ≤ 𝑧 ) ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
32 3 30 31 elrnmpt1d ⊢ ( ( ( 𝜑 ∧ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑦 ≤ 𝑧 ) ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
33 28 29 32 rspcdva ⊢ ( ( ( 𝜑 ∧ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑦 ≤ 𝑧 ) ∧ 𝑥 ∈ 𝐴 ) → 𝑦 ≤ 𝐵 )
34 27 33 ralrimia ⊢ ( ( 𝜑 ∧ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑦 ≤ 𝑧 ) → ∀ 𝑥 ∈ 𝐴 𝑦 ≤ 𝐵 )
35 34 ex ⊢ ( 𝜑 → ( ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑦 ≤ 𝑧 → ∀ 𝑥 ∈ 𝐴 𝑦 ≤ 𝐵 ) )
36 35 reximdv ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑦 ≤ 𝑧 → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝑦 ≤ 𝐵 ) )
37 23 36 impbid ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝑦 ≤ 𝐵 ↔ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑦 ≤ 𝑧 ) )