Step | Hyp | Ref
| Expression |
1 | | 1arymaptfv.h |
. . 3
⊢ 𝐻 = (ℎ ∈ (1-aryF 𝑋) ↦ (𝑥 ∈ 𝑋 ↦ (ℎ‘{〈0, 𝑥〉}))) |
2 | 1 | 1arymaptf 45614 |
. 2
⊢ (𝑋 ∈ 𝑉 → 𝐻:(1-aryF 𝑋)⟶(𝑋 ↑m 𝑋)) |
3 | | elmapi 8519 |
. . . . 5
⊢ (𝑓 ∈ (𝑋 ↑m 𝑋) → 𝑓:𝑋⟶𝑋) |
4 | | eqid 2734 |
. . . . . 6
⊢ (𝑎 ∈ (𝑋 ↑m {0}) ↦ (𝑓‘(𝑎‘0))) = (𝑎 ∈ (𝑋 ↑m {0}) ↦ (𝑓‘(𝑎‘0))) |
5 | 4 | 1arympt1 45611 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑓:𝑋⟶𝑋) → (𝑎 ∈ (𝑋 ↑m {0}) ↦ (𝑓‘(𝑎‘0))) ∈ (1-aryF 𝑋)) |
6 | 3, 5 | sylan2 596 |
. . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑓 ∈ (𝑋 ↑m 𝑋)) → (𝑎 ∈ (𝑋 ↑m {0}) ↦ (𝑓‘(𝑎‘0))) ∈ (1-aryF 𝑋)) |
7 | | fveq2 6706 |
. . . . . 6
⊢ (𝑔 = (𝑎 ∈ (𝑋 ↑m {0}) ↦ (𝑓‘(𝑎‘0))) → (𝐻‘𝑔) = (𝐻‘(𝑎 ∈ (𝑋 ↑m {0}) ↦ (𝑓‘(𝑎‘0))))) |
8 | 7 | eqeq2d 2745 |
. . . . 5
⊢ (𝑔 = (𝑎 ∈ (𝑋 ↑m {0}) ↦ (𝑓‘(𝑎‘0))) → (𝑓 = (𝐻‘𝑔) ↔ 𝑓 = (𝐻‘(𝑎 ∈ (𝑋 ↑m {0}) ↦ (𝑓‘(𝑎‘0)))))) |
9 | 8 | adantl 485 |
. . . 4
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑓 ∈ (𝑋 ↑m 𝑋)) ∧ 𝑔 = (𝑎 ∈ (𝑋 ↑m {0}) ↦ (𝑓‘(𝑎‘0)))) → (𝑓 = (𝐻‘𝑔) ↔ 𝑓 = (𝐻‘(𝑎 ∈ (𝑋 ↑m {0}) ↦ (𝑓‘(𝑎‘0)))))) |
10 | 3 | adantl 485 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑓 ∈ (𝑋 ↑m 𝑋)) → 𝑓:𝑋⟶𝑋) |
11 | 10 | feqmptd 6769 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑓 ∈ (𝑋 ↑m 𝑋)) → 𝑓 = (𝑥 ∈ 𝑋 ↦ (𝑓‘𝑥))) |
12 | | simplr 769 |
. . . . . . . 8
⊢ ((((𝑋 ∈ 𝑉 ∧ 𝑓 ∈ (𝑋 ↑m 𝑋)) ∧ ℎ = (𝑎 ∈ (𝑋 ↑m {0}) ↦ (𝑓‘(𝑎‘0)))) ∧ 𝑥 ∈ 𝑋) → ℎ = (𝑎 ∈ (𝑋 ↑m {0}) ↦ (𝑓‘(𝑎‘0)))) |
13 | | fveq1 6705 |
. . . . . . . . . . 11
⊢ (𝑎 = {〈0, 𝑥〉} → (𝑎‘0) = ({〈0, 𝑥〉}‘0)) |
14 | | c0ex 10810 |
. . . . . . . . . . . 12
⊢ 0 ∈
V |
15 | | vex 3405 |
. . . . . . . . . . . 12
⊢ 𝑥 ∈ V |
16 | 14, 15 | fvsn 6985 |
. . . . . . . . . . 11
⊢
({〈0, 𝑥〉}‘0) = 𝑥 |
17 | 13, 16 | eqtrdi 2790 |
. . . . . . . . . 10
⊢ (𝑎 = {〈0, 𝑥〉} → (𝑎‘0) = 𝑥) |
18 | 17 | fveq2d 6710 |
. . . . . . . . 9
⊢ (𝑎 = {〈0, 𝑥〉} → (𝑓‘(𝑎‘0)) = (𝑓‘𝑥)) |
19 | 18 | adantl 485 |
. . . . . . . 8
⊢
(((((𝑋 ∈ 𝑉 ∧ 𝑓 ∈ (𝑋 ↑m 𝑋)) ∧ ℎ = (𝑎 ∈ (𝑋 ↑m {0}) ↦ (𝑓‘(𝑎‘0)))) ∧ 𝑥 ∈ 𝑋) ∧ 𝑎 = {〈0, 𝑥〉}) → (𝑓‘(𝑎‘0)) = (𝑓‘𝑥)) |
20 | 14 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑥 ∈ 𝑋) → 0 ∈ V) |
21 | | simpr 488 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑋) |
22 | 20, 21 | fsnd 6692 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑥 ∈ 𝑋) → {〈0, 𝑥〉}:{0}⟶𝑋) |
23 | | snex 5313 |
. . . . . . . . . . . 12
⊢ {0}
∈ V |
24 | 23 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝑋 → {0} ∈ V) |
25 | | elmapg 8510 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝑉 ∧ {0} ∈ V) → ({〈0, 𝑥〉} ∈ (𝑋 ↑m {0}) ↔
{〈0, 𝑥〉}:{0}⟶𝑋)) |
26 | 24, 25 | sylan2 596 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑥 ∈ 𝑋) → ({〈0, 𝑥〉} ∈ (𝑋 ↑m {0}) ↔ {〈0,
𝑥〉}:{0}⟶𝑋)) |
27 | 22, 26 | mpbird 260 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑥 ∈ 𝑋) → {〈0, 𝑥〉} ∈ (𝑋 ↑m {0})) |
28 | 27 | ad4ant14 752 |
. . . . . . . 8
⊢ ((((𝑋 ∈ 𝑉 ∧ 𝑓 ∈ (𝑋 ↑m 𝑋)) ∧ ℎ = (𝑎 ∈ (𝑋 ↑m {0}) ↦ (𝑓‘(𝑎‘0)))) ∧ 𝑥 ∈ 𝑋) → {〈0, 𝑥〉} ∈ (𝑋 ↑m {0})) |
29 | | fvexd 6721 |
. . . . . . . 8
⊢ ((((𝑋 ∈ 𝑉 ∧ 𝑓 ∈ (𝑋 ↑m 𝑋)) ∧ ℎ = (𝑎 ∈ (𝑋 ↑m {0}) ↦ (𝑓‘(𝑎‘0)))) ∧ 𝑥 ∈ 𝑋) → (𝑓‘𝑥) ∈ V) |
30 | | nfv 1922 |
. . . . . . . . . 10
⊢
Ⅎ𝑎(𝑋 ∈ 𝑉 ∧ 𝑓 ∈ (𝑋 ↑m 𝑋)) |
31 | | nfmpt1 5142 |
. . . . . . . . . . 11
⊢
Ⅎ𝑎(𝑎 ∈ (𝑋 ↑m {0}) ↦ (𝑓‘(𝑎‘0))) |
32 | 31 | nfeq2 2917 |
. . . . . . . . . 10
⊢
Ⅎ𝑎 ℎ = (𝑎 ∈ (𝑋 ↑m {0}) ↦ (𝑓‘(𝑎‘0))) |
33 | 30, 32 | nfan 1907 |
. . . . . . . . 9
⊢
Ⅎ𝑎((𝑋 ∈ 𝑉 ∧ 𝑓 ∈ (𝑋 ↑m 𝑋)) ∧ ℎ = (𝑎 ∈ (𝑋 ↑m {0}) ↦ (𝑓‘(𝑎‘0)))) |
34 | | nfv 1922 |
. . . . . . . . 9
⊢
Ⅎ𝑎 𝑥 ∈ 𝑋 |
35 | 33, 34 | nfan 1907 |
. . . . . . . 8
⊢
Ⅎ𝑎(((𝑋 ∈ 𝑉 ∧ 𝑓 ∈ (𝑋 ↑m 𝑋)) ∧ ℎ = (𝑎 ∈ (𝑋 ↑m {0}) ↦ (𝑓‘(𝑎‘0)))) ∧ 𝑥 ∈ 𝑋) |
36 | | nfcv 2900 |
. . . . . . . 8
⊢
Ⅎ𝑎{〈0, 𝑥〉} |
37 | | nfcv 2900 |
. . . . . . . 8
⊢
Ⅎ𝑎(𝑓‘𝑥) |
38 | 12, 19, 28, 29, 35, 36, 37 | fvmptdf 6813 |
. . . . . . 7
⊢ ((((𝑋 ∈ 𝑉 ∧ 𝑓 ∈ (𝑋 ↑m 𝑋)) ∧ ℎ = (𝑎 ∈ (𝑋 ↑m {0}) ↦ (𝑓‘(𝑎‘0)))) ∧ 𝑥 ∈ 𝑋) → (ℎ‘{〈0, 𝑥〉}) = (𝑓‘𝑥)) |
39 | 38 | mpteq2dva 5139 |
. . . . . 6
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑓 ∈ (𝑋 ↑m 𝑋)) ∧ ℎ = (𝑎 ∈ (𝑋 ↑m {0}) ↦ (𝑓‘(𝑎‘0)))) → (𝑥 ∈ 𝑋 ↦ (ℎ‘{〈0, 𝑥〉})) = (𝑥 ∈ 𝑋 ↦ (𝑓‘𝑥))) |
40 | | simpl 486 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑓 ∈ (𝑋 ↑m 𝑋)) → 𝑋 ∈ 𝑉) |
41 | 40 | mptexd 7029 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑓 ∈ (𝑋 ↑m 𝑋)) → (𝑥 ∈ 𝑋 ↦ (𝑓‘𝑥)) ∈ V) |
42 | 1, 39, 6, 41 | fvmptd2 6815 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑓 ∈ (𝑋 ↑m 𝑋)) → (𝐻‘(𝑎 ∈ (𝑋 ↑m {0}) ↦ (𝑓‘(𝑎‘0)))) = (𝑥 ∈ 𝑋 ↦ (𝑓‘𝑥))) |
43 | 11, 42 | eqtr4d 2777 |
. . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑓 ∈ (𝑋 ↑m 𝑋)) → 𝑓 = (𝐻‘(𝑎 ∈ (𝑋 ↑m {0}) ↦ (𝑓‘(𝑎‘0))))) |
44 | 6, 9, 43 | rspcedvd 3533 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑓 ∈ (𝑋 ↑m 𝑋)) → ∃𝑔 ∈ (1-aryF 𝑋)𝑓 = (𝐻‘𝑔)) |
45 | 44 | ralrimiva 3098 |
. 2
⊢ (𝑋 ∈ 𝑉 → ∀𝑓 ∈ (𝑋 ↑m 𝑋)∃𝑔 ∈ (1-aryF 𝑋)𝑓 = (𝐻‘𝑔)) |
46 | | dffo3 6910 |
. 2
⊢ (𝐻:(1-aryF 𝑋)–onto→(𝑋 ↑m 𝑋) ↔ (𝐻:(1-aryF 𝑋)⟶(𝑋 ↑m 𝑋) ∧ ∀𝑓 ∈ (𝑋 ↑m 𝑋)∃𝑔 ∈ (1-aryF 𝑋)𝑓 = (𝐻‘𝑔))) |
47 | 2, 45, 46 | sylanbrc 586 |
1
⊢ (𝑋 ∈ 𝑉 → 𝐻:(1-aryF 𝑋)–onto→(𝑋 ↑m 𝑋)) |