Step | Hyp | Ref
| Expression |
1 | | 2arymaptf.h |
. . 3
⊢ 𝐻 = (ℎ ∈ (2-aryF 𝑋) ↦ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (ℎ‘{〈0, 𝑥〉, 〈1, 𝑦〉}))) |
2 | 1 | 2arymaptf 45416 |
. 2
⊢ (𝑋 ∈ 𝑉 → 𝐻:(2-aryF 𝑋)⟶(𝑋 ↑m (𝑋 × 𝑋))) |
3 | | elmapi 8431 |
. . . . 5
⊢ (𝑓 ∈ (𝑋 ↑m (𝑋 × 𝑋)) → 𝑓:(𝑋 × 𝑋)⟶𝑋) |
4 | | eqid 2759 |
. . . . . 6
⊢ (𝑎 ∈ (𝑋 ↑m {0, 1}) ↦ ((𝑎‘0)𝑓(𝑎‘1))) = (𝑎 ∈ (𝑋 ↑m {0, 1}) ↦ ((𝑎‘0)𝑓(𝑎‘1))) |
5 | 4 | 2arympt 45413 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑓:(𝑋 × 𝑋)⟶𝑋) → (𝑎 ∈ (𝑋 ↑m {0, 1}) ↦ ((𝑎‘0)𝑓(𝑎‘1))) ∈ (2-aryF 𝑋)) |
6 | 3, 5 | sylan2 596 |
. . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑓 ∈ (𝑋 ↑m (𝑋 × 𝑋))) → (𝑎 ∈ (𝑋 ↑m {0, 1}) ↦ ((𝑎‘0)𝑓(𝑎‘1))) ∈ (2-aryF 𝑋)) |
7 | | fveq2 6651 |
. . . . . 6
⊢ (𝑔 = (𝑎 ∈ (𝑋 ↑m {0, 1}) ↦ ((𝑎‘0)𝑓(𝑎‘1))) → (𝐻‘𝑔) = (𝐻‘(𝑎 ∈ (𝑋 ↑m {0, 1}) ↦ ((𝑎‘0)𝑓(𝑎‘1))))) |
8 | 7 | eqeq2d 2770 |
. . . . 5
⊢ (𝑔 = (𝑎 ∈ (𝑋 ↑m {0, 1}) ↦ ((𝑎‘0)𝑓(𝑎‘1))) → (𝑓 = (𝐻‘𝑔) ↔ 𝑓 = (𝐻‘(𝑎 ∈ (𝑋 ↑m {0, 1}) ↦ ((𝑎‘0)𝑓(𝑎‘1)))))) |
9 | 8 | adantl 486 |
. . . 4
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑓 ∈ (𝑋 ↑m (𝑋 × 𝑋))) ∧ 𝑔 = (𝑎 ∈ (𝑋 ↑m {0, 1}) ↦ ((𝑎‘0)𝑓(𝑎‘1)))) → (𝑓 = (𝐻‘𝑔) ↔ 𝑓 = (𝐻‘(𝑎 ∈ (𝑋 ↑m {0, 1}) ↦ ((𝑎‘0)𝑓(𝑎‘1)))))) |
10 | | elmapfn 8440 |
. . . . . . 7
⊢ (𝑓 ∈ (𝑋 ↑m (𝑋 × 𝑋)) → 𝑓 Fn (𝑋 × 𝑋)) |
11 | 10 | adantl 486 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑓 ∈ (𝑋 ↑m (𝑋 × 𝑋))) → 𝑓 Fn (𝑋 × 𝑋)) |
12 | | fnov 7270 |
. . . . . 6
⊢ (𝑓 Fn (𝑋 × 𝑋) ↔ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (𝑥𝑓𝑦))) |
13 | 11, 12 | sylib 221 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑓 ∈ (𝑋 ↑m (𝑋 × 𝑋))) → 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (𝑥𝑓𝑦))) |
14 | | simp1r 1196 |
. . . . . . . 8
⊢ ((((𝑋 ∈ 𝑉 ∧ 𝑓 ∈ (𝑋 ↑m (𝑋 × 𝑋))) ∧ ℎ = (𝑎 ∈ (𝑋 ↑m {0, 1}) ↦ ((𝑎‘0)𝑓(𝑎‘1)))) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ℎ = (𝑎 ∈ (𝑋 ↑m {0, 1}) ↦ ((𝑎‘0)𝑓(𝑎‘1)))) |
15 | | fveq1 6650 |
. . . . . . . . . . 11
⊢ (𝑎 = {〈0, 𝑥〉, 〈1, 𝑦〉} → (𝑎‘0) = ({〈0, 𝑥〉, 〈1, 𝑦〉}‘0)) |
16 | | 0ne1 11730 |
. . . . . . . . . . . 12
⊢ 0 ≠
1 |
17 | | c0ex 10658 |
. . . . . . . . . . . . 13
⊢ 0 ∈
V |
18 | | vex 3411 |
. . . . . . . . . . . . 13
⊢ 𝑥 ∈ V |
19 | 17, 18 | fvpr1 6936 |
. . . . . . . . . . . 12
⊢ (0 ≠ 1
→ ({〈0, 𝑥〉,
〈1, 𝑦〉}‘0)
= 𝑥) |
20 | 16, 19 | ax-mp 5 |
. . . . . . . . . . 11
⊢
({〈0, 𝑥〉,
〈1, 𝑦〉}‘0)
= 𝑥 |
21 | 15, 20 | eqtrdi 2810 |
. . . . . . . . . 10
⊢ (𝑎 = {〈0, 𝑥〉, 〈1, 𝑦〉} → (𝑎‘0) = 𝑥) |
22 | | fveq1 6650 |
. . . . . . . . . . 11
⊢ (𝑎 = {〈0, 𝑥〉, 〈1, 𝑦〉} → (𝑎‘1) = ({〈0, 𝑥〉, 〈1, 𝑦〉}‘1)) |
23 | | 1ex 10660 |
. . . . . . . . . . . . 13
⊢ 1 ∈
V |
24 | | vex 3411 |
. . . . . . . . . . . . 13
⊢ 𝑦 ∈ V |
25 | 23, 24 | fvpr2 6937 |
. . . . . . . . . . . 12
⊢ (0 ≠ 1
→ ({〈0, 𝑥〉,
〈1, 𝑦〉}‘1)
= 𝑦) |
26 | 16, 25 | ax-mp 5 |
. . . . . . . . . . 11
⊢
({〈0, 𝑥〉,
〈1, 𝑦〉}‘1)
= 𝑦 |
27 | 22, 26 | eqtrdi 2810 |
. . . . . . . . . 10
⊢ (𝑎 = {〈0, 𝑥〉, 〈1, 𝑦〉} → (𝑎‘1) = 𝑦) |
28 | 21, 27 | oveq12d 7161 |
. . . . . . . . 9
⊢ (𝑎 = {〈0, 𝑥〉, 〈1, 𝑦〉} → ((𝑎‘0)𝑓(𝑎‘1)) = (𝑥𝑓𝑦)) |
29 | 28 | adantl 486 |
. . . . . . . 8
⊢
(((((𝑋 ∈ 𝑉 ∧ 𝑓 ∈ (𝑋 ↑m (𝑋 × 𝑋))) ∧ ℎ = (𝑎 ∈ (𝑋 ↑m {0, 1}) ↦ ((𝑎‘0)𝑓(𝑎‘1)))) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ 𝑎 = {〈0, 𝑥〉, 〈1, 𝑦〉}) → ((𝑎‘0)𝑓(𝑎‘1)) = (𝑥𝑓𝑦)) |
30 | 17, 23 | pm3.2i 475 |
. . . . . . . . . . . . . 14
⊢ (0 ∈
V ∧ 1 ∈ V) |
31 | | fprg 6901 |
. . . . . . . . . . . . . 14
⊢ (((0
∈ V ∧ 1 ∈ V) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ 0 ≠ 1) → {〈0, 𝑥〉, 〈1, 𝑦〉}:{0, 1}⟶{𝑥, 𝑦}) |
32 | 30, 16, 31 | mp3an13 1450 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → {〈0, 𝑥〉, 〈1, 𝑦〉}:{0, 1}⟶{𝑥, 𝑦}) |
33 | 32 | 3adant1 1128 |
. . . . . . . . . . . 12
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → {〈0, 𝑥〉, 〈1, 𝑦〉}:{0, 1}⟶{𝑥, 𝑦}) |
34 | | prssi 4704 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → {𝑥, 𝑦} ⊆ 𝑋) |
35 | 34 | 3adant1 1128 |
. . . . . . . . . . . 12
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → {𝑥, 𝑦} ⊆ 𝑋) |
36 | 33, 35 | fssd 6506 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → {〈0, 𝑥〉, 〈1, 𝑦〉}:{0, 1}⟶𝑋) |
37 | | simp1 1134 |
. . . . . . . . . . . 12
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → 𝑋 ∈ 𝑉) |
38 | | prex 5294 |
. . . . . . . . . . . . 13
⊢ {0, 1}
∈ V |
39 | 38 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → {0, 1} ∈ V) |
40 | 37, 39 | elmapd 8423 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ({〈0, 𝑥〉, 〈1, 𝑦〉} ∈ (𝑋 ↑m {0, 1}) ↔ {〈0,
𝑥〉, 〈1, 𝑦〉}:{0, 1}⟶𝑋)) |
41 | 36, 40 | mpbird 260 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → {〈0, 𝑥〉, 〈1, 𝑦〉} ∈ (𝑋 ↑m {0,
1})) |
42 | 41 | 3adant1r 1175 |
. . . . . . . . 9
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑓 ∈ (𝑋 ↑m (𝑋 × 𝑋))) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → {〈0, 𝑥〉, 〈1, 𝑦〉} ∈ (𝑋 ↑m {0,
1})) |
43 | 42 | 3adant1r 1175 |
. . . . . . . 8
⊢ ((((𝑋 ∈ 𝑉 ∧ 𝑓 ∈ (𝑋 ↑m (𝑋 × 𝑋))) ∧ ℎ = (𝑎 ∈ (𝑋 ↑m {0, 1}) ↦ ((𝑎‘0)𝑓(𝑎‘1)))) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → {〈0, 𝑥〉, 〈1, 𝑦〉} ∈ (𝑋 ↑m {0,
1})) |
44 | | ovexd 7178 |
. . . . . . . 8
⊢ ((((𝑋 ∈ 𝑉 ∧ 𝑓 ∈ (𝑋 ↑m (𝑋 × 𝑋))) ∧ ℎ = (𝑎 ∈ (𝑋 ↑m {0, 1}) ↦ ((𝑎‘0)𝑓(𝑎‘1)))) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥𝑓𝑦) ∈ V) |
45 | | nfv 1916 |
. . . . . . . . . 10
⊢
Ⅎ𝑎(𝑋 ∈ 𝑉 ∧ 𝑓 ∈ (𝑋 ↑m (𝑋 × 𝑋))) |
46 | | nfmpt1 5123 |
. . . . . . . . . . 11
⊢
Ⅎ𝑎(𝑎 ∈ (𝑋 ↑m {0, 1}) ↦ ((𝑎‘0)𝑓(𝑎‘1))) |
47 | 46 | nfeq2 2934 |
. . . . . . . . . 10
⊢
Ⅎ𝑎 ℎ = (𝑎 ∈ (𝑋 ↑m {0, 1}) ↦ ((𝑎‘0)𝑓(𝑎‘1))) |
48 | 45, 47 | nfan 1901 |
. . . . . . . . 9
⊢
Ⅎ𝑎((𝑋 ∈ 𝑉 ∧ 𝑓 ∈ (𝑋 ↑m (𝑋 × 𝑋))) ∧ ℎ = (𝑎 ∈ (𝑋 ↑m {0, 1}) ↦ ((𝑎‘0)𝑓(𝑎‘1)))) |
49 | | nfv 1916 |
. . . . . . . . 9
⊢
Ⅎ𝑎 𝑥 ∈ 𝑋 |
50 | | nfv 1916 |
. . . . . . . . 9
⊢
Ⅎ𝑎 𝑦 ∈ 𝑋 |
51 | 48, 49, 50 | nf3an 1903 |
. . . . . . . 8
⊢
Ⅎ𝑎(((𝑋 ∈ 𝑉 ∧ 𝑓 ∈ (𝑋 ↑m (𝑋 × 𝑋))) ∧ ℎ = (𝑎 ∈ (𝑋 ↑m {0, 1}) ↦ ((𝑎‘0)𝑓(𝑎‘1)))) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) |
52 | | nfcv 2917 |
. . . . . . . 8
⊢
Ⅎ𝑎{〈0, 𝑥〉, 〈1, 𝑦〉} |
53 | | nfcv 2917 |
. . . . . . . 8
⊢
Ⅎ𝑎(𝑥𝑓𝑦) |
54 | 14, 29, 43, 44, 51, 52, 53 | fvmptdf 6758 |
. . . . . . 7
⊢ ((((𝑋 ∈ 𝑉 ∧ 𝑓 ∈ (𝑋 ↑m (𝑋 × 𝑋))) ∧ ℎ = (𝑎 ∈ (𝑋 ↑m {0, 1}) ↦ ((𝑎‘0)𝑓(𝑎‘1)))) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (ℎ‘{〈0, 𝑥〉, 〈1, 𝑦〉}) = (𝑥𝑓𝑦)) |
55 | 54 | mpoeq3dva 7218 |
. . . . . 6
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑓 ∈ (𝑋 ↑m (𝑋 × 𝑋))) ∧ ℎ = (𝑎 ∈ (𝑋 ↑m {0, 1}) ↦ ((𝑎‘0)𝑓(𝑎‘1)))) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (ℎ‘{〈0, 𝑥〉, 〈1, 𝑦〉})) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (𝑥𝑓𝑦))) |
56 | | mpoexga 7773 |
. . . . . . . 8
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (𝑥𝑓𝑦)) ∈ V) |
57 | 56 | anidms 571 |
. . . . . . 7
⊢ (𝑋 ∈ 𝑉 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (𝑥𝑓𝑦)) ∈ V) |
58 | 57 | adantr 485 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑓 ∈ (𝑋 ↑m (𝑋 × 𝑋))) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (𝑥𝑓𝑦)) ∈ V) |
59 | 1, 55, 6, 58 | fvmptd2 6760 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑓 ∈ (𝑋 ↑m (𝑋 × 𝑋))) → (𝐻‘(𝑎 ∈ (𝑋 ↑m {0, 1}) ↦ ((𝑎‘0)𝑓(𝑎‘1)))) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (𝑥𝑓𝑦))) |
60 | 13, 59 | eqtr4d 2797 |
. . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑓 ∈ (𝑋 ↑m (𝑋 × 𝑋))) → 𝑓 = (𝐻‘(𝑎 ∈ (𝑋 ↑m {0, 1}) ↦ ((𝑎‘0)𝑓(𝑎‘1))))) |
61 | 6, 9, 60 | rspcedvd 3542 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑓 ∈ (𝑋 ↑m (𝑋 × 𝑋))) → ∃𝑔 ∈ (2-aryF 𝑋)𝑓 = (𝐻‘𝑔)) |
62 | 61 | ralrimiva 3111 |
. 2
⊢ (𝑋 ∈ 𝑉 → ∀𝑓 ∈ (𝑋 ↑m (𝑋 × 𝑋))∃𝑔 ∈ (2-aryF 𝑋)𝑓 = (𝐻‘𝑔)) |
63 | | dffo3 6852 |
. 2
⊢ (𝐻:(2-aryF 𝑋)–onto→(𝑋 ↑m (𝑋 × 𝑋)) ↔ (𝐻:(2-aryF 𝑋)⟶(𝑋 ↑m (𝑋 × 𝑋)) ∧ ∀𝑓 ∈ (𝑋 ↑m (𝑋 × 𝑋))∃𝑔 ∈ (2-aryF 𝑋)𝑓 = (𝐻‘𝑔))) |
64 | 2, 62, 63 | sylanbrc 587 |
1
⊢ (𝑋 ∈ 𝑉 → 𝐻:(2-aryF 𝑋)–onto→(𝑋 ↑m (𝑋 × 𝑋))) |