Step | Hyp | Ref
| Expression |
1 | | 2arymaptf.h |
. . 3
⊢ 𝐻 = (ℎ ∈ (2-aryF 𝑋) ↦ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (ℎ‘{〈0, 𝑥〉, 〈1, 𝑦〉}))) |
2 | 1 | 2arymaptf 45416 |
. 2
⊢ (𝑋 ∈ 𝑉 → 𝐻:(2-aryF 𝑋)⟶(𝑋 ↑m (𝑋 × 𝑋))) |
3 | 1 | 2arymaptfv 45415 |
. . . . . 6
⊢ (𝑓 ∈ (2-aryF 𝑋) → (𝐻‘𝑓) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (𝑓‘{〈0, 𝑥〉, 〈1, 𝑦〉}))) |
4 | 3 | ad2antrl 728 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ (𝑓 ∈ (2-aryF 𝑋) ∧ 𝑔 ∈ (2-aryF 𝑋))) → (𝐻‘𝑓) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (𝑓‘{〈0, 𝑥〉, 〈1, 𝑦〉}))) |
5 | 1 | 2arymaptfv 45415 |
. . . . . 6
⊢ (𝑔 ∈ (2-aryF 𝑋) → (𝐻‘𝑔) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (𝑔‘{〈0, 𝑥〉, 〈1, 𝑦〉}))) |
6 | 5 | ad2antll 729 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ (𝑓 ∈ (2-aryF 𝑋) ∧ 𝑔 ∈ (2-aryF 𝑋))) → (𝐻‘𝑔) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (𝑔‘{〈0, 𝑥〉, 〈1, 𝑦〉}))) |
7 | 4, 6 | eqeq12d 2775 |
. . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ (𝑓 ∈ (2-aryF 𝑋) ∧ 𝑔 ∈ (2-aryF 𝑋))) → ((𝐻‘𝑓) = (𝐻‘𝑔) ↔ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (𝑓‘{〈0, 𝑥〉, 〈1, 𝑦〉})) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (𝑔‘{〈0, 𝑥〉, 〈1, 𝑦〉})))) |
8 | | fvex 6664 |
. . . . . . 7
⊢ (𝑓‘{〈0, 𝑥〉, 〈1, 𝑦〉}) ∈
V |
9 | 8 | rgen2w 3081 |
. . . . . 6
⊢
∀𝑥 ∈
𝑋 ∀𝑦 ∈ 𝑋 (𝑓‘{〈0, 𝑥〉, 〈1, 𝑦〉}) ∈ V |
10 | | mpo2eqb 7271 |
. . . . . 6
⊢
(∀𝑥 ∈
𝑋 ∀𝑦 ∈ 𝑋 (𝑓‘{〈0, 𝑥〉, 〈1, 𝑦〉}) ∈ V → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (𝑓‘{〈0, 𝑥〉, 〈1, 𝑦〉})) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (𝑔‘{〈0, 𝑥〉, 〈1, 𝑦〉})) ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑓‘{〈0, 𝑥〉, 〈1, 𝑦〉}) = (𝑔‘{〈0, 𝑥〉, 〈1, 𝑦〉}))) |
11 | 9, 10 | mp1i 13 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ (𝑓 ∈ (2-aryF 𝑋) ∧ 𝑔 ∈ (2-aryF 𝑋))) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (𝑓‘{〈0, 𝑥〉, 〈1, 𝑦〉})) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (𝑔‘{〈0, 𝑥〉, 〈1, 𝑦〉})) ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑓‘{〈0, 𝑥〉, 〈1, 𝑦〉}) = (𝑔‘{〈0, 𝑥〉, 〈1, 𝑦〉}))) |
12 | | 2aryfvalel 45411 |
. . . . . . . 8
⊢ (𝑋 ∈ 𝑉 → (𝑓 ∈ (2-aryF 𝑋) ↔ 𝑓:(𝑋 ↑m {0, 1})⟶𝑋)) |
13 | | 2aryfvalel 45411 |
. . . . . . . 8
⊢ (𝑋 ∈ 𝑉 → (𝑔 ∈ (2-aryF 𝑋) ↔ 𝑔:(𝑋 ↑m {0, 1})⟶𝑋)) |
14 | 12, 13 | anbi12d 634 |
. . . . . . 7
⊢ (𝑋 ∈ 𝑉 → ((𝑓 ∈ (2-aryF 𝑋) ∧ 𝑔 ∈ (2-aryF 𝑋)) ↔ (𝑓:(𝑋 ↑m {0, 1})⟶𝑋 ∧ 𝑔:(𝑋 ↑m {0, 1})⟶𝑋))) |
15 | | ffn 6491 |
. . . . . . . . . . 11
⊢ (𝑓:(𝑋 ↑m {0, 1})⟶𝑋 → 𝑓 Fn (𝑋 ↑m {0,
1})) |
16 | 15 | adantr 485 |
. . . . . . . . . 10
⊢ ((𝑓:(𝑋 ↑m {0, 1})⟶𝑋 ∧ 𝑔:(𝑋 ↑m {0, 1})⟶𝑋) → 𝑓 Fn (𝑋 ↑m {0,
1})) |
17 | 16 | 3ad2ant2 1132 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝑉 ∧ (𝑓:(𝑋 ↑m {0, 1})⟶𝑋 ∧ 𝑔:(𝑋 ↑m {0, 1})⟶𝑋) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑓‘{〈0, 𝑥〉, 〈1, 𝑦〉}) = (𝑔‘{〈0, 𝑥〉, 〈1, 𝑦〉})) → 𝑓 Fn (𝑋 ↑m {0,
1})) |
18 | | ffn 6491 |
. . . . . . . . . . 11
⊢ (𝑔:(𝑋 ↑m {0, 1})⟶𝑋 → 𝑔 Fn (𝑋 ↑m {0,
1})) |
19 | 18 | adantl 486 |
. . . . . . . . . 10
⊢ ((𝑓:(𝑋 ↑m {0, 1})⟶𝑋 ∧ 𝑔:(𝑋 ↑m {0, 1})⟶𝑋) → 𝑔 Fn (𝑋 ↑m {0,
1})) |
20 | 19 | 3ad2ant2 1132 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝑉 ∧ (𝑓:(𝑋 ↑m {0, 1})⟶𝑋 ∧ 𝑔:(𝑋 ↑m {0, 1})⟶𝑋) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑓‘{〈0, 𝑥〉, 〈1, 𝑦〉}) = (𝑔‘{〈0, 𝑥〉, 〈1, 𝑦〉})) → 𝑔 Fn (𝑋 ↑m {0,
1})) |
21 | | elmapi 8431 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ (𝑋 ↑m {0, 1}) → 𝑧:{0, 1}⟶𝑋) |
22 | | 0ne1 11730 |
. . . . . . . . . . . . 13
⊢ 0 ≠
1 |
23 | | c0ex 10658 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
V |
24 | | 1ex 10660 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
V |
25 | 23, 24 | fprb 6940 |
. . . . . . . . . . . . 13
⊢ (0 ≠ 1
→ (𝑧:{0,
1}⟶𝑋 ↔
∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑋 𝑧 = {〈0, 𝑎〉, 〈1, 𝑏〉})) |
26 | 22, 25 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ (𝑧:{0, 1}⟶𝑋 ↔ ∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑋 𝑧 = {〈0, 𝑎〉, 〈1, 𝑏〉}) |
27 | 21, 26 | sylib 221 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ (𝑋 ↑m {0, 1}) →
∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑋 𝑧 = {〈0, 𝑎〉, 〈1, 𝑏〉}) |
28 | | opeq2 4756 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = 𝑎 → 〈0, 𝑥〉 = 〈0, 𝑎〉) |
29 | 28 | preq1d 4625 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑎 → {〈0, 𝑥〉, 〈1, 𝑦〉} = {〈0, 𝑎〉, 〈1, 𝑦〉}) |
30 | 29 | fveq2d 6655 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑎 → (𝑓‘{〈0, 𝑥〉, 〈1, 𝑦〉}) = (𝑓‘{〈0, 𝑎〉, 〈1, 𝑦〉})) |
31 | 29 | fveq2d 6655 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑎 → (𝑔‘{〈0, 𝑥〉, 〈1, 𝑦〉}) = (𝑔‘{〈0, 𝑎〉, 〈1, 𝑦〉})) |
32 | 30, 31 | eqeq12d 2775 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑎 → ((𝑓‘{〈0, 𝑥〉, 〈1, 𝑦〉}) = (𝑔‘{〈0, 𝑥〉, 〈1, 𝑦〉}) ↔ (𝑓‘{〈0, 𝑎〉, 〈1, 𝑦〉}) = (𝑔‘{〈0, 𝑎〉, 〈1, 𝑦〉}))) |
33 | | opeq2 4756 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 = 𝑏 → 〈1, 𝑦〉 = 〈1, 𝑏〉) |
34 | 33 | preq2d 4626 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 = 𝑏 → {〈0, 𝑎〉, 〈1, 𝑦〉} = {〈0, 𝑎〉, 〈1, 𝑏〉}) |
35 | 34 | fveq2d 6655 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = 𝑏 → (𝑓‘{〈0, 𝑎〉, 〈1, 𝑦〉}) = (𝑓‘{〈0, 𝑎〉, 〈1, 𝑏〉})) |
36 | 34 | fveq2d 6655 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = 𝑏 → (𝑔‘{〈0, 𝑎〉, 〈1, 𝑦〉}) = (𝑔‘{〈0, 𝑎〉, 〈1, 𝑏〉})) |
37 | 35, 36 | eqeq12d 2775 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = 𝑏 → ((𝑓‘{〈0, 𝑎〉, 〈1, 𝑦〉}) = (𝑔‘{〈0, 𝑎〉, 〈1, 𝑦〉}) ↔ (𝑓‘{〈0, 𝑎〉, 〈1, 𝑏〉}) = (𝑔‘{〈0, 𝑎〉, 〈1, 𝑏〉}))) |
38 | 32, 37 | rspc2va 3550 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑓‘{〈0, 𝑥〉, 〈1, 𝑦〉}) = (𝑔‘{〈0, 𝑥〉, 〈1, 𝑦〉})) → (𝑓‘{〈0, 𝑎〉, 〈1, 𝑏〉}) = (𝑔‘{〈0, 𝑎〉, 〈1, 𝑏〉})) |
39 | 38 | expcom 418 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑥 ∈
𝑋 ∀𝑦 ∈ 𝑋 (𝑓‘{〈0, 𝑥〉, 〈1, 𝑦〉}) = (𝑔‘{〈0, 𝑥〉, 〈1, 𝑦〉}) → ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → (𝑓‘{〈0, 𝑎〉, 〈1, 𝑏〉}) = (𝑔‘{〈0, 𝑎〉, 〈1, 𝑏〉}))) |
40 | 39 | 3ad2ant3 1133 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑋 ∈ 𝑉 ∧ (𝑓:(𝑋 ↑m {0, 1})⟶𝑋 ∧ 𝑔:(𝑋 ↑m {0, 1})⟶𝑋) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑓‘{〈0, 𝑥〉, 〈1, 𝑦〉}) = (𝑔‘{〈0, 𝑥〉, 〈1, 𝑦〉})) → ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → (𝑓‘{〈0, 𝑎〉, 〈1, 𝑏〉}) = (𝑔‘{〈0, 𝑎〉, 〈1, 𝑏〉}))) |
41 | 40 | com12 32 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → ((𝑋 ∈ 𝑉 ∧ (𝑓:(𝑋 ↑m {0, 1})⟶𝑋 ∧ 𝑔:(𝑋 ↑m {0, 1})⟶𝑋) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑓‘{〈0, 𝑥〉, 〈1, 𝑦〉}) = (𝑔‘{〈0, 𝑥〉, 〈1, 𝑦〉})) → (𝑓‘{〈0, 𝑎〉, 〈1, 𝑏〉}) = (𝑔‘{〈0, 𝑎〉, 〈1, 𝑏〉}))) |
42 | 41 | adantr 485 |
. . . . . . . . . . . . . 14
⊢ (((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ 𝑧 = {〈0, 𝑎〉, 〈1, 𝑏〉}) → ((𝑋 ∈ 𝑉 ∧ (𝑓:(𝑋 ↑m {0, 1})⟶𝑋 ∧ 𝑔:(𝑋 ↑m {0, 1})⟶𝑋) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑓‘{〈0, 𝑥〉, 〈1, 𝑦〉}) = (𝑔‘{〈0, 𝑥〉, 〈1, 𝑦〉})) → (𝑓‘{〈0, 𝑎〉, 〈1, 𝑏〉}) = (𝑔‘{〈0, 𝑎〉, 〈1, 𝑏〉}))) |
43 | | fveq2 6651 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = {〈0, 𝑎〉, 〈1, 𝑏〉} → (𝑓‘𝑧) = (𝑓‘{〈0, 𝑎〉, 〈1, 𝑏〉})) |
44 | | fveq2 6651 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = {〈0, 𝑎〉, 〈1, 𝑏〉} → (𝑔‘𝑧) = (𝑔‘{〈0, 𝑎〉, 〈1, 𝑏〉})) |
45 | 43, 44 | eqeq12d 2775 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = {〈0, 𝑎〉, 〈1, 𝑏〉} → ((𝑓‘𝑧) = (𝑔‘𝑧) ↔ (𝑓‘{〈0, 𝑎〉, 〈1, 𝑏〉}) = (𝑔‘{〈0, 𝑎〉, 〈1, 𝑏〉}))) |
46 | 45 | adantl 486 |
. . . . . . . . . . . . . 14
⊢ (((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ 𝑧 = {〈0, 𝑎〉, 〈1, 𝑏〉}) → ((𝑓‘𝑧) = (𝑔‘𝑧) ↔ (𝑓‘{〈0, 𝑎〉, 〈1, 𝑏〉}) = (𝑔‘{〈0, 𝑎〉, 〈1, 𝑏〉}))) |
47 | 42, 46 | sylibrd 262 |
. . . . . . . . . . . . 13
⊢ (((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ 𝑧 = {〈0, 𝑎〉, 〈1, 𝑏〉}) → ((𝑋 ∈ 𝑉 ∧ (𝑓:(𝑋 ↑m {0, 1})⟶𝑋 ∧ 𝑔:(𝑋 ↑m {0, 1})⟶𝑋) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑓‘{〈0, 𝑥〉, 〈1, 𝑦〉}) = (𝑔‘{〈0, 𝑥〉, 〈1, 𝑦〉})) → (𝑓‘𝑧) = (𝑔‘𝑧))) |
48 | 47 | ex 417 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → (𝑧 = {〈0, 𝑎〉, 〈1, 𝑏〉} → ((𝑋 ∈ 𝑉 ∧ (𝑓:(𝑋 ↑m {0, 1})⟶𝑋 ∧ 𝑔:(𝑋 ↑m {0, 1})⟶𝑋) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑓‘{〈0, 𝑥〉, 〈1, 𝑦〉}) = (𝑔‘{〈0, 𝑥〉, 〈1, 𝑦〉})) → (𝑓‘𝑧) = (𝑔‘𝑧)))) |
49 | 48 | rexlimivv 3214 |
. . . . . . . . . . 11
⊢
(∃𝑎 ∈
𝑋 ∃𝑏 ∈ 𝑋 𝑧 = {〈0, 𝑎〉, 〈1, 𝑏〉} → ((𝑋 ∈ 𝑉 ∧ (𝑓:(𝑋 ↑m {0, 1})⟶𝑋 ∧ 𝑔:(𝑋 ↑m {0, 1})⟶𝑋) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑓‘{〈0, 𝑥〉, 〈1, 𝑦〉}) = (𝑔‘{〈0, 𝑥〉, 〈1, 𝑦〉})) → (𝑓‘𝑧) = (𝑔‘𝑧))) |
50 | 27, 49 | syl 17 |
. . . . . . . . . 10
⊢ (𝑧 ∈ (𝑋 ↑m {0, 1}) → ((𝑋 ∈ 𝑉 ∧ (𝑓:(𝑋 ↑m {0, 1})⟶𝑋 ∧ 𝑔:(𝑋 ↑m {0, 1})⟶𝑋) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑓‘{〈0, 𝑥〉, 〈1, 𝑦〉}) = (𝑔‘{〈0, 𝑥〉, 〈1, 𝑦〉})) → (𝑓‘𝑧) = (𝑔‘𝑧))) |
51 | 50 | impcom 412 |
. . . . . . . . 9
⊢ (((𝑋 ∈ 𝑉 ∧ (𝑓:(𝑋 ↑m {0, 1})⟶𝑋 ∧ 𝑔:(𝑋 ↑m {0, 1})⟶𝑋) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑓‘{〈0, 𝑥〉, 〈1, 𝑦〉}) = (𝑔‘{〈0, 𝑥〉, 〈1, 𝑦〉})) ∧ 𝑧 ∈ (𝑋 ↑m {0, 1})) → (𝑓‘𝑧) = (𝑔‘𝑧)) |
52 | 17, 20, 51 | eqfnfvd 6789 |
. . . . . . . 8
⊢ ((𝑋 ∈ 𝑉 ∧ (𝑓:(𝑋 ↑m {0, 1})⟶𝑋 ∧ 𝑔:(𝑋 ↑m {0, 1})⟶𝑋) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑓‘{〈0, 𝑥〉, 〈1, 𝑦〉}) = (𝑔‘{〈0, 𝑥〉, 〈1, 𝑦〉})) → 𝑓 = 𝑔) |
53 | 52 | 3exp 1117 |
. . . . . . 7
⊢ (𝑋 ∈ 𝑉 → ((𝑓:(𝑋 ↑m {0, 1})⟶𝑋 ∧ 𝑔:(𝑋 ↑m {0, 1})⟶𝑋) → (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑓‘{〈0, 𝑥〉, 〈1, 𝑦〉}) = (𝑔‘{〈0, 𝑥〉, 〈1, 𝑦〉}) → 𝑓 = 𝑔))) |
54 | 14, 53 | sylbid 243 |
. . . . . 6
⊢ (𝑋 ∈ 𝑉 → ((𝑓 ∈ (2-aryF 𝑋) ∧ 𝑔 ∈ (2-aryF 𝑋)) → (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑓‘{〈0, 𝑥〉, 〈1, 𝑦〉}) = (𝑔‘{〈0, 𝑥〉, 〈1, 𝑦〉}) → 𝑓 = 𝑔))) |
55 | 54 | imp 411 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ (𝑓 ∈ (2-aryF 𝑋) ∧ 𝑔 ∈ (2-aryF 𝑋))) → (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑓‘{〈0, 𝑥〉, 〈1, 𝑦〉}) = (𝑔‘{〈0, 𝑥〉, 〈1, 𝑦〉}) → 𝑓 = 𝑔)) |
56 | 11, 55 | sylbid 243 |
. . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ (𝑓 ∈ (2-aryF 𝑋) ∧ 𝑔 ∈ (2-aryF 𝑋))) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (𝑓‘{〈0, 𝑥〉, 〈1, 𝑦〉})) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (𝑔‘{〈0, 𝑥〉, 〈1, 𝑦〉})) → 𝑓 = 𝑔)) |
57 | 7, 56 | sylbid 243 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ (𝑓 ∈ (2-aryF 𝑋) ∧ 𝑔 ∈ (2-aryF 𝑋))) → ((𝐻‘𝑓) = (𝐻‘𝑔) → 𝑓 = 𝑔)) |
58 | 57 | ralrimivva 3118 |
. 2
⊢ (𝑋 ∈ 𝑉 → ∀𝑓 ∈ (2-aryF 𝑋)∀𝑔 ∈ (2-aryF 𝑋)((𝐻‘𝑓) = (𝐻‘𝑔) → 𝑓 = 𝑔)) |
59 | | dff13 6998 |
. 2
⊢ (𝐻:(2-aryF 𝑋)–1-1→(𝑋 ↑m (𝑋 × 𝑋)) ↔ (𝐻:(2-aryF 𝑋)⟶(𝑋 ↑m (𝑋 × 𝑋)) ∧ ∀𝑓 ∈ (2-aryF 𝑋)∀𝑔 ∈ (2-aryF 𝑋)((𝐻‘𝑓) = (𝐻‘𝑔) → 𝑓 = 𝑔))) |
60 | 2, 58, 59 | sylanbrc 587 |
1
⊢ (𝑋 ∈ 𝑉 → 𝐻:(2-aryF 𝑋)–1-1→(𝑋 ↑m (𝑋 × 𝑋))) |