Step | Hyp | Ref
| Expression |
1 | | fsuppcurry2.g |
. . . 4
⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝑥𝐹𝐶)) |
2 | | oveq1 7220 |
. . . . 5
⊢ (𝑥 = 𝑦 → (𝑥𝐹𝐶) = (𝑦𝐹𝐶)) |
3 | 2 | cbvmptv 5158 |
. . . 4
⊢ (𝑥 ∈ 𝐴 ↦ (𝑥𝐹𝐶)) = (𝑦 ∈ 𝐴 ↦ (𝑦𝐹𝐶)) |
4 | 1, 3 | eqtri 2765 |
. . 3
⊢ 𝐺 = (𝑦 ∈ 𝐴 ↦ (𝑦𝐹𝐶)) |
5 | | fsuppcurry2.a |
. . . 4
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
6 | 5 | mptexd 7040 |
. . 3
⊢ (𝜑 → (𝑦 ∈ 𝐴 ↦ (𝑦𝐹𝐶)) ∈ V) |
7 | 4, 6 | eqeltrid 2842 |
. 2
⊢ (𝜑 → 𝐺 ∈ V) |
8 | 1 | funmpt2 6419 |
. . 3
⊢ Fun 𝐺 |
9 | 8 | a1i 11 |
. 2
⊢ (𝜑 → Fun 𝐺) |
10 | | fsuppcurry2.z |
. 2
⊢ (𝜑 → 𝑍 ∈ 𝑈) |
11 | | fo1st 7781 |
. . . . 5
⊢
1st :V–onto→V |
12 | | fofun 6634 |
. . . . 5
⊢
(1st :V–onto→V → Fun 1st ) |
13 | 11, 12 | ax-mp 5 |
. . . 4
⊢ Fun
1st |
14 | | funres 6422 |
. . . 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 8992 |
. . 3
⊢ (𝜑 → (𝐹 supp 𝑍) ∈ Fin) |
18 | | imafi 8853 |
. . 3
⊢ ((Fun
(1st ↾ (V × V)) ∧ (𝐹 supp 𝑍) ∈ Fin) → ((1st
↾ (V × V)) “ (𝐹 supp 𝑍)) ∈ Fin) |
19 | 15, 17, 18 | syl2anc 587 |
. 2
⊢ (𝜑 → ((1st ↾
(V × V)) “ (𝐹
supp 𝑍)) ∈
Fin) |
20 | | ovexd 7248 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝑦𝐹𝐶) ∈ V) |
21 | 20, 4 | fmptd 6931 |
. . 3
⊢ (𝜑 → 𝐺:𝐴⟶V) |
22 | | eldif 3876 |
. . . 4
⊢ (𝑦 ∈ (𝐴 ∖ ((1st ↾ (V ×
V)) “ (𝐹 supp 𝑍))) ↔ (𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ ((1st ↾ (V ×
V)) “ (𝐹 supp 𝑍)))) |
23 | | simplr 769 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ (𝐺‘𝑦) = 𝑍) → 𝑦 ∈ 𝐴) |
24 | | fsuppcurry2.c |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐶 ∈ 𝐵) |
25 | 24 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ (𝐺‘𝑦) = 𝑍) → 𝐶 ∈ 𝐵) |
26 | 23, 25 | opelxpd 5589 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ (𝐺‘𝑦) = 𝑍) → 〈𝑦, 𝐶〉 ∈ (𝐴 × 𝐵)) |
27 | | df-ov 7216 |
. . . . . . . . . . 11
⊢ (𝑦𝐹𝐶) = (𝐹‘〈𝑦, 𝐶〉) |
28 | | ovexd 7248 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ (𝐺‘𝑦) = 𝑍) → (𝑦𝐹𝐶) ∈ V) |
29 | 1, 2, 23, 28 | fvmptd3 6841 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ (𝐺‘𝑦) = 𝑍) → (𝐺‘𝑦) = (𝑦𝐹𝐶)) |
30 | | simpr 488 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ (𝐺‘𝑦) = 𝑍) → ¬ (𝐺‘𝑦) = 𝑍) |
31 | 30 | neqned 2947 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ (𝐺‘𝑦) = 𝑍) → (𝐺‘𝑦) ≠ 𝑍) |
32 | 29, 31 | eqnetrrd 3009 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ (𝐺‘𝑦) = 𝑍) → (𝑦𝐹𝐶) ≠ 𝑍) |
33 | 27, 32 | eqnetrrid 3016 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ (𝐺‘𝑦) = 𝑍) → (𝐹‘〈𝑦, 𝐶〉) ≠ 𝑍) |
34 | | fsuppcurry2.f |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹 Fn (𝐴 × 𝐵)) |
35 | | fsuppcurry2.b |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐵 ∈ 𝑊) |
36 | 5, 35 | xpexd 7536 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 × 𝐵) ∈ V) |
37 | | elsuppfn 7913 |
. . . . . . . . . . . 12
⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ (𝐴 × 𝐵) ∈ V ∧ 𝑍 ∈ 𝑈) → (〈𝑦, 𝐶〉 ∈ (𝐹 supp 𝑍) ↔ (〈𝑦, 𝐶〉 ∈ (𝐴 × 𝐵) ∧ (𝐹‘〈𝑦, 𝐶〉) ≠ 𝑍))) |
38 | 34, 36, 10, 37 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ (𝜑 → (〈𝑦, 𝐶〉 ∈ (𝐹 supp 𝑍) ↔ (〈𝑦, 𝐶〉 ∈ (𝐴 × 𝐵) ∧ (𝐹‘〈𝑦, 𝐶〉) ≠ 𝑍))) |
39 | 38 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ (𝐺‘𝑦) = 𝑍) → (〈𝑦, 𝐶〉 ∈ (𝐹 supp 𝑍) ↔ (〈𝑦, 𝐶〉 ∈ (𝐴 × 𝐵) ∧ (𝐹‘〈𝑦, 𝐶〉) ≠ 𝑍))) |
40 | 26, 33, 39 | mpbir2and 713 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ (𝐺‘𝑦) = 𝑍) → 〈𝑦, 𝐶〉 ∈ (𝐹 supp 𝑍)) |
41 | | simpr 488 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ (𝐺‘𝑦) = 𝑍) ∧ 𝑧 = 〈𝑦, 𝐶〉) → 𝑧 = 〈𝑦, 𝐶〉) |
42 | 41 | fveq2d 6721 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ (𝐺‘𝑦) = 𝑍) ∧ 𝑧 = 〈𝑦, 𝐶〉) → ((1st ↾ (V
× V))‘𝑧) =
((1st ↾ (V × V))‘〈𝑦, 𝐶〉)) |
43 | | xpss 5567 |
. . . . . . . . . . . 12
⊢ (𝐴 × 𝐵) ⊆ (V × V) |
44 | 26 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ (𝐺‘𝑦) = 𝑍) ∧ 𝑧 = 〈𝑦, 𝐶〉) → 〈𝑦, 𝐶〉 ∈ (𝐴 × 𝐵)) |
45 | 43, 44 | sseldi 3899 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ (𝐺‘𝑦) = 𝑍) ∧ 𝑧 = 〈𝑦, 𝐶〉) → 〈𝑦, 𝐶〉 ∈ (V ×
V)) |
46 | 45 | fvresd 6737 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ (𝐺‘𝑦) = 𝑍) ∧ 𝑧 = 〈𝑦, 𝐶〉) → ((1st ↾ (V
× V))‘〈𝑦,
𝐶〉) = (1st
‘〈𝑦, 𝐶〉)) |
47 | 23 | adantr 484 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ (𝐺‘𝑦) = 𝑍) ∧ 𝑧 = 〈𝑦, 𝐶〉) → 𝑦 ∈ 𝐴) |
48 | 25 | adantr 484 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ (𝐺‘𝑦) = 𝑍) ∧ 𝑧 = 〈𝑦, 𝐶〉) → 𝐶 ∈ 𝐵) |
49 | | op1stg 7773 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ 𝐴 ∧ 𝐶 ∈ 𝐵) → (1st ‘〈𝑦, 𝐶〉) = 𝑦) |
50 | 47, 48, 49 | syl2anc 587 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ (𝐺‘𝑦) = 𝑍) ∧ 𝑧 = 〈𝑦, 𝐶〉) → (1st
‘〈𝑦, 𝐶〉) = 𝑦) |
51 | 42, 46, 50 | 3eqtrd 2781 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ (𝐺‘𝑦) = 𝑍) ∧ 𝑧 = 〈𝑦, 𝐶〉) → ((1st ↾ (V
× V))‘𝑧) =
𝑦) |
52 | 40, 51 | rspcedeq1vd 3543 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ (𝐺‘𝑦) = 𝑍) → ∃𝑧 ∈ (𝐹 supp 𝑍)((1st ↾ (V ×
V))‘𝑧) = 𝑦) |
53 | | fofn 6635 |
. . . . . . . . . . . . 13
⊢
(1st :V–onto→V → 1st Fn V) |
54 | | fnresin 30680 |
. . . . . . . . . . . . 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 3925 |
. . . . . . . . . . . . . 14
⊢ (V
× V) ⊆ V |
57 | | sseqin2 4130 |
. . . . . . . . . . . . . 14
⊢ ((V
× V) ⊆ V ↔ (V ∩ (V × V)) = (V ×
V)) |
58 | 56, 57 | mpbi 233 |
. . . . . . . . . . . . 13
⊢ (V ∩
(V × V)) = (V × V) |
59 | 58 | fneq2i 6477 |
. . . . . . . . . . . 12
⊢
((1st ↾ (V × V)) Fn (V ∩ (V × V))
↔ (1st ↾ (V × V)) Fn (V ×
V)) |
60 | 55, 59 | mpbi 233 |
. . . . . . . . . . 11
⊢
(1st ↾ (V × V)) Fn (V × V) |
61 | 60 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → (1st ↾ (V
× V)) Fn (V × V)) |
62 | | suppssdm 7919 |
. . . . . . . . . . . 12
⊢ (𝐹 supp 𝑍) ⊆ dom 𝐹 |
63 | 34 | fndmd 6483 |
. . . . . . . . . . . 12
⊢ (𝜑 → dom 𝐹 = (𝐴 × 𝐵)) |
64 | 62, 63 | sseqtrid 3953 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐹 supp 𝑍) ⊆ (𝐴 × 𝐵)) |
65 | 64, 43 | sstrdi 3913 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹 supp 𝑍) ⊆ (V × V)) |
66 | 61, 65 | fvelimabd 6785 |
. . . . . . . . 9
⊢ (𝜑 → (𝑦 ∈ ((1st ↾ (V ×
V)) “ (𝐹 supp 𝑍)) ↔ ∃𝑧 ∈ (𝐹 supp 𝑍)((1st ↾ (V ×
V))‘𝑧) = 𝑦)) |
67 | 66 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ (𝐺‘𝑦) = 𝑍) → (𝑦 ∈ ((1st ↾ (V ×
V)) “ (𝐹 supp 𝑍)) ↔ ∃𝑧 ∈ (𝐹 supp 𝑍)((1st ↾ (V ×
V))‘𝑧) = 𝑦)) |
68 | 52, 67 | mpbird 260 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ (𝐺‘𝑦) = 𝑍) → 𝑦 ∈ ((1st ↾ (V ×
V)) “ (𝐹 supp 𝑍))) |
69 | 68 | ex 416 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (¬ (𝐺‘𝑦) = 𝑍 → 𝑦 ∈ ((1st ↾ (V ×
V)) “ (𝐹 supp 𝑍)))) |
70 | 69 | con1d 147 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (¬ 𝑦 ∈ ((1st ↾ (V ×
V)) “ (𝐹 supp 𝑍)) → (𝐺‘𝑦) = 𝑍)) |
71 | 70 | impr 458 |
. . . 4
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ ((1st ↾ (V ×
V)) “ (𝐹 supp 𝑍)))) → (𝐺‘𝑦) = 𝑍) |
72 | 22, 71 | sylan2b 597 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ ((1st ↾ (V ×
V)) “ (𝐹 supp 𝑍)))) → (𝐺‘𝑦) = 𝑍) |
73 | 21, 72 | suppss 7936 |
. 2
⊢ (𝜑 → (𝐺 supp 𝑍) ⊆ ((1st ↾ (V
× V)) “ (𝐹 supp
𝑍))) |
74 | | suppssfifsupp 9000 |
. 2
⊢ (((𝐺 ∈ V ∧ Fun 𝐺 ∧ 𝑍 ∈ 𝑈) ∧ (((1st ↾ (V ×
V)) “ (𝐹 supp 𝑍)) ∈ Fin ∧ (𝐺 supp 𝑍) ⊆ ((1st ↾ (V
× V)) “ (𝐹 supp
𝑍)))) → 𝐺 finSupp 𝑍) |
75 | 7, 9, 10, 19, 73, 74 | syl32anc 1380 |
1
⊢ (𝜑 → 𝐺 finSupp 𝑍) |