| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 2arymaptf.h | . . 3
⊢ 𝐻 = (ℎ ∈ (2-aryF 𝑋) ↦ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (ℎ‘{〈0, 𝑥〉, 〈1, 𝑦〉}))) | 
| 2 | 1 | 2arymaptf 48573 | . 2
⊢ (𝑋 ∈ 𝑉 → 𝐻:(2-aryF 𝑋)⟶(𝑋 ↑m (𝑋 × 𝑋))) | 
| 3 |  | elmapi 8889 | . . . . 5
⊢ (𝑓 ∈ (𝑋 ↑m (𝑋 × 𝑋)) → 𝑓:(𝑋 × 𝑋)⟶𝑋) | 
| 4 |  | eqid 2737 | . . . . . 6
⊢ (𝑎 ∈ (𝑋 ↑m {0, 1}) ↦ ((𝑎‘0)𝑓(𝑎‘1))) = (𝑎 ∈ (𝑋 ↑m {0, 1}) ↦ ((𝑎‘0)𝑓(𝑎‘1))) | 
| 5 | 4 | 2arympt 48570 | . . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑓:(𝑋 × 𝑋)⟶𝑋) → (𝑎 ∈ (𝑋 ↑m {0, 1}) ↦ ((𝑎‘0)𝑓(𝑎‘1))) ∈ (2-aryF 𝑋)) | 
| 6 | 3, 5 | sylan2 593 | . . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑓 ∈ (𝑋 ↑m (𝑋 × 𝑋))) → (𝑎 ∈ (𝑋 ↑m {0, 1}) ↦ ((𝑎‘0)𝑓(𝑎‘1))) ∈ (2-aryF 𝑋)) | 
| 7 |  | fveq2 6906 | . . . . . 6
⊢ (𝑔 = (𝑎 ∈ (𝑋 ↑m {0, 1}) ↦ ((𝑎‘0)𝑓(𝑎‘1))) → (𝐻‘𝑔) = (𝐻‘(𝑎 ∈ (𝑋 ↑m {0, 1}) ↦ ((𝑎‘0)𝑓(𝑎‘1))))) | 
| 8 | 7 | eqeq2d 2748 | . . . . 5
⊢ (𝑔 = (𝑎 ∈ (𝑋 ↑m {0, 1}) ↦ ((𝑎‘0)𝑓(𝑎‘1))) → (𝑓 = (𝐻‘𝑔) ↔ 𝑓 = (𝐻‘(𝑎 ∈ (𝑋 ↑m {0, 1}) ↦ ((𝑎‘0)𝑓(𝑎‘1)))))) | 
| 9 | 8 | adantl 481 | . . . 4
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑓 ∈ (𝑋 ↑m (𝑋 × 𝑋))) ∧ 𝑔 = (𝑎 ∈ (𝑋 ↑m {0, 1}) ↦ ((𝑎‘0)𝑓(𝑎‘1)))) → (𝑓 = (𝐻‘𝑔) ↔ 𝑓 = (𝐻‘(𝑎 ∈ (𝑋 ↑m {0, 1}) ↦ ((𝑎‘0)𝑓(𝑎‘1)))))) | 
| 10 |  | elmapfn 8905 | . . . . . . 7
⊢ (𝑓 ∈ (𝑋 ↑m (𝑋 × 𝑋)) → 𝑓 Fn (𝑋 × 𝑋)) | 
| 11 | 10 | adantl 481 | . . . . . 6
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑓 ∈ (𝑋 ↑m (𝑋 × 𝑋))) → 𝑓 Fn (𝑋 × 𝑋)) | 
| 12 |  | fnov 7564 | . . . . . 6
⊢ (𝑓 Fn (𝑋 × 𝑋) ↔ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (𝑥𝑓𝑦))) | 
| 13 | 11, 12 | sylib 218 | . . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑓 ∈ (𝑋 ↑m (𝑋 × 𝑋))) → 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (𝑥𝑓𝑦))) | 
| 14 |  | simp1r 1199 | . . . . . . . 8
⊢ ((((𝑋 ∈ 𝑉 ∧ 𝑓 ∈ (𝑋 ↑m (𝑋 × 𝑋))) ∧ ℎ = (𝑎 ∈ (𝑋 ↑m {0, 1}) ↦ ((𝑎‘0)𝑓(𝑎‘1)))) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ℎ = (𝑎 ∈ (𝑋 ↑m {0, 1}) ↦ ((𝑎‘0)𝑓(𝑎‘1)))) | 
| 15 |  | fveq1 6905 | . . . . . . . . . . 11
⊢ (𝑎 = {〈0, 𝑥〉, 〈1, 𝑦〉} → (𝑎‘0) = ({〈0, 𝑥〉, 〈1, 𝑦〉}‘0)) | 
| 16 |  | 0ne1 12337 | . . . . . . . . . . . 12
⊢ 0 ≠
1 | 
| 17 |  | c0ex 11255 | . . . . . . . . . . . . 13
⊢ 0 ∈
V | 
| 18 |  | vex 3484 | . . . . . . . . . . . . 13
⊢ 𝑥 ∈ V | 
| 19 | 17, 18 | fvpr1 7212 | . . . . . . . . . . . 12
⊢ (0 ≠ 1
→ ({〈0, 𝑥〉,
〈1, 𝑦〉}‘0)
= 𝑥) | 
| 20 | 16, 19 | ax-mp 5 | . . . . . . . . . . 11
⊢
({〈0, 𝑥〉,
〈1, 𝑦〉}‘0)
= 𝑥 | 
| 21 | 15, 20 | eqtrdi 2793 | . . . . . . . . . 10
⊢ (𝑎 = {〈0, 𝑥〉, 〈1, 𝑦〉} → (𝑎‘0) = 𝑥) | 
| 22 |  | fveq1 6905 | . . . . . . . . . . 11
⊢ (𝑎 = {〈0, 𝑥〉, 〈1, 𝑦〉} → (𝑎‘1) = ({〈0, 𝑥〉, 〈1, 𝑦〉}‘1)) | 
| 23 |  | 1ex 11257 | . . . . . . . . . . . . 13
⊢ 1 ∈
V | 
| 24 |  | vex 3484 | . . . . . . . . . . . . 13
⊢ 𝑦 ∈ V | 
| 25 | 23, 24 | fvpr2 7213 | . . . . . . . . . . . 12
⊢ (0 ≠ 1
→ ({〈0, 𝑥〉,
〈1, 𝑦〉}‘1)
= 𝑦) | 
| 26 | 16, 25 | ax-mp 5 | . . . . . . . . . . 11
⊢
({〈0, 𝑥〉,
〈1, 𝑦〉}‘1)
= 𝑦 | 
| 27 | 22, 26 | eqtrdi 2793 | . . . . . . . . . 10
⊢ (𝑎 = {〈0, 𝑥〉, 〈1, 𝑦〉} → (𝑎‘1) = 𝑦) | 
| 28 | 21, 27 | oveq12d 7449 | . . . . . . . . 9
⊢ (𝑎 = {〈0, 𝑥〉, 〈1, 𝑦〉} → ((𝑎‘0)𝑓(𝑎‘1)) = (𝑥𝑓𝑦)) | 
| 29 | 28 | adantl 481 | . . . . . . . 8
⊢
(((((𝑋 ∈ 𝑉 ∧ 𝑓 ∈ (𝑋 ↑m (𝑋 × 𝑋))) ∧ ℎ = (𝑎 ∈ (𝑋 ↑m {0, 1}) ↦ ((𝑎‘0)𝑓(𝑎‘1)))) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ 𝑎 = {〈0, 𝑥〉, 〈1, 𝑦〉}) → ((𝑎‘0)𝑓(𝑎‘1)) = (𝑥𝑓𝑦)) | 
| 30 | 17, 23 | pm3.2i 470 | . . . . . . . . . . . . . 14
⊢ (0 ∈
V ∧ 1 ∈ V) | 
| 31 |  | fprg 7175 | . . . . . . . . . . . . . 14
⊢ (((0
∈ V ∧ 1 ∈ V) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ 0 ≠ 1) → {〈0, 𝑥〉, 〈1, 𝑦〉}:{0, 1}⟶{𝑥, 𝑦}) | 
| 32 | 30, 16, 31 | mp3an13 1454 | . . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → {〈0, 𝑥〉, 〈1, 𝑦〉}:{0, 1}⟶{𝑥, 𝑦}) | 
| 33 | 32 | 3adant1 1131 | . . . . . . . . . . . 12
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → {〈0, 𝑥〉, 〈1, 𝑦〉}:{0, 1}⟶{𝑥, 𝑦}) | 
| 34 |  | prssi 4821 | . . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → {𝑥, 𝑦} ⊆ 𝑋) | 
| 35 | 34 | 3adant1 1131 | . . . . . . . . . . . 12
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → {𝑥, 𝑦} ⊆ 𝑋) | 
| 36 | 33, 35 | fssd 6753 | . . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → {〈0, 𝑥〉, 〈1, 𝑦〉}:{0, 1}⟶𝑋) | 
| 37 |  | simp1 1137 | . . . . . . . . . . . 12
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → 𝑋 ∈ 𝑉) | 
| 38 |  | prex 5437 | . . . . . . . . . . . . 13
⊢ {0, 1}
∈ V | 
| 39 | 38 | a1i 11 | . . . . . . . . . . . 12
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → {0, 1} ∈ V) | 
| 40 | 37, 39 | elmapd 8880 | . . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ({〈0, 𝑥〉, 〈1, 𝑦〉} ∈ (𝑋 ↑m {0, 1}) ↔ {〈0,
𝑥〉, 〈1, 𝑦〉}:{0, 1}⟶𝑋)) | 
| 41 | 36, 40 | mpbird 257 | . . . . . . . . . 10
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → {〈0, 𝑥〉, 〈1, 𝑦〉} ∈ (𝑋 ↑m {0,
1})) | 
| 42 | 41 | 3adant1r 1178 | . . . . . . . . 9
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑓 ∈ (𝑋 ↑m (𝑋 × 𝑋))) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → {〈0, 𝑥〉, 〈1, 𝑦〉} ∈ (𝑋 ↑m {0,
1})) | 
| 43 | 42 | 3adant1r 1178 | . . . . . . . 8
⊢ ((((𝑋 ∈ 𝑉 ∧ 𝑓 ∈ (𝑋 ↑m (𝑋 × 𝑋))) ∧ ℎ = (𝑎 ∈ (𝑋 ↑m {0, 1}) ↦ ((𝑎‘0)𝑓(𝑎‘1)))) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → {〈0, 𝑥〉, 〈1, 𝑦〉} ∈ (𝑋 ↑m {0,
1})) | 
| 44 |  | ovexd 7466 | . . . . . . . 8
⊢ ((((𝑋 ∈ 𝑉 ∧ 𝑓 ∈ (𝑋 ↑m (𝑋 × 𝑋))) ∧ ℎ = (𝑎 ∈ (𝑋 ↑m {0, 1}) ↦ ((𝑎‘0)𝑓(𝑎‘1)))) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥𝑓𝑦) ∈ V) | 
| 45 |  | nfv 1914 | . . . . . . . . . 10
⊢
Ⅎ𝑎(𝑋 ∈ 𝑉 ∧ 𝑓 ∈ (𝑋 ↑m (𝑋 × 𝑋))) | 
| 46 |  | nfmpt1 5250 | . . . . . . . . . . 11
⊢
Ⅎ𝑎(𝑎 ∈ (𝑋 ↑m {0, 1}) ↦ ((𝑎‘0)𝑓(𝑎‘1))) | 
| 47 | 46 | nfeq2 2923 | . . . . . . . . . 10
⊢
Ⅎ𝑎 ℎ = (𝑎 ∈ (𝑋 ↑m {0, 1}) ↦ ((𝑎‘0)𝑓(𝑎‘1))) | 
| 48 | 45, 47 | nfan 1899 | . . . . . . . . 9
⊢
Ⅎ𝑎((𝑋 ∈ 𝑉 ∧ 𝑓 ∈ (𝑋 ↑m (𝑋 × 𝑋))) ∧ ℎ = (𝑎 ∈ (𝑋 ↑m {0, 1}) ↦ ((𝑎‘0)𝑓(𝑎‘1)))) | 
| 49 |  | nfv 1914 | . . . . . . . . 9
⊢
Ⅎ𝑎 𝑥 ∈ 𝑋 | 
| 50 |  | nfv 1914 | . . . . . . . . 9
⊢
Ⅎ𝑎 𝑦 ∈ 𝑋 | 
| 51 | 48, 49, 50 | nf3an 1901 | . . . . . . . 8
⊢
Ⅎ𝑎(((𝑋 ∈ 𝑉 ∧ 𝑓 ∈ (𝑋 ↑m (𝑋 × 𝑋))) ∧ ℎ = (𝑎 ∈ (𝑋 ↑m {0, 1}) ↦ ((𝑎‘0)𝑓(𝑎‘1)))) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) | 
| 52 |  | nfcv 2905 | . . . . . . . 8
⊢
Ⅎ𝑎{〈0, 𝑥〉, 〈1, 𝑦〉} | 
| 53 |  | nfcv 2905 | . . . . . . . 8
⊢
Ⅎ𝑎(𝑥𝑓𝑦) | 
| 54 | 14, 29, 43, 44, 51, 52, 53 | fvmptdf 7022 | . . . . . . 7
⊢ ((((𝑋 ∈ 𝑉 ∧ 𝑓 ∈ (𝑋 ↑m (𝑋 × 𝑋))) ∧ ℎ = (𝑎 ∈ (𝑋 ↑m {0, 1}) ↦ ((𝑎‘0)𝑓(𝑎‘1)))) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (ℎ‘{〈0, 𝑥〉, 〈1, 𝑦〉}) = (𝑥𝑓𝑦)) | 
| 55 | 54 | mpoeq3dva 7510 | . . . . . 6
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑓 ∈ (𝑋 ↑m (𝑋 × 𝑋))) ∧ ℎ = (𝑎 ∈ (𝑋 ↑m {0, 1}) ↦ ((𝑎‘0)𝑓(𝑎‘1)))) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (ℎ‘{〈0, 𝑥〉, 〈1, 𝑦〉})) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (𝑥𝑓𝑦))) | 
| 56 |  | mpoexga 8102 | . . . . . . . 8
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (𝑥𝑓𝑦)) ∈ V) | 
| 57 | 56 | anidms 566 | . . . . . . 7
⊢ (𝑋 ∈ 𝑉 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (𝑥𝑓𝑦)) ∈ V) | 
| 58 | 57 | adantr 480 | . . . . . 6
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑓 ∈ (𝑋 ↑m (𝑋 × 𝑋))) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (𝑥𝑓𝑦)) ∈ V) | 
| 59 | 1, 55, 6, 58 | fvmptd2 7024 | . . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑓 ∈ (𝑋 ↑m (𝑋 × 𝑋))) → (𝐻‘(𝑎 ∈ (𝑋 ↑m {0, 1}) ↦ ((𝑎‘0)𝑓(𝑎‘1)))) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (𝑥𝑓𝑦))) | 
| 60 | 13, 59 | eqtr4d 2780 | . . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑓 ∈ (𝑋 ↑m (𝑋 × 𝑋))) → 𝑓 = (𝐻‘(𝑎 ∈ (𝑋 ↑m {0, 1}) ↦ ((𝑎‘0)𝑓(𝑎‘1))))) | 
| 61 | 6, 9, 60 | rspcedvd 3624 | . . 3
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑓 ∈ (𝑋 ↑m (𝑋 × 𝑋))) → ∃𝑔 ∈ (2-aryF 𝑋)𝑓 = (𝐻‘𝑔)) | 
| 62 | 61 | ralrimiva 3146 | . 2
⊢ (𝑋 ∈ 𝑉 → ∀𝑓 ∈ (𝑋 ↑m (𝑋 × 𝑋))∃𝑔 ∈ (2-aryF 𝑋)𝑓 = (𝐻‘𝑔)) | 
| 63 |  | dffo3 7122 | . 2
⊢ (𝐻:(2-aryF 𝑋)–onto→(𝑋 ↑m (𝑋 × 𝑋)) ↔ (𝐻:(2-aryF 𝑋)⟶(𝑋 ↑m (𝑋 × 𝑋)) ∧ ∀𝑓 ∈ (𝑋 ↑m (𝑋 × 𝑋))∃𝑔 ∈ (2-aryF 𝑋)𝑓 = (𝐻‘𝑔))) | 
| 64 | 2, 62, 63 | sylanbrc 583 | 1
⊢ (𝑋 ∈ 𝑉 → 𝐻:(2-aryF 𝑋)–onto→(𝑋 ↑m (𝑋 × 𝑋))) |