| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 1arymaptfv.h | . . 3
⊢ 𝐻 = (ℎ ∈ (1-aryF 𝑋) ↦ (𝑥 ∈ 𝑋 ↦ (ℎ‘{〈0, 𝑥〉}))) | 
| 2 | 1 | 1arymaptf 48562 | . 2
⊢ (𝑋 ∈ 𝑉 → 𝐻:(1-aryF 𝑋)⟶(𝑋 ↑m 𝑋)) | 
| 3 | 1 | 1arymaptfv 48561 | . . . . . 6
⊢ (𝑓 ∈ (1-aryF 𝑋) → (𝐻‘𝑓) = (𝑥 ∈ 𝑋 ↦ (𝑓‘{〈0, 𝑥〉}))) | 
| 4 | 3 | ad2antrl 728 | . . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ (𝑓 ∈ (1-aryF 𝑋) ∧ 𝑔 ∈ (1-aryF 𝑋))) → (𝐻‘𝑓) = (𝑥 ∈ 𝑋 ↦ (𝑓‘{〈0, 𝑥〉}))) | 
| 5 | 1 | 1arymaptfv 48561 | . . . . . 6
⊢ (𝑔 ∈ (1-aryF 𝑋) → (𝐻‘𝑔) = (𝑥 ∈ 𝑋 ↦ (𝑔‘{〈0, 𝑥〉}))) | 
| 6 | 5 | ad2antll 729 | . . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ (𝑓 ∈ (1-aryF 𝑋) ∧ 𝑔 ∈ (1-aryF 𝑋))) → (𝐻‘𝑔) = (𝑥 ∈ 𝑋 ↦ (𝑔‘{〈0, 𝑥〉}))) | 
| 7 | 4, 6 | eqeq12d 2753 | . . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ (𝑓 ∈ (1-aryF 𝑋) ∧ 𝑔 ∈ (1-aryF 𝑋))) → ((𝐻‘𝑓) = (𝐻‘𝑔) ↔ (𝑥 ∈ 𝑋 ↦ (𝑓‘{〈0, 𝑥〉})) = (𝑥 ∈ 𝑋 ↦ (𝑔‘{〈0, 𝑥〉})))) | 
| 8 |  | fvex 6919 | . . . . . . 7
⊢ (𝑓‘{〈0, 𝑥〉}) ∈
V | 
| 9 | 8 | rgenw 3065 | . . . . . 6
⊢
∀𝑥 ∈
𝑋 (𝑓‘{〈0, 𝑥〉}) ∈ V | 
| 10 |  | mpteqb 7035 | . . . . . 6
⊢
(∀𝑥 ∈
𝑋 (𝑓‘{〈0, 𝑥〉}) ∈ V → ((𝑥 ∈ 𝑋 ↦ (𝑓‘{〈0, 𝑥〉})) = (𝑥 ∈ 𝑋 ↦ (𝑔‘{〈0, 𝑥〉})) ↔ ∀𝑥 ∈ 𝑋 (𝑓‘{〈0, 𝑥〉}) = (𝑔‘{〈0, 𝑥〉}))) | 
| 11 | 9, 10 | mp1i 13 | . . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ (𝑓 ∈ (1-aryF 𝑋) ∧ 𝑔 ∈ (1-aryF 𝑋))) → ((𝑥 ∈ 𝑋 ↦ (𝑓‘{〈0, 𝑥〉})) = (𝑥 ∈ 𝑋 ↦ (𝑔‘{〈0, 𝑥〉})) ↔ ∀𝑥 ∈ 𝑋 (𝑓‘{〈0, 𝑥〉}) = (𝑔‘{〈0, 𝑥〉}))) | 
| 12 |  | 1aryfvalel 48557 | . . . . . . . 8
⊢ (𝑋 ∈ 𝑉 → (𝑓 ∈ (1-aryF 𝑋) ↔ 𝑓:(𝑋 ↑m {0})⟶𝑋)) | 
| 13 |  | 1aryfvalel 48557 | . . . . . . . 8
⊢ (𝑋 ∈ 𝑉 → (𝑔 ∈ (1-aryF 𝑋) ↔ 𝑔:(𝑋 ↑m {0})⟶𝑋)) | 
| 14 | 12, 13 | anbi12d 632 | . . . . . . 7
⊢ (𝑋 ∈ 𝑉 → ((𝑓 ∈ (1-aryF 𝑋) ∧ 𝑔 ∈ (1-aryF 𝑋)) ↔ (𝑓:(𝑋 ↑m {0})⟶𝑋 ∧ 𝑔:(𝑋 ↑m {0})⟶𝑋))) | 
| 15 |  | ffn 6736 | . . . . . . . . . . 11
⊢ (𝑓:(𝑋 ↑m {0})⟶𝑋 → 𝑓 Fn (𝑋 ↑m {0})) | 
| 16 | 15 | adantr 480 | . . . . . . . . . 10
⊢ ((𝑓:(𝑋 ↑m {0})⟶𝑋 ∧ 𝑔:(𝑋 ↑m {0})⟶𝑋) → 𝑓 Fn (𝑋 ↑m {0})) | 
| 17 | 16 | 3ad2ant2 1135 | . . . . . . . . 9
⊢ ((𝑋 ∈ 𝑉 ∧ (𝑓:(𝑋 ↑m {0})⟶𝑋 ∧ 𝑔:(𝑋 ↑m {0})⟶𝑋) ∧ ∀𝑥 ∈ 𝑋 (𝑓‘{〈0, 𝑥〉}) = (𝑔‘{〈0, 𝑥〉})) → 𝑓 Fn (𝑋 ↑m {0})) | 
| 18 |  | ffn 6736 | . . . . . . . . . . 11
⊢ (𝑔:(𝑋 ↑m {0})⟶𝑋 → 𝑔 Fn (𝑋 ↑m {0})) | 
| 19 | 18 | adantl 481 | . . . . . . . . . 10
⊢ ((𝑓:(𝑋 ↑m {0})⟶𝑋 ∧ 𝑔:(𝑋 ↑m {0})⟶𝑋) → 𝑔 Fn (𝑋 ↑m {0})) | 
| 20 | 19 | 3ad2ant2 1135 | . . . . . . . . 9
⊢ ((𝑋 ∈ 𝑉 ∧ (𝑓:(𝑋 ↑m {0})⟶𝑋 ∧ 𝑔:(𝑋 ↑m {0})⟶𝑋) ∧ ∀𝑥 ∈ 𝑋 (𝑓‘{〈0, 𝑥〉}) = (𝑔‘{〈0, 𝑥〉})) → 𝑔 Fn (𝑋 ↑m {0})) | 
| 21 |  | elmapi 8889 | . . . . . . . . . . . 12
⊢ (𝑦 ∈ (𝑋 ↑m {0}) → 𝑦:{0}⟶𝑋) | 
| 22 |  | c0ex 11255 | . . . . . . . . . . . . 13
⊢ 0 ∈
V | 
| 23 | 22 | fsn2 7156 | . . . . . . . . . . . 12
⊢ (𝑦:{0}⟶𝑋 ↔ ((𝑦‘0) ∈ 𝑋 ∧ 𝑦 = {〈0, (𝑦‘0)〉})) | 
| 24 | 21, 23 | sylib 218 | . . . . . . . . . . 11
⊢ (𝑦 ∈ (𝑋 ↑m {0}) → ((𝑦‘0) ∈ 𝑋 ∧ 𝑦 = {〈0, (𝑦‘0)〉})) | 
| 25 |  | opeq2 4874 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = (𝑦‘0) → 〈0, 𝑥〉 = 〈0, (𝑦‘0)〉) | 
| 26 | 25 | sneqd 4638 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = (𝑦‘0) → {〈0, 𝑥〉} = {〈0, (𝑦‘0)〉}) | 
| 27 | 26 | fveq2d 6910 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥 = (𝑦‘0) → (𝑓‘{〈0, 𝑥〉}) = (𝑓‘{〈0, (𝑦‘0)〉})) | 
| 28 | 26 | fveq2d 6910 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥 = (𝑦‘0) → (𝑔‘{〈0, 𝑥〉}) = (𝑔‘{〈0, (𝑦‘0)〉})) | 
| 29 | 27, 28 | eqeq12d 2753 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 = (𝑦‘0) → ((𝑓‘{〈0, 𝑥〉}) = (𝑔‘{〈0, 𝑥〉}) ↔ (𝑓‘{〈0, (𝑦‘0)〉}) = (𝑔‘{〈0, (𝑦‘0)〉}))) | 
| 30 | 29 | rspccv 3619 | . . . . . . . . . . . . . . 15
⊢
(∀𝑥 ∈
𝑋 (𝑓‘{〈0, 𝑥〉}) = (𝑔‘{〈0, 𝑥〉}) → ((𝑦‘0) ∈ 𝑋 → (𝑓‘{〈0, (𝑦‘0)〉}) = (𝑔‘{〈0, (𝑦‘0)〉}))) | 
| 31 | 30 | 3ad2ant3 1136 | . . . . . . . . . . . . . 14
⊢ ((𝑋 ∈ 𝑉 ∧ (𝑓:(𝑋 ↑m {0})⟶𝑋 ∧ 𝑔:(𝑋 ↑m {0})⟶𝑋) ∧ ∀𝑥 ∈ 𝑋 (𝑓‘{〈0, 𝑥〉}) = (𝑔‘{〈0, 𝑥〉})) → ((𝑦‘0) ∈ 𝑋 → (𝑓‘{〈0, (𝑦‘0)〉}) = (𝑔‘{〈0, (𝑦‘0)〉}))) | 
| 32 | 31 | com12 32 | . . . . . . . . . . . . 13
⊢ ((𝑦‘0) ∈ 𝑋 → ((𝑋 ∈ 𝑉 ∧ (𝑓:(𝑋 ↑m {0})⟶𝑋 ∧ 𝑔:(𝑋 ↑m {0})⟶𝑋) ∧ ∀𝑥 ∈ 𝑋 (𝑓‘{〈0, 𝑥〉}) = (𝑔‘{〈0, 𝑥〉})) → (𝑓‘{〈0, (𝑦‘0)〉}) = (𝑔‘{〈0, (𝑦‘0)〉}))) | 
| 33 | 32 | adantr 480 | . . . . . . . . . . . 12
⊢ (((𝑦‘0) ∈ 𝑋 ∧ 𝑦 = {〈0, (𝑦‘0)〉}) → ((𝑋 ∈ 𝑉 ∧ (𝑓:(𝑋 ↑m {0})⟶𝑋 ∧ 𝑔:(𝑋 ↑m {0})⟶𝑋) ∧ ∀𝑥 ∈ 𝑋 (𝑓‘{〈0, 𝑥〉}) = (𝑔‘{〈0, 𝑥〉})) → (𝑓‘{〈0, (𝑦‘0)〉}) = (𝑔‘{〈0, (𝑦‘0)〉}))) | 
| 34 |  | fveq2 6906 | . . . . . . . . . . . . . 14
⊢ (𝑦 = {〈0, (𝑦‘0)〉} → (𝑓‘𝑦) = (𝑓‘{〈0, (𝑦‘0)〉})) | 
| 35 |  | fveq2 6906 | . . . . . . . . . . . . . 14
⊢ (𝑦 = {〈0, (𝑦‘0)〉} → (𝑔‘𝑦) = (𝑔‘{〈0, (𝑦‘0)〉})) | 
| 36 | 34, 35 | eqeq12d 2753 | . . . . . . . . . . . . 13
⊢ (𝑦 = {〈0, (𝑦‘0)〉} → ((𝑓‘𝑦) = (𝑔‘𝑦) ↔ (𝑓‘{〈0, (𝑦‘0)〉}) = (𝑔‘{〈0, (𝑦‘0)〉}))) | 
| 37 | 36 | adantl 481 | . . . . . . . . . . . 12
⊢ (((𝑦‘0) ∈ 𝑋 ∧ 𝑦 = {〈0, (𝑦‘0)〉}) → ((𝑓‘𝑦) = (𝑔‘𝑦) ↔ (𝑓‘{〈0, (𝑦‘0)〉}) = (𝑔‘{〈0, (𝑦‘0)〉}))) | 
| 38 | 33, 37 | sylibrd 259 | . . . . . . . . . . 11
⊢ (((𝑦‘0) ∈ 𝑋 ∧ 𝑦 = {〈0, (𝑦‘0)〉}) → ((𝑋 ∈ 𝑉 ∧ (𝑓:(𝑋 ↑m {0})⟶𝑋 ∧ 𝑔:(𝑋 ↑m {0})⟶𝑋) ∧ ∀𝑥 ∈ 𝑋 (𝑓‘{〈0, 𝑥〉}) = (𝑔‘{〈0, 𝑥〉})) → (𝑓‘𝑦) = (𝑔‘𝑦))) | 
| 39 | 24, 38 | syl 17 | . . . . . . . . . 10
⊢ (𝑦 ∈ (𝑋 ↑m {0}) → ((𝑋 ∈ 𝑉 ∧ (𝑓:(𝑋 ↑m {0})⟶𝑋 ∧ 𝑔:(𝑋 ↑m {0})⟶𝑋) ∧ ∀𝑥 ∈ 𝑋 (𝑓‘{〈0, 𝑥〉}) = (𝑔‘{〈0, 𝑥〉})) → (𝑓‘𝑦) = (𝑔‘𝑦))) | 
| 40 | 39 | impcom 407 | . . . . . . . . 9
⊢ (((𝑋 ∈ 𝑉 ∧ (𝑓:(𝑋 ↑m {0})⟶𝑋 ∧ 𝑔:(𝑋 ↑m {0})⟶𝑋) ∧ ∀𝑥 ∈ 𝑋 (𝑓‘{〈0, 𝑥〉}) = (𝑔‘{〈0, 𝑥〉})) ∧ 𝑦 ∈ (𝑋 ↑m {0})) → (𝑓‘𝑦) = (𝑔‘𝑦)) | 
| 41 | 17, 20, 40 | eqfnfvd 7054 | . . . . . . . 8
⊢ ((𝑋 ∈ 𝑉 ∧ (𝑓:(𝑋 ↑m {0})⟶𝑋 ∧ 𝑔:(𝑋 ↑m {0})⟶𝑋) ∧ ∀𝑥 ∈ 𝑋 (𝑓‘{〈0, 𝑥〉}) = (𝑔‘{〈0, 𝑥〉})) → 𝑓 = 𝑔) | 
| 42 | 41 | 3exp 1120 | . . . . . . 7
⊢ (𝑋 ∈ 𝑉 → ((𝑓:(𝑋 ↑m {0})⟶𝑋 ∧ 𝑔:(𝑋 ↑m {0})⟶𝑋) → (∀𝑥 ∈ 𝑋 (𝑓‘{〈0, 𝑥〉}) = (𝑔‘{〈0, 𝑥〉}) → 𝑓 = 𝑔))) | 
| 43 | 14, 42 | sylbid 240 | . . . . . 6
⊢ (𝑋 ∈ 𝑉 → ((𝑓 ∈ (1-aryF 𝑋) ∧ 𝑔 ∈ (1-aryF 𝑋)) → (∀𝑥 ∈ 𝑋 (𝑓‘{〈0, 𝑥〉}) = (𝑔‘{〈0, 𝑥〉}) → 𝑓 = 𝑔))) | 
| 44 | 43 | imp 406 | . . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ (𝑓 ∈ (1-aryF 𝑋) ∧ 𝑔 ∈ (1-aryF 𝑋))) → (∀𝑥 ∈ 𝑋 (𝑓‘{〈0, 𝑥〉}) = (𝑔‘{〈0, 𝑥〉}) → 𝑓 = 𝑔)) | 
| 45 | 11, 44 | sylbid 240 | . . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ (𝑓 ∈ (1-aryF 𝑋) ∧ 𝑔 ∈ (1-aryF 𝑋))) → ((𝑥 ∈ 𝑋 ↦ (𝑓‘{〈0, 𝑥〉})) = (𝑥 ∈ 𝑋 ↦ (𝑔‘{〈0, 𝑥〉})) → 𝑓 = 𝑔)) | 
| 46 | 7, 45 | sylbid 240 | . . 3
⊢ ((𝑋 ∈ 𝑉 ∧ (𝑓 ∈ (1-aryF 𝑋) ∧ 𝑔 ∈ (1-aryF 𝑋))) → ((𝐻‘𝑓) = (𝐻‘𝑔) → 𝑓 = 𝑔)) | 
| 47 | 46 | ralrimivva 3202 | . 2
⊢ (𝑋 ∈ 𝑉 → ∀𝑓 ∈ (1-aryF 𝑋)∀𝑔 ∈ (1-aryF 𝑋)((𝐻‘𝑓) = (𝐻‘𝑔) → 𝑓 = 𝑔)) | 
| 48 |  | dff13 7275 | . 2
⊢ (𝐻:(1-aryF 𝑋)–1-1→(𝑋 ↑m 𝑋) ↔ (𝐻:(1-aryF 𝑋)⟶(𝑋 ↑m 𝑋) ∧ ∀𝑓 ∈ (1-aryF 𝑋)∀𝑔 ∈ (1-aryF 𝑋)((𝐻‘𝑓) = (𝐻‘𝑔) → 𝑓 = 𝑔))) | 
| 49 | 2, 47, 48 | sylanbrc 583 | 1
⊢ (𝑋 ∈ 𝑉 → 𝐻:(1-aryF 𝑋)–1-1→(𝑋 ↑m 𝑋)) |