| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 1arymaptfv.h | . . 3
⊢ 𝐻 = (ℎ ∈ (1-aryF 𝑋) ↦ (𝑥 ∈ 𝑋 ↦ (ℎ‘{〈0, 𝑥〉}))) | 
| 2 | 1 | 1arymaptf 48562 | . 2
⊢ (𝑋 ∈ 𝑉 → 𝐻:(1-aryF 𝑋)⟶(𝑋 ↑m 𝑋)) | 
| 3 |  | elmapi 8889 | . . . . 5
⊢ (𝑓 ∈ (𝑋 ↑m 𝑋) → 𝑓:𝑋⟶𝑋) | 
| 4 |  | eqid 2737 | . . . . . 6
⊢ (𝑎 ∈ (𝑋 ↑m {0}) ↦ (𝑓‘(𝑎‘0))) = (𝑎 ∈ (𝑋 ↑m {0}) ↦ (𝑓‘(𝑎‘0))) | 
| 5 | 4 | 1arympt1 48559 | . . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑓:𝑋⟶𝑋) → (𝑎 ∈ (𝑋 ↑m {0}) ↦ (𝑓‘(𝑎‘0))) ∈ (1-aryF 𝑋)) | 
| 6 | 3, 5 | sylan2 593 | . . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑓 ∈ (𝑋 ↑m 𝑋)) → (𝑎 ∈ (𝑋 ↑m {0}) ↦ (𝑓‘(𝑎‘0))) ∈ (1-aryF 𝑋)) | 
| 7 |  | fveq2 6906 | . . . . . 6
⊢ (𝑔 = (𝑎 ∈ (𝑋 ↑m {0}) ↦ (𝑓‘(𝑎‘0))) → (𝐻‘𝑔) = (𝐻‘(𝑎 ∈ (𝑋 ↑m {0}) ↦ (𝑓‘(𝑎‘0))))) | 
| 8 | 7 | eqeq2d 2748 | . . . . 5
⊢ (𝑔 = (𝑎 ∈ (𝑋 ↑m {0}) ↦ (𝑓‘(𝑎‘0))) → (𝑓 = (𝐻‘𝑔) ↔ 𝑓 = (𝐻‘(𝑎 ∈ (𝑋 ↑m {0}) ↦ (𝑓‘(𝑎‘0)))))) | 
| 9 | 8 | adantl 481 | . . . 4
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑓 ∈ (𝑋 ↑m 𝑋)) ∧ 𝑔 = (𝑎 ∈ (𝑋 ↑m {0}) ↦ (𝑓‘(𝑎‘0)))) → (𝑓 = (𝐻‘𝑔) ↔ 𝑓 = (𝐻‘(𝑎 ∈ (𝑋 ↑m {0}) ↦ (𝑓‘(𝑎‘0)))))) | 
| 10 | 3 | adantl 481 | . . . . . 6
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑓 ∈ (𝑋 ↑m 𝑋)) → 𝑓:𝑋⟶𝑋) | 
| 11 | 10 | feqmptd 6977 | . . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑓 ∈ (𝑋 ↑m 𝑋)) → 𝑓 = (𝑥 ∈ 𝑋 ↦ (𝑓‘𝑥))) | 
| 12 |  | simplr 769 | . . . . . . . 8
⊢ ((((𝑋 ∈ 𝑉 ∧ 𝑓 ∈ (𝑋 ↑m 𝑋)) ∧ ℎ = (𝑎 ∈ (𝑋 ↑m {0}) ↦ (𝑓‘(𝑎‘0)))) ∧ 𝑥 ∈ 𝑋) → ℎ = (𝑎 ∈ (𝑋 ↑m {0}) ↦ (𝑓‘(𝑎‘0)))) | 
| 13 |  | fveq1 6905 | . . . . . . . . . . 11
⊢ (𝑎 = {〈0, 𝑥〉} → (𝑎‘0) = ({〈0, 𝑥〉}‘0)) | 
| 14 |  | c0ex 11255 | . . . . . . . . . . . 12
⊢ 0 ∈
V | 
| 15 |  | vex 3484 | . . . . . . . . . . . 12
⊢ 𝑥 ∈ V | 
| 16 | 14, 15 | fvsn 7201 | . . . . . . . . . . 11
⊢
({〈0, 𝑥〉}‘0) = 𝑥 | 
| 17 | 13, 16 | eqtrdi 2793 | . . . . . . . . . 10
⊢ (𝑎 = {〈0, 𝑥〉} → (𝑎‘0) = 𝑥) | 
| 18 | 17 | fveq2d 6910 | . . . . . . . . 9
⊢ (𝑎 = {〈0, 𝑥〉} → (𝑓‘(𝑎‘0)) = (𝑓‘𝑥)) | 
| 19 | 18 | adantl 481 | . . . . . . . 8
⊢
(((((𝑋 ∈ 𝑉 ∧ 𝑓 ∈ (𝑋 ↑m 𝑋)) ∧ ℎ = (𝑎 ∈ (𝑋 ↑m {0}) ↦ (𝑓‘(𝑎‘0)))) ∧ 𝑥 ∈ 𝑋) ∧ 𝑎 = {〈0, 𝑥〉}) → (𝑓‘(𝑎‘0)) = (𝑓‘𝑥)) | 
| 20 | 14 | a1i 11 | . . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑥 ∈ 𝑋) → 0 ∈ V) | 
| 21 |  | simpr 484 | . . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑋) | 
| 22 | 20, 21 | fsnd 6891 | . . . . . . . . . 10
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑥 ∈ 𝑋) → {〈0, 𝑥〉}:{0}⟶𝑋) | 
| 23 |  | snex 5436 | . . . . . . . . . . . 12
⊢ {0}
∈ V | 
| 24 | 23 | a1i 11 | . . . . . . . . . . 11
⊢ (𝑥 ∈ 𝑋 → {0} ∈ V) | 
| 25 |  | elmapg 8879 | . . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝑉 ∧ {0} ∈ V) → ({〈0, 𝑥〉} ∈ (𝑋 ↑m {0}) ↔
{〈0, 𝑥〉}:{0}⟶𝑋)) | 
| 26 | 24, 25 | sylan2 593 | . . . . . . . . . 10
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑥 ∈ 𝑋) → ({〈0, 𝑥〉} ∈ (𝑋 ↑m {0}) ↔ {〈0,
𝑥〉}:{0}⟶𝑋)) | 
| 27 | 22, 26 | mpbird 257 | . . . . . . . . 9
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑥 ∈ 𝑋) → {〈0, 𝑥〉} ∈ (𝑋 ↑m {0})) | 
| 28 | 27 | ad4ant14 752 | . . . . . . . 8
⊢ ((((𝑋 ∈ 𝑉 ∧ 𝑓 ∈ (𝑋 ↑m 𝑋)) ∧ ℎ = (𝑎 ∈ (𝑋 ↑m {0}) ↦ (𝑓‘(𝑎‘0)))) ∧ 𝑥 ∈ 𝑋) → {〈0, 𝑥〉} ∈ (𝑋 ↑m {0})) | 
| 29 |  | fvexd 6921 | . . . . . . . 8
⊢ ((((𝑋 ∈ 𝑉 ∧ 𝑓 ∈ (𝑋 ↑m 𝑋)) ∧ ℎ = (𝑎 ∈ (𝑋 ↑m {0}) ↦ (𝑓‘(𝑎‘0)))) ∧ 𝑥 ∈ 𝑋) → (𝑓‘𝑥) ∈ V) | 
| 30 |  | nfv 1914 | . . . . . . . . . 10
⊢
Ⅎ𝑎(𝑋 ∈ 𝑉 ∧ 𝑓 ∈ (𝑋 ↑m 𝑋)) | 
| 31 |  | nfmpt1 5250 | . . . . . . . . . . 11
⊢
Ⅎ𝑎(𝑎 ∈ (𝑋 ↑m {0}) ↦ (𝑓‘(𝑎‘0))) | 
| 32 | 31 | nfeq2 2923 | . . . . . . . . . 10
⊢
Ⅎ𝑎 ℎ = (𝑎 ∈ (𝑋 ↑m {0}) ↦ (𝑓‘(𝑎‘0))) | 
| 33 | 30, 32 | nfan 1899 | . . . . . . . . 9
⊢
Ⅎ𝑎((𝑋 ∈ 𝑉 ∧ 𝑓 ∈ (𝑋 ↑m 𝑋)) ∧ ℎ = (𝑎 ∈ (𝑋 ↑m {0}) ↦ (𝑓‘(𝑎‘0)))) | 
| 34 |  | nfv 1914 | . . . . . . . . 9
⊢
Ⅎ𝑎 𝑥 ∈ 𝑋 | 
| 35 | 33, 34 | nfan 1899 | . . . . . . . 8
⊢
Ⅎ𝑎(((𝑋 ∈ 𝑉 ∧ 𝑓 ∈ (𝑋 ↑m 𝑋)) ∧ ℎ = (𝑎 ∈ (𝑋 ↑m {0}) ↦ (𝑓‘(𝑎‘0)))) ∧ 𝑥 ∈ 𝑋) | 
| 36 |  | nfcv 2905 | . . . . . . . 8
⊢
Ⅎ𝑎{〈0, 𝑥〉} | 
| 37 |  | nfcv 2905 | . . . . . . . 8
⊢
Ⅎ𝑎(𝑓‘𝑥) | 
| 38 | 12, 19, 28, 29, 35, 36, 37 | fvmptdf 7022 | . . . . . . 7
⊢ ((((𝑋 ∈ 𝑉 ∧ 𝑓 ∈ (𝑋 ↑m 𝑋)) ∧ ℎ = (𝑎 ∈ (𝑋 ↑m {0}) ↦ (𝑓‘(𝑎‘0)))) ∧ 𝑥 ∈ 𝑋) → (ℎ‘{〈0, 𝑥〉}) = (𝑓‘𝑥)) | 
| 39 | 38 | mpteq2dva 5242 | . . . . . 6
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑓 ∈ (𝑋 ↑m 𝑋)) ∧ ℎ = (𝑎 ∈ (𝑋 ↑m {0}) ↦ (𝑓‘(𝑎‘0)))) → (𝑥 ∈ 𝑋 ↦ (ℎ‘{〈0, 𝑥〉})) = (𝑥 ∈ 𝑋 ↦ (𝑓‘𝑥))) | 
| 40 |  | simpl 482 | . . . . . . 7
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑓 ∈ (𝑋 ↑m 𝑋)) → 𝑋 ∈ 𝑉) | 
| 41 | 40 | mptexd 7244 | . . . . . 6
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑓 ∈ (𝑋 ↑m 𝑋)) → (𝑥 ∈ 𝑋 ↦ (𝑓‘𝑥)) ∈ V) | 
| 42 | 1, 39, 6, 41 | fvmptd2 7024 | . . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑓 ∈ (𝑋 ↑m 𝑋)) → (𝐻‘(𝑎 ∈ (𝑋 ↑m {0}) ↦ (𝑓‘(𝑎‘0)))) = (𝑥 ∈ 𝑋 ↦ (𝑓‘𝑥))) | 
| 43 | 11, 42 | eqtr4d 2780 | . . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑓 ∈ (𝑋 ↑m 𝑋)) → 𝑓 = (𝐻‘(𝑎 ∈ (𝑋 ↑m {0}) ↦ (𝑓‘(𝑎‘0))))) | 
| 44 | 6, 9, 43 | rspcedvd 3624 | . . 3
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑓 ∈ (𝑋 ↑m 𝑋)) → ∃𝑔 ∈ (1-aryF 𝑋)𝑓 = (𝐻‘𝑔)) | 
| 45 | 44 | ralrimiva 3146 | . 2
⊢ (𝑋 ∈ 𝑉 → ∀𝑓 ∈ (𝑋 ↑m 𝑋)∃𝑔 ∈ (1-aryF 𝑋)𝑓 = (𝐻‘𝑔)) | 
| 46 |  | dffo3 7122 | . 2
⊢ (𝐻:(1-aryF 𝑋)–onto→(𝑋 ↑m 𝑋) ↔ (𝐻:(1-aryF 𝑋)⟶(𝑋 ↑m 𝑋) ∧ ∀𝑓 ∈ (𝑋 ↑m 𝑋)∃𝑔 ∈ (1-aryF 𝑋)𝑓 = (𝐻‘𝑔))) | 
| 47 | 2, 45, 46 | sylanbrc 583 | 1
⊢ (𝑋 ∈ 𝑉 → 𝐻:(1-aryF 𝑋)–onto→(𝑋 ↑m 𝑋)) |