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 𝐹 ⊆ 𝐶 ↔ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ) ) |