Step |
Hyp |
Ref |
Expression |
1 |
|
ulmrel |
⊢ Rel ( ⇝𝑢 ‘ 𝑆 ) |
2 |
|
ulmuni |
⊢ ( ( 𝑥 ( ⇝𝑢 ‘ 𝑆 ) 𝑦 ∧ 𝑥 ( ⇝𝑢 ‘ 𝑆 ) 𝑧 ) → 𝑦 = 𝑧 ) |
3 |
2
|
ax-gen |
⊢ ∀ 𝑧 ( ( 𝑥 ( ⇝𝑢 ‘ 𝑆 ) 𝑦 ∧ 𝑥 ( ⇝𝑢 ‘ 𝑆 ) 𝑧 ) → 𝑦 = 𝑧 ) |
4 |
3
|
gen2 |
⊢ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ( ⇝𝑢 ‘ 𝑆 ) 𝑦 ∧ 𝑥 ( ⇝𝑢 ‘ 𝑆 ) 𝑧 ) → 𝑦 = 𝑧 ) |
5 |
|
dffun2 |
⊢ ( Fun ( ⇝𝑢 ‘ 𝑆 ) ↔ ( Rel ( ⇝𝑢 ‘ 𝑆 ) ∧ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ( ⇝𝑢 ‘ 𝑆 ) 𝑦 ∧ 𝑥 ( ⇝𝑢 ‘ 𝑆 ) 𝑧 ) → 𝑦 = 𝑧 ) ) ) |
6 |
1 4 5
|
mpbir2an |
⊢ Fun ( ⇝𝑢 ‘ 𝑆 ) |
7 |
|
funfvbrb |
⊢ ( Fun ( ⇝𝑢 ‘ 𝑆 ) → ( 𝐹 ∈ dom ( ⇝𝑢 ‘ 𝑆 ) ↔ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) ( ( ⇝𝑢 ‘ 𝑆 ) ‘ 𝐹 ) ) ) |
8 |
6 7
|
ax-mp |
⊢ ( 𝐹 ∈ dom ( ⇝𝑢 ‘ 𝑆 ) ↔ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) ( ( ⇝𝑢 ‘ 𝑆 ) ‘ 𝐹 ) ) |