Metamath Proof Explorer


Theorem rnmptssbi

Description: The range of an operation given by the maps-to notation as a subset. (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypotheses rnmptssbi.1 𝑥 𝜑
rnmptssbi.2 𝐹 = ( 𝑥𝐴𝐵 )
rnmptssbi.3 ( ( 𝜑𝑥𝐴 ) → 𝐵𝑉 )
Assertion rnmptssbi ( 𝜑 → ( ran 𝐹𝐶 ↔ ∀ 𝑥𝐴 𝐵𝐶 ) )

Proof

Step Hyp Ref Expression
1 rnmptssbi.1 𝑥 𝜑
2 rnmptssbi.2 𝐹 = ( 𝑥𝐴𝐵 )
3 rnmptssbi.3 ( ( 𝜑𝑥𝐴 ) → 𝐵𝑉 )
4 nfmpt1 𝑥 ( 𝑥𝐴𝐵 )
5 2 4 nfcxfr 𝑥 𝐹
6 5 nfrn 𝑥 ran 𝐹
7 nfcv 𝑥 𝐶
8 6 7 nfss 𝑥 ran 𝐹𝐶
9 1 8 nfan 𝑥 ( 𝜑 ∧ ran 𝐹𝐶 )
10 simplr ( ( ( 𝜑 ∧ ran 𝐹𝐶 ) ∧ 𝑥𝐴 ) → ran 𝐹𝐶 )
11 simpr ( ( ( 𝜑 ∧ ran 𝐹𝐶 ) ∧ 𝑥𝐴 ) → 𝑥𝐴 )
12 3 adantlr ( ( ( 𝜑 ∧ ran 𝐹𝐶 ) ∧ 𝑥𝐴 ) → 𝐵𝑉 )
13 2 11 12 elrnmpt1d ( ( ( 𝜑 ∧ ran 𝐹𝐶 ) ∧ 𝑥𝐴 ) → 𝐵 ∈ ran 𝐹 )
14 10 13 sseldd ( ( ( 𝜑 ∧ ran 𝐹𝐶 ) ∧ 𝑥𝐴 ) → 𝐵𝐶 )
15 9 14 ralrimia ( ( 𝜑 ∧ ran 𝐹𝐶 ) → ∀ 𝑥𝐴 𝐵𝐶 )
16 2 rnmptss ( ∀ 𝑥𝐴 𝐵𝐶 → ran 𝐹𝐶 )
17 16 adantl ( ( 𝜑 ∧ ∀ 𝑥𝐴 𝐵𝐶 ) → ran 𝐹𝐶 )
18 15 17 impbida ( 𝜑 → ( ran 𝐹𝐶 ↔ ∀ 𝑥𝐴 𝐵𝐶 ) )