Step | Hyp | Ref
| Expression |
1 | | 1arymaptfv.h |
. . 3
⊢ 𝐻 = (ℎ ∈ (1-aryF 𝑋) ↦ (𝑥 ∈ 𝑋 ↦ (ℎ‘{〈0, 𝑥〉}))) |
2 | 1 | 1arymaptf 45405 |
. 2
⊢ (𝑋 ∈ 𝑉 → 𝐻:(1-aryF 𝑋)⟶(𝑋 ↑m 𝑋)) |
3 | 1 | 1arymaptfv 45404 |
. . . . . 6
⊢ (𝑓 ∈ (1-aryF 𝑋) → (𝐻‘𝑓) = (𝑥 ∈ 𝑋 ↦ (𝑓‘{〈0, 𝑥〉}))) |
4 | 3 | ad2antrl 728 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ (𝑓 ∈ (1-aryF 𝑋) ∧ 𝑔 ∈ (1-aryF 𝑋))) → (𝐻‘𝑓) = (𝑥 ∈ 𝑋 ↦ (𝑓‘{〈0, 𝑥〉}))) |
5 | 1 | 1arymaptfv 45404 |
. . . . . 6
⊢ (𝑔 ∈ (1-aryF 𝑋) → (𝐻‘𝑔) = (𝑥 ∈ 𝑋 ↦ (𝑔‘{〈0, 𝑥〉}))) |
6 | 5 | ad2antll 729 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ (𝑓 ∈ (1-aryF 𝑋) ∧ 𝑔 ∈ (1-aryF 𝑋))) → (𝐻‘𝑔) = (𝑥 ∈ 𝑋 ↦ (𝑔‘{〈0, 𝑥〉}))) |
7 | 4, 6 | eqeq12d 2775 |
. . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ (𝑓 ∈ (1-aryF 𝑋) ∧ 𝑔 ∈ (1-aryF 𝑋))) → ((𝐻‘𝑓) = (𝐻‘𝑔) ↔ (𝑥 ∈ 𝑋 ↦ (𝑓‘{〈0, 𝑥〉})) = (𝑥 ∈ 𝑋 ↦ (𝑔‘{〈0, 𝑥〉})))) |
8 | | fvex 6664 |
. . . . . . 7
⊢ (𝑓‘{〈0, 𝑥〉}) ∈
V |
9 | 8 | rgenw 3080 |
. . . . . 6
⊢
∀𝑥 ∈
𝑋 (𝑓‘{〈0, 𝑥〉}) ∈ V |
10 | | mpteqb 6771 |
. . . . . 6
⊢
(∀𝑥 ∈
𝑋 (𝑓‘{〈0, 𝑥〉}) ∈ V → ((𝑥 ∈ 𝑋 ↦ (𝑓‘{〈0, 𝑥〉})) = (𝑥 ∈ 𝑋 ↦ (𝑔‘{〈0, 𝑥〉})) ↔ ∀𝑥 ∈ 𝑋 (𝑓‘{〈0, 𝑥〉}) = (𝑔‘{〈0, 𝑥〉}))) |
11 | 9, 10 | mp1i 13 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ (𝑓 ∈ (1-aryF 𝑋) ∧ 𝑔 ∈ (1-aryF 𝑋))) → ((𝑥 ∈ 𝑋 ↦ (𝑓‘{〈0, 𝑥〉})) = (𝑥 ∈ 𝑋 ↦ (𝑔‘{〈0, 𝑥〉})) ↔ ∀𝑥 ∈ 𝑋 (𝑓‘{〈0, 𝑥〉}) = (𝑔‘{〈0, 𝑥〉}))) |
12 | | 1aryfvalel 45400 |
. . . . . . . 8
⊢ (𝑋 ∈ 𝑉 → (𝑓 ∈ (1-aryF 𝑋) ↔ 𝑓:(𝑋 ↑m {0})⟶𝑋)) |
13 | | 1aryfvalel 45400 |
. . . . . . . 8
⊢ (𝑋 ∈ 𝑉 → (𝑔 ∈ (1-aryF 𝑋) ↔ 𝑔:(𝑋 ↑m {0})⟶𝑋)) |
14 | 12, 13 | anbi12d 634 |
. . . . . . 7
⊢ (𝑋 ∈ 𝑉 → ((𝑓 ∈ (1-aryF 𝑋) ∧ 𝑔 ∈ (1-aryF 𝑋)) ↔ (𝑓:(𝑋 ↑m {0})⟶𝑋 ∧ 𝑔:(𝑋 ↑m {0})⟶𝑋))) |
15 | | ffn 6491 |
. . . . . . . . . . 11
⊢ (𝑓:(𝑋 ↑m {0})⟶𝑋 → 𝑓 Fn (𝑋 ↑m {0})) |
16 | 15 | adantr 485 |
. . . . . . . . . 10
⊢ ((𝑓:(𝑋 ↑m {0})⟶𝑋 ∧ 𝑔:(𝑋 ↑m {0})⟶𝑋) → 𝑓 Fn (𝑋 ↑m {0})) |
17 | 16 | 3ad2ant2 1132 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝑉 ∧ (𝑓:(𝑋 ↑m {0})⟶𝑋 ∧ 𝑔:(𝑋 ↑m {0})⟶𝑋) ∧ ∀𝑥 ∈ 𝑋 (𝑓‘{〈0, 𝑥〉}) = (𝑔‘{〈0, 𝑥〉})) → 𝑓 Fn (𝑋 ↑m {0})) |
18 | | ffn 6491 |
. . . . . . . . . . 11
⊢ (𝑔:(𝑋 ↑m {0})⟶𝑋 → 𝑔 Fn (𝑋 ↑m {0})) |
19 | 18 | adantl 486 |
. . . . . . . . . 10
⊢ ((𝑓:(𝑋 ↑m {0})⟶𝑋 ∧ 𝑔:(𝑋 ↑m {0})⟶𝑋) → 𝑔 Fn (𝑋 ↑m {0})) |
20 | 19 | 3ad2ant2 1132 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝑉 ∧ (𝑓:(𝑋 ↑m {0})⟶𝑋 ∧ 𝑔:(𝑋 ↑m {0})⟶𝑋) ∧ ∀𝑥 ∈ 𝑋 (𝑓‘{〈0, 𝑥〉}) = (𝑔‘{〈0, 𝑥〉})) → 𝑔 Fn (𝑋 ↑m {0})) |
21 | | elmapi 8431 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ (𝑋 ↑m {0}) → 𝑦:{0}⟶𝑋) |
22 | | c0ex 10658 |
. . . . . . . . . . . . 13
⊢ 0 ∈
V |
23 | 22 | fsn2 6882 |
. . . . . . . . . . . 12
⊢ (𝑦:{0}⟶𝑋 ↔ ((𝑦‘0) ∈ 𝑋 ∧ 𝑦 = {〈0, (𝑦‘0)〉})) |
24 | 21, 23 | sylib 221 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ (𝑋 ↑m {0}) → ((𝑦‘0) ∈ 𝑋 ∧ 𝑦 = {〈0, (𝑦‘0)〉})) |
25 | | opeq2 4756 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = (𝑦‘0) → 〈0, 𝑥〉 = 〈0, (𝑦‘0)〉) |
26 | 25 | sneqd 4527 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = (𝑦‘0) → {〈0, 𝑥〉} = {〈0, (𝑦‘0)〉}) |
27 | 26 | fveq2d 6655 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = (𝑦‘0) → (𝑓‘{〈0, 𝑥〉}) = (𝑓‘{〈0, (𝑦‘0)〉})) |
28 | 26 | fveq2d 6655 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = (𝑦‘0) → (𝑔‘{〈0, 𝑥〉}) = (𝑔‘{〈0, (𝑦‘0)〉})) |
29 | 27, 28 | eqeq12d 2775 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = (𝑦‘0) → ((𝑓‘{〈0, 𝑥〉}) = (𝑔‘{〈0, 𝑥〉}) ↔ (𝑓‘{〈0, (𝑦‘0)〉}) = (𝑔‘{〈0, (𝑦‘0)〉}))) |
30 | 29 | rspccv 3536 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑥 ∈
𝑋 (𝑓‘{〈0, 𝑥〉}) = (𝑔‘{〈0, 𝑥〉}) → ((𝑦‘0) ∈ 𝑋 → (𝑓‘{〈0, (𝑦‘0)〉}) = (𝑔‘{〈0, (𝑦‘0)〉}))) |
31 | 30 | 3ad2ant3 1133 |
. . . . . . . . . . . . . 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 485 |
. . . . . . . . . . . 12
⊢ (((𝑦‘0) ∈ 𝑋 ∧ 𝑦 = {〈0, (𝑦‘0)〉}) → ((𝑋 ∈ 𝑉 ∧ (𝑓:(𝑋 ↑m {0})⟶𝑋 ∧ 𝑔:(𝑋 ↑m {0})⟶𝑋) ∧ ∀𝑥 ∈ 𝑋 (𝑓‘{〈0, 𝑥〉}) = (𝑔‘{〈0, 𝑥〉})) → (𝑓‘{〈0, (𝑦‘0)〉}) = (𝑔‘{〈0, (𝑦‘0)〉}))) |
34 | | fveq2 6651 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = {〈0, (𝑦‘0)〉} → (𝑓‘𝑦) = (𝑓‘{〈0, (𝑦‘0)〉})) |
35 | | fveq2 6651 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = {〈0, (𝑦‘0)〉} → (𝑔‘𝑦) = (𝑔‘{〈0, (𝑦‘0)〉})) |
36 | 34, 35 | eqeq12d 2775 |
. . . . . . . . . . . . 13
⊢ (𝑦 = {〈0, (𝑦‘0)〉} → ((𝑓‘𝑦) = (𝑔‘𝑦) ↔ (𝑓‘{〈0, (𝑦‘0)〉}) = (𝑔‘{〈0, (𝑦‘0)〉}))) |
37 | 36 | adantl 486 |
. . . . . . . . . . . 12
⊢ (((𝑦‘0) ∈ 𝑋 ∧ 𝑦 = {〈0, (𝑦‘0)〉}) → ((𝑓‘𝑦) = (𝑔‘𝑦) ↔ (𝑓‘{〈0, (𝑦‘0)〉}) = (𝑔‘{〈0, (𝑦‘0)〉}))) |
38 | 33, 37 | sylibrd 262 |
. . . . . . . . . . 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 412 |
. . . . . . . . 9
⊢ (((𝑋 ∈ 𝑉 ∧ (𝑓:(𝑋 ↑m {0})⟶𝑋 ∧ 𝑔:(𝑋 ↑m {0})⟶𝑋) ∧ ∀𝑥 ∈ 𝑋 (𝑓‘{〈0, 𝑥〉}) = (𝑔‘{〈0, 𝑥〉})) ∧ 𝑦 ∈ (𝑋 ↑m {0})) → (𝑓‘𝑦) = (𝑔‘𝑦)) |
41 | 17, 20, 40 | eqfnfvd 6789 |
. . . . . . . 8
⊢ ((𝑋 ∈ 𝑉 ∧ (𝑓:(𝑋 ↑m {0})⟶𝑋 ∧ 𝑔:(𝑋 ↑m {0})⟶𝑋) ∧ ∀𝑥 ∈ 𝑋 (𝑓‘{〈0, 𝑥〉}) = (𝑔‘{〈0, 𝑥〉})) → 𝑓 = 𝑔) |
42 | 41 | 3exp 1117 |
. . . . . . 7
⊢ (𝑋 ∈ 𝑉 → ((𝑓:(𝑋 ↑m {0})⟶𝑋 ∧ 𝑔:(𝑋 ↑m {0})⟶𝑋) → (∀𝑥 ∈ 𝑋 (𝑓‘{〈0, 𝑥〉}) = (𝑔‘{〈0, 𝑥〉}) → 𝑓 = 𝑔))) |
43 | 14, 42 | sylbid 243 |
. . . . . 6
⊢ (𝑋 ∈ 𝑉 → ((𝑓 ∈ (1-aryF 𝑋) ∧ 𝑔 ∈ (1-aryF 𝑋)) → (∀𝑥 ∈ 𝑋 (𝑓‘{〈0, 𝑥〉}) = (𝑔‘{〈0, 𝑥〉}) → 𝑓 = 𝑔))) |
44 | 43 | imp 411 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ (𝑓 ∈ (1-aryF 𝑋) ∧ 𝑔 ∈ (1-aryF 𝑋))) → (∀𝑥 ∈ 𝑋 (𝑓‘{〈0, 𝑥〉}) = (𝑔‘{〈0, 𝑥〉}) → 𝑓 = 𝑔)) |
45 | 11, 44 | sylbid 243 |
. . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ (𝑓 ∈ (1-aryF 𝑋) ∧ 𝑔 ∈ (1-aryF 𝑋))) → ((𝑥 ∈ 𝑋 ↦ (𝑓‘{〈0, 𝑥〉})) = (𝑥 ∈ 𝑋 ↦ (𝑔‘{〈0, 𝑥〉})) → 𝑓 = 𝑔)) |
46 | 7, 45 | sylbid 243 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ (𝑓 ∈ (1-aryF 𝑋) ∧ 𝑔 ∈ (1-aryF 𝑋))) → ((𝐻‘𝑓) = (𝐻‘𝑔) → 𝑓 = 𝑔)) |
47 | 46 | ralrimivva 3118 |
. 2
⊢ (𝑋 ∈ 𝑉 → ∀𝑓 ∈ (1-aryF 𝑋)∀𝑔 ∈ (1-aryF 𝑋)((𝐻‘𝑓) = (𝐻‘𝑔) → 𝑓 = 𝑔)) |
48 | | dff13 6998 |
. 2
⊢ (𝐻:(1-aryF 𝑋)–1-1→(𝑋 ↑m 𝑋) ↔ (𝐻:(1-aryF 𝑋)⟶(𝑋 ↑m 𝑋) ∧ ∀𝑓 ∈ (1-aryF 𝑋)∀𝑔 ∈ (1-aryF 𝑋)((𝐻‘𝑓) = (𝐻‘𝑔) → 𝑓 = 𝑔))) |
49 | 2, 47, 48 | sylanbrc 587 |
1
⊢ (𝑋 ∈ 𝑉 → 𝐻:(1-aryF 𝑋)–1-1→(𝑋 ↑m 𝑋)) |