Step | Hyp | Ref
| Expression |
1 | | fsuppcurry2.g |
. . . 4
⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝑥𝐹𝐶)) |
2 | | oveq1 7349 |
. . . . 5
⊢ (𝑥 = 𝑦 → (𝑥𝐹𝐶) = (𝑦𝐹𝐶)) |
3 | 2 | cbvmptv 5210 |
. . . 4
⊢ (𝑥 ∈ 𝐴 ↦ (𝑥𝐹𝐶)) = (𝑦 ∈ 𝐴 ↦ (𝑦𝐹𝐶)) |
4 | 1, 3 | eqtri 2765 |
. . 3
⊢ 𝐺 = (𝑦 ∈ 𝐴 ↦ (𝑦𝐹𝐶)) |
5 | | fsuppcurry2.a |
. . . 4
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
6 | 5 | mptexd 7161 |
. . 3
⊢ (𝜑 → (𝑦 ∈ 𝐴 ↦ (𝑦𝐹𝐶)) ∈ V) |
7 | 4, 6 | eqeltrid 2842 |
. 2
⊢ (𝜑 → 𝐺 ∈ V) |
8 | 1 | funmpt2 6528 |
. . 3
⊢ Fun 𝐺 |
9 | 8 | a1i 11 |
. 2
⊢ (𝜑 → Fun 𝐺) |
10 | | fsuppcurry2.z |
. 2
⊢ (𝜑 → 𝑍 ∈ 𝑈) |
11 | | fo1st 7924 |
. . . . 5
⊢
1st :V–onto→V |
12 | | fofun 6745 |
. . . . 5
⊢
(1st :V–onto→V → Fun 1st ) |
13 | 11, 12 | ax-mp 5 |
. . . 4
⊢ Fun
1st |
14 | | funres 6531 |
. . . 4
⊢ (Fun
1st → Fun (1st ↾ (V ×
V))) |
15 | 13, 14 | mp1i 13 |
. . 3
⊢ (𝜑 → Fun (1st
↾ (V × V))) |
16 | | fsuppcurry2.1 |
. . . 4
⊢ (𝜑 → 𝐹 finSupp 𝑍) |
17 | 16 | fsuppimpd 9238 |
. . 3
⊢ (𝜑 → (𝐹 supp 𝑍) ∈ Fin) |
18 | | imafi 9045 |
. . 3
⊢ ((Fun
(1st ↾ (V × V)) ∧ (𝐹 supp 𝑍) ∈ Fin) → ((1st
↾ (V × V)) “ (𝐹 supp 𝑍)) ∈ Fin) |
19 | 15, 17, 18 | syl2anc 585 |
. 2
⊢ (𝜑 → ((1st ↾
(V × V)) “ (𝐹
supp 𝑍)) ∈
Fin) |
20 | | ovexd 7377 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝑦𝐹𝐶) ∈ V) |
21 | 20, 4 | fmptd 7049 |
. . 3
⊢ (𝜑 → 𝐺:𝐴⟶V) |
22 | | eldif 3912 |
. . . 4
⊢ (𝑦 ∈ (𝐴 ∖ ((1st ↾ (V ×
V)) “ (𝐹 supp 𝑍))) ↔ (𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ ((1st ↾ (V ×
V)) “ (𝐹 supp 𝑍)))) |
23 | | simplr 767 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ (𝐺‘𝑦) = 𝑍) → 𝑦 ∈ 𝐴) |
24 | | fsuppcurry2.c |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐶 ∈ 𝐵) |
25 | 24 | ad2antrr 724 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ (𝐺‘𝑦) = 𝑍) → 𝐶 ∈ 𝐵) |
26 | 23, 25 | opelxpd 5663 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ (𝐺‘𝑦) = 𝑍) → 〈𝑦, 𝐶〉 ∈ (𝐴 × 𝐵)) |
27 | | df-ov 7345 |
. . . . . . . . . . 11
⊢ (𝑦𝐹𝐶) = (𝐹‘〈𝑦, 𝐶〉) |
28 | | ovexd 7377 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ (𝐺‘𝑦) = 𝑍) → (𝑦𝐹𝐶) ∈ V) |
29 | 1, 2, 23, 28 | fvmptd3 6959 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ (𝐺‘𝑦) = 𝑍) → (𝐺‘𝑦) = (𝑦𝐹𝐶)) |
30 | | simpr 486 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ (𝐺‘𝑦) = 𝑍) → ¬ (𝐺‘𝑦) = 𝑍) |
31 | 30 | neqned 2948 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ (𝐺‘𝑦) = 𝑍) → (𝐺‘𝑦) ≠ 𝑍) |
32 | 29, 31 | eqnetrrd 3010 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ (𝐺‘𝑦) = 𝑍) → (𝑦𝐹𝐶) ≠ 𝑍) |
33 | 27, 32 | eqnetrrid 3017 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ (𝐺‘𝑦) = 𝑍) → (𝐹‘〈𝑦, 𝐶〉) ≠ 𝑍) |
34 | | fsuppcurry2.f |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹 Fn (𝐴 × 𝐵)) |
35 | | fsuppcurry2.b |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐵 ∈ 𝑊) |
36 | 5, 35 | xpexd 7668 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 × 𝐵) ∈ V) |
37 | | elsuppfn 8062 |
. . . . . . . . . . . 12
⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ (𝐴 × 𝐵) ∈ V ∧ 𝑍 ∈ 𝑈) → (〈𝑦, 𝐶〉 ∈ (𝐹 supp 𝑍) ↔ (〈𝑦, 𝐶〉 ∈ (𝐴 × 𝐵) ∧ (𝐹‘〈𝑦, 𝐶〉) ≠ 𝑍))) |
38 | 34, 36, 10, 37 | syl3anc 1371 |
. . . . . . . . . . 11
⊢ (𝜑 → (〈𝑦, 𝐶〉 ∈ (𝐹 supp 𝑍) ↔ (〈𝑦, 𝐶〉 ∈ (𝐴 × 𝐵) ∧ (𝐹‘〈𝑦, 𝐶〉) ≠ 𝑍))) |
39 | 38 | ad2antrr 724 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ (𝐺‘𝑦) = 𝑍) → (〈𝑦, 𝐶〉 ∈ (𝐹 supp 𝑍) ↔ (〈𝑦, 𝐶〉 ∈ (𝐴 × 𝐵) ∧ (𝐹‘〈𝑦, 𝐶〉) ≠ 𝑍))) |
40 | 26, 33, 39 | mpbir2and 711 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ (𝐺‘𝑦) = 𝑍) → 〈𝑦, 𝐶〉 ∈ (𝐹 supp 𝑍)) |
41 | | simpr 486 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ (𝐺‘𝑦) = 𝑍) ∧ 𝑧 = 〈𝑦, 𝐶〉) → 𝑧 = 〈𝑦, 𝐶〉) |
42 | 41 | fveq2d 6834 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ (𝐺‘𝑦) = 𝑍) ∧ 𝑧 = 〈𝑦, 𝐶〉) → ((1st ↾ (V
× V))‘𝑧) =
((1st ↾ (V × V))‘〈𝑦, 𝐶〉)) |
43 | | xpss 5641 |
. . . . . . . . . . . 12
⊢ (𝐴 × 𝐵) ⊆ (V × V) |
44 | 26 | adantr 482 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ (𝐺‘𝑦) = 𝑍) ∧ 𝑧 = 〈𝑦, 𝐶〉) → 〈𝑦, 𝐶〉 ∈ (𝐴 × 𝐵)) |
45 | 43, 44 | sselid 3934 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ (𝐺‘𝑦) = 𝑍) ∧ 𝑧 = 〈𝑦, 𝐶〉) → 〈𝑦, 𝐶〉 ∈ (V ×
V)) |
46 | 45 | fvresd 6850 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ (𝐺‘𝑦) = 𝑍) ∧ 𝑧 = 〈𝑦, 𝐶〉) → ((1st ↾ (V
× V))‘〈𝑦,
𝐶〉) = (1st
‘〈𝑦, 𝐶〉)) |
47 | 23 | adantr 482 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ (𝐺‘𝑦) = 𝑍) ∧ 𝑧 = 〈𝑦, 𝐶〉) → 𝑦 ∈ 𝐴) |
48 | 25 | adantr 482 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ (𝐺‘𝑦) = 𝑍) ∧ 𝑧 = 〈𝑦, 𝐶〉) → 𝐶 ∈ 𝐵) |
49 | | op1stg 7916 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ 𝐴 ∧ 𝐶 ∈ 𝐵) → (1st ‘〈𝑦, 𝐶〉) = 𝑦) |
50 | 47, 48, 49 | syl2anc 585 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ (𝐺‘𝑦) = 𝑍) ∧ 𝑧 = 〈𝑦, 𝐶〉) → (1st
‘〈𝑦, 𝐶〉) = 𝑦) |
51 | 42, 46, 50 | 3eqtrd 2781 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ (𝐺‘𝑦) = 𝑍) ∧ 𝑧 = 〈𝑦, 𝐶〉) → ((1st ↾ (V
× V))‘𝑧) =
𝑦) |
52 | 40, 51 | rspcedeq1vd 3579 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ (𝐺‘𝑦) = 𝑍) → ∃𝑧 ∈ (𝐹 supp 𝑍)((1st ↾ (V ×
V))‘𝑧) = 𝑦) |
53 | | fofn 6746 |
. . . . . . . . . . . . 13
⊢
(1st :V–onto→V → 1st Fn V) |
54 | | fnresin 31246 |
. . . . . . . . . . . . 13
⊢
(1st Fn V → (1st ↾ (V × V)) Fn (V
∩ (V × V))) |
55 | 11, 53, 54 | mp2b 10 |
. . . . . . . . . . . 12
⊢
(1st ↾ (V × V)) Fn (V ∩ (V ×
V)) |
56 | | ssv 3960 |
. . . . . . . . . . . . . 14
⊢ (V
× V) ⊆ V |
57 | | sseqin2 4167 |
. . . . . . . . . . . . . 14
⊢ ((V
× V) ⊆ V ↔ (V ∩ (V × V)) = (V ×
V)) |
58 | 56, 57 | mpbi 229 |
. . . . . . . . . . . . 13
⊢ (V ∩
(V × V)) = (V × V) |
59 | 58 | fneq2i 6588 |
. . . . . . . . . . . 12
⊢
((1st ↾ (V × V)) Fn (V ∩ (V × V))
↔ (1st ↾ (V × V)) Fn (V ×
V)) |
60 | 55, 59 | mpbi 229 |
. . . . . . . . . . 11
⊢
(1st ↾ (V × V)) Fn (V × V) |
61 | 60 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → (1st ↾ (V
× V)) Fn (V × V)) |
62 | | suppssdm 8068 |
. . . . . . . . . . . 12
⊢ (𝐹 supp 𝑍) ⊆ dom 𝐹 |
63 | 34 | fndmd 6595 |
. . . . . . . . . . . 12
⊢ (𝜑 → dom 𝐹 = (𝐴 × 𝐵)) |
64 | 62, 63 | sseqtrid 3988 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐹 supp 𝑍) ⊆ (𝐴 × 𝐵)) |
65 | 64, 43 | sstrdi 3948 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹 supp 𝑍) ⊆ (V × V)) |
66 | 61, 65 | fvelimabd 6903 |
. . . . . . . . 9
⊢ (𝜑 → (𝑦 ∈ ((1st ↾ (V ×
V)) “ (𝐹 supp 𝑍)) ↔ ∃𝑧 ∈ (𝐹 supp 𝑍)((1st ↾ (V ×
V))‘𝑧) = 𝑦)) |
67 | 66 | ad2antrr 724 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ (𝐺‘𝑦) = 𝑍) → (𝑦 ∈ ((1st ↾ (V ×
V)) “ (𝐹 supp 𝑍)) ↔ ∃𝑧 ∈ (𝐹 supp 𝑍)((1st ↾ (V ×
V))‘𝑧) = 𝑦)) |
68 | 52, 67 | mpbird 257 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ (𝐺‘𝑦) = 𝑍) → 𝑦 ∈ ((1st ↾ (V ×
V)) “ (𝐹 supp 𝑍))) |
69 | 68 | ex 414 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (¬ (𝐺‘𝑦) = 𝑍 → 𝑦 ∈ ((1st ↾ (V ×
V)) “ (𝐹 supp 𝑍)))) |
70 | 69 | con1d 145 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (¬ 𝑦 ∈ ((1st ↾ (V ×
V)) “ (𝐹 supp 𝑍)) → (𝐺‘𝑦) = 𝑍)) |
71 | 70 | impr 456 |
. . . 4
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ ((1st ↾ (V ×
V)) “ (𝐹 supp 𝑍)))) → (𝐺‘𝑦) = 𝑍) |
72 | 22, 71 | sylan2b 595 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ ((1st ↾ (V ×
V)) “ (𝐹 supp 𝑍)))) → (𝐺‘𝑦) = 𝑍) |
73 | 21, 72 | suppss 8085 |
. 2
⊢ (𝜑 → (𝐺 supp 𝑍) ⊆ ((1st ↾ (V
× V)) “ (𝐹 supp
𝑍))) |
74 | | suppssfifsupp 9246 |
. 2
⊢ (((𝐺 ∈ V ∧ Fun 𝐺 ∧ 𝑍 ∈ 𝑈) ∧ (((1st ↾ (V ×
V)) “ (𝐹 supp 𝑍)) ∈ Fin ∧ (𝐺 supp 𝑍) ⊆ ((1st ↾ (V
× V)) “ (𝐹 supp
𝑍)))) → 𝐺 finSupp 𝑍) |
75 | 7, 9, 10, 19, 73, 74 | syl32anc 1378 |
1
⊢ (𝜑 → 𝐺 finSupp 𝑍) |