Step | Hyp | Ref
| Expression |
1 | | 1arymaptfv.h |
. . 3
⊢ 𝐻 = (ℎ ∈ (1-aryF 𝑋) ↦ (𝑥 ∈ 𝑋 ↦ (ℎ‘{⟨0, 𝑥⟩}))) |
2 | 1 | 1arymaptf 46801 |
. 2
⊢ (𝑋 ∈ 𝑉 → 𝐻:(1-aryF 𝑋)⟶(𝑋 ↑m 𝑋)) |
3 | 1 | 1arymaptfv 46800 |
. . . . . 6
⊢ (𝑓 ∈ (1-aryF 𝑋) → (𝐻‘𝑓) = (𝑥 ∈ 𝑋 ↦ (𝑓‘{⟨0, 𝑥⟩}))) |
4 | 3 | ad2antrl 727 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ (𝑓 ∈ (1-aryF 𝑋) ∧ 𝑔 ∈ (1-aryF 𝑋))) → (𝐻‘𝑓) = (𝑥 ∈ 𝑋 ↦ (𝑓‘{⟨0, 𝑥⟩}))) |
5 | 1 | 1arymaptfv 46800 |
. . . . . 6
⊢ (𝑔 ∈ (1-aryF 𝑋) → (𝐻‘𝑔) = (𝑥 ∈ 𝑋 ↦ (𝑔‘{⟨0, 𝑥⟩}))) |
6 | 5 | ad2antll 728 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ (𝑓 ∈ (1-aryF 𝑋) ∧ 𝑔 ∈ (1-aryF 𝑋))) → (𝐻‘𝑔) = (𝑥 ∈ 𝑋 ↦ (𝑔‘{⟨0, 𝑥⟩}))) |
7 | 4, 6 | eqeq12d 2753 |
. . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ (𝑓 ∈ (1-aryF 𝑋) ∧ 𝑔 ∈ (1-aryF 𝑋))) → ((𝐻‘𝑓) = (𝐻‘𝑔) ↔ (𝑥 ∈ 𝑋 ↦ (𝑓‘{⟨0, 𝑥⟩})) = (𝑥 ∈ 𝑋 ↦ (𝑔‘{⟨0, 𝑥⟩})))) |
8 | | fvex 6860 |
. . . . . . 7
⊢ (𝑓‘{⟨0, 𝑥⟩}) ∈
V |
9 | 8 | rgenw 3069 |
. . . . . 6
⊢
∀𝑥 ∈
𝑋 (𝑓‘{⟨0, 𝑥⟩}) ∈ V |
10 | | mpteqb 6972 |
. . . . . 6
⊢
(∀𝑥 ∈
𝑋 (𝑓‘{⟨0, 𝑥⟩}) ∈ V → ((𝑥 ∈ 𝑋 ↦ (𝑓‘{⟨0, 𝑥⟩})) = (𝑥 ∈ 𝑋 ↦ (𝑔‘{⟨0, 𝑥⟩})) ↔ ∀𝑥 ∈ 𝑋 (𝑓‘{⟨0, 𝑥⟩}) = (𝑔‘{⟨0, 𝑥⟩}))) |
11 | 9, 10 | mp1i 13 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ (𝑓 ∈ (1-aryF 𝑋) ∧ 𝑔 ∈ (1-aryF 𝑋))) → ((𝑥 ∈ 𝑋 ↦ (𝑓‘{⟨0, 𝑥⟩})) = (𝑥 ∈ 𝑋 ↦ (𝑔‘{⟨0, 𝑥⟩})) ↔ ∀𝑥 ∈ 𝑋 (𝑓‘{⟨0, 𝑥⟩}) = (𝑔‘{⟨0, 𝑥⟩}))) |
12 | | 1aryfvalel 46796 |
. . . . . . . 8
⊢ (𝑋 ∈ 𝑉 → (𝑓 ∈ (1-aryF 𝑋) ↔ 𝑓:(𝑋 ↑m {0})⟶𝑋)) |
13 | | 1aryfvalel 46796 |
. . . . . . . 8
⊢ (𝑋 ∈ 𝑉 → (𝑔 ∈ (1-aryF 𝑋) ↔ 𝑔:(𝑋 ↑m {0})⟶𝑋)) |
14 | 12, 13 | anbi12d 632 |
. . . . . . 7
⊢ (𝑋 ∈ 𝑉 → ((𝑓 ∈ (1-aryF 𝑋) ∧ 𝑔 ∈ (1-aryF 𝑋)) ↔ (𝑓:(𝑋 ↑m {0})⟶𝑋 ∧ 𝑔:(𝑋 ↑m {0})⟶𝑋))) |
15 | | ffn 6673 |
. . . . . . . . . . 11
⊢ (𝑓:(𝑋 ↑m {0})⟶𝑋 → 𝑓 Fn (𝑋 ↑m {0})) |
16 | 15 | adantr 482 |
. . . . . . . . . 10
⊢ ((𝑓:(𝑋 ↑m {0})⟶𝑋 ∧ 𝑔:(𝑋 ↑m {0})⟶𝑋) → 𝑓 Fn (𝑋 ↑m {0})) |
17 | 16 | 3ad2ant2 1135 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝑉 ∧ (𝑓:(𝑋 ↑m {0})⟶𝑋 ∧ 𝑔:(𝑋 ↑m {0})⟶𝑋) ∧ ∀𝑥 ∈ 𝑋 (𝑓‘{⟨0, 𝑥⟩}) = (𝑔‘{⟨0, 𝑥⟩})) → 𝑓 Fn (𝑋 ↑m {0})) |
18 | | ffn 6673 |
. . . . . . . . . . 11
⊢ (𝑔:(𝑋 ↑m {0})⟶𝑋 → 𝑔 Fn (𝑋 ↑m {0})) |
19 | 18 | adantl 483 |
. . . . . . . . . 10
⊢ ((𝑓:(𝑋 ↑m {0})⟶𝑋 ∧ 𝑔:(𝑋 ↑m {0})⟶𝑋) → 𝑔 Fn (𝑋 ↑m {0})) |
20 | 19 | 3ad2ant2 1135 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝑉 ∧ (𝑓:(𝑋 ↑m {0})⟶𝑋 ∧ 𝑔:(𝑋 ↑m {0})⟶𝑋) ∧ ∀𝑥 ∈ 𝑋 (𝑓‘{⟨0, 𝑥⟩}) = (𝑔‘{⟨0, 𝑥⟩})) → 𝑔 Fn (𝑋 ↑m {0})) |
21 | | elmapi 8794 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ (𝑋 ↑m {0}) → 𝑦:{0}⟶𝑋) |
22 | | c0ex 11156 |
. . . . . . . . . . . . 13
⊢ 0 ∈
V |
23 | 22 | fsn2 7087 |
. . . . . . . . . . . 12
⊢ (𝑦:{0}⟶𝑋 ↔ ((𝑦‘0) ∈ 𝑋 ∧ 𝑦 = {⟨0, (𝑦‘0)⟩})) |
24 | 21, 23 | sylib 217 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ (𝑋 ↑m {0}) → ((𝑦‘0) ∈ 𝑋 ∧ 𝑦 = {⟨0, (𝑦‘0)⟩})) |
25 | | opeq2 4836 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = (𝑦‘0) → ⟨0, 𝑥⟩ = ⟨0, (𝑦‘0)⟩) |
26 | 25 | sneqd 4603 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = (𝑦‘0) → {⟨0, 𝑥⟩} = {⟨0, (𝑦‘0)⟩}) |
27 | 26 | fveq2d 6851 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = (𝑦‘0) → (𝑓‘{⟨0, 𝑥⟩}) = (𝑓‘{⟨0, (𝑦‘0)⟩})) |
28 | 26 | fveq2d 6851 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = (𝑦‘0) → (𝑔‘{⟨0, 𝑥⟩}) = (𝑔‘{⟨0, (𝑦‘0)⟩})) |
29 | 27, 28 | eqeq12d 2753 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = (𝑦‘0) → ((𝑓‘{⟨0, 𝑥⟩}) = (𝑔‘{⟨0, 𝑥⟩}) ↔ (𝑓‘{⟨0, (𝑦‘0)⟩}) = (𝑔‘{⟨0, (𝑦‘0)⟩}))) |
30 | 29 | rspccv 3581 |
. . . . . . . . . . . . . . 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 482 |
. . . . . . . . . . . 12
⊢ (((𝑦‘0) ∈ 𝑋 ∧ 𝑦 = {⟨0, (𝑦‘0)⟩}) → ((𝑋 ∈ 𝑉 ∧ (𝑓:(𝑋 ↑m {0})⟶𝑋 ∧ 𝑔:(𝑋 ↑m {0})⟶𝑋) ∧ ∀𝑥 ∈ 𝑋 (𝑓‘{⟨0, 𝑥⟩}) = (𝑔‘{⟨0, 𝑥⟩})) → (𝑓‘{⟨0, (𝑦‘0)⟩}) = (𝑔‘{⟨0, (𝑦‘0)⟩}))) |
34 | | fveq2 6847 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = {⟨0, (𝑦‘0)⟩} → (𝑓‘𝑦) = (𝑓‘{⟨0, (𝑦‘0)⟩})) |
35 | | fveq2 6847 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = {⟨0, (𝑦‘0)⟩} → (𝑔‘𝑦) = (𝑔‘{⟨0, (𝑦‘0)⟩})) |
36 | 34, 35 | eqeq12d 2753 |
. . . . . . . . . . . . 13
⊢ (𝑦 = {⟨0, (𝑦‘0)⟩} → ((𝑓‘𝑦) = (𝑔‘𝑦) ↔ (𝑓‘{⟨0, (𝑦‘0)⟩}) = (𝑔‘{⟨0, (𝑦‘0)⟩}))) |
37 | 36 | adantl 483 |
. . . . . . . . . . . 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 409 |
. . . . . . . . 9
⊢ (((𝑋 ∈ 𝑉 ∧ (𝑓:(𝑋 ↑m {0})⟶𝑋 ∧ 𝑔:(𝑋 ↑m {0})⟶𝑋) ∧ ∀𝑥 ∈ 𝑋 (𝑓‘{⟨0, 𝑥⟩}) = (𝑔‘{⟨0, 𝑥⟩})) ∧ 𝑦 ∈ (𝑋 ↑m {0})) → (𝑓‘𝑦) = (𝑔‘𝑦)) |
41 | 17, 20, 40 | eqfnfvd 6990 |
. . . . . . . 8
⊢ ((𝑋 ∈ 𝑉 ∧ (𝑓:(𝑋 ↑m {0})⟶𝑋 ∧ 𝑔:(𝑋 ↑m {0})⟶𝑋) ∧ ∀𝑥 ∈ 𝑋 (𝑓‘{⟨0, 𝑥⟩}) = (𝑔‘{⟨0, 𝑥⟩})) → 𝑓 = 𝑔) |
42 | 41 | 3exp 1120 |
. . . . . . 7
⊢ (𝑋 ∈ 𝑉 → ((𝑓:(𝑋 ↑m {0})⟶𝑋 ∧ 𝑔:(𝑋 ↑m {0})⟶𝑋) → (∀𝑥 ∈ 𝑋 (𝑓‘{⟨0, 𝑥⟩}) = (𝑔‘{⟨0, 𝑥⟩}) → 𝑓 = 𝑔))) |
43 | 14, 42 | sylbid 239 |
. . . . . 6
⊢ (𝑋 ∈ 𝑉 → ((𝑓 ∈ (1-aryF 𝑋) ∧ 𝑔 ∈ (1-aryF 𝑋)) → (∀𝑥 ∈ 𝑋 (𝑓‘{⟨0, 𝑥⟩}) = (𝑔‘{⟨0, 𝑥⟩}) → 𝑓 = 𝑔))) |
44 | 43 | imp 408 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ (𝑓 ∈ (1-aryF 𝑋) ∧ 𝑔 ∈ (1-aryF 𝑋))) → (∀𝑥 ∈ 𝑋 (𝑓‘{⟨0, 𝑥⟩}) = (𝑔‘{⟨0, 𝑥⟩}) → 𝑓 = 𝑔)) |
45 | 11, 44 | sylbid 239 |
. . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ (𝑓 ∈ (1-aryF 𝑋) ∧ 𝑔 ∈ (1-aryF 𝑋))) → ((𝑥 ∈ 𝑋 ↦ (𝑓‘{⟨0, 𝑥⟩})) = (𝑥 ∈ 𝑋 ↦ (𝑔‘{⟨0, 𝑥⟩})) → 𝑓 = 𝑔)) |
46 | 7, 45 | sylbid 239 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ (𝑓 ∈ (1-aryF 𝑋) ∧ 𝑔 ∈ (1-aryF 𝑋))) → ((𝐻‘𝑓) = (𝐻‘𝑔) → 𝑓 = 𝑔)) |
47 | 46 | ralrimivva 3198 |
. 2
⊢ (𝑋 ∈ 𝑉 → ∀𝑓 ∈ (1-aryF 𝑋)∀𝑔 ∈ (1-aryF 𝑋)((𝐻‘𝑓) = (𝐻‘𝑔) → 𝑓 = 𝑔)) |
48 | | dff13 7207 |
. 2
⊢ (𝐻:(1-aryF 𝑋)–1-1→(𝑋 ↑m 𝑋) ↔ (𝐻:(1-aryF 𝑋)⟶(𝑋 ↑m 𝑋) ∧ ∀𝑓 ∈ (1-aryF 𝑋)∀𝑔 ∈ (1-aryF 𝑋)((𝐻‘𝑓) = (𝐻‘𝑔) → 𝑓 = 𝑔))) |
49 | 2, 47, 48 | sylanbrc 584 |
1
⊢ (𝑋 ∈ 𝑉 → 𝐻:(1-aryF 𝑋)–1-1→(𝑋 ↑m 𝑋)) |