Step |
Hyp |
Ref |
Expression |
1 |
|
s1f1.1 |
⊢ ( 𝜑 → 𝐼 ∈ 𝐷 ) |
2 |
|
0nn0 |
⊢ 0 ∈ ℕ0 |
3 |
2
|
a1i |
⊢ ( 𝜑 → 0 ∈ ℕ0 ) |
4 |
|
f1osng |
⊢ ( ( 0 ∈ ℕ0 ∧ 𝐼 ∈ 𝐷 ) → { 〈 0 , 𝐼 〉 } : { 0 } –1-1-onto→ { 𝐼 } ) |
5 |
3 1 4
|
syl2anc |
⊢ ( 𝜑 → { 〈 0 , 𝐼 〉 } : { 0 } –1-1-onto→ { 𝐼 } ) |
6 |
|
f1of1 |
⊢ ( { 〈 0 , 𝐼 〉 } : { 0 } –1-1-onto→ { 𝐼 } → { 〈 0 , 𝐼 〉 } : { 0 } –1-1→ { 𝐼 } ) |
7 |
5 6
|
syl |
⊢ ( 𝜑 → { 〈 0 , 𝐼 〉 } : { 0 } –1-1→ { 𝐼 } ) |
8 |
1
|
snssd |
⊢ ( 𝜑 → { 𝐼 } ⊆ 𝐷 ) |
9 |
|
f1ss |
⊢ ( ( { 〈 0 , 𝐼 〉 } : { 0 } –1-1→ { 𝐼 } ∧ { 𝐼 } ⊆ 𝐷 ) → { 〈 0 , 𝐼 〉 } : { 0 } –1-1→ 𝐷 ) |
10 |
7 8 9
|
syl2anc |
⊢ ( 𝜑 → { 〈 0 , 𝐼 〉 } : { 0 } –1-1→ 𝐷 ) |
11 |
|
s1val |
⊢ ( 𝐼 ∈ 𝐷 → 〈“ 𝐼 ”〉 = { 〈 0 , 𝐼 〉 } ) |
12 |
1 11
|
syl |
⊢ ( 𝜑 → 〈“ 𝐼 ”〉 = { 〈 0 , 𝐼 〉 } ) |
13 |
|
s1dm |
⊢ dom 〈“ 𝐼 ”〉 = { 0 } |
14 |
13
|
a1i |
⊢ ( 𝜑 → dom 〈“ 𝐼 ”〉 = { 0 } ) |
15 |
|
eqidd |
⊢ ( 𝜑 → 𝐷 = 𝐷 ) |
16 |
12 14 15
|
f1eq123d |
⊢ ( 𝜑 → ( 〈“ 𝐼 ”〉 : dom 〈“ 𝐼 ”〉 –1-1→ 𝐷 ↔ { 〈 0 , 𝐼 〉 } : { 0 } –1-1→ 𝐷 ) ) |
17 |
10 16
|
mpbird |
⊢ ( 𝜑 → 〈“ 𝐼 ”〉 : dom 〈“ 𝐼 ”〉 –1-1→ 𝐷 ) |