| Step | Hyp | Ref
| Expression |
| 1 | | fsuppcurry2.g |
. . . 4
⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝑥𝐹𝐶)) |
| 2 | | oveq1 7438 |
. . . . 5
⊢ (𝑥 = 𝑦 → (𝑥𝐹𝐶) = (𝑦𝐹𝐶)) |
| 3 | 2 | cbvmptv 5255 |
. . . 4
⊢ (𝑥 ∈ 𝐴 ↦ (𝑥𝐹𝐶)) = (𝑦 ∈ 𝐴 ↦ (𝑦𝐹𝐶)) |
| 4 | 1, 3 | eqtri 2765 |
. . 3
⊢ 𝐺 = (𝑦 ∈ 𝐴 ↦ (𝑦𝐹𝐶)) |
| 5 | | fsuppcurry2.a |
. . . 4
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
| 6 | 5 | mptexd 7244 |
. . 3
⊢ (𝜑 → (𝑦 ∈ 𝐴 ↦ (𝑦𝐹𝐶)) ∈ V) |
| 7 | 4, 6 | eqeltrid 2845 |
. 2
⊢ (𝜑 → 𝐺 ∈ V) |
| 8 | 1 | funmpt2 6605 |
. . 3
⊢ Fun 𝐺 |
| 9 | 8 | a1i 11 |
. 2
⊢ (𝜑 → Fun 𝐺) |
| 10 | | fsuppcurry2.z |
. 2
⊢ (𝜑 → 𝑍 ∈ 𝑈) |
| 11 | | fo1st 8034 |
. . . . 5
⊢
1st :V–onto→V |
| 12 | | fofun 6821 |
. . . . 5
⊢
(1st :V–onto→V → Fun 1st ) |
| 13 | 11, 12 | ax-mp 5 |
. . . 4
⊢ Fun
1st |
| 14 | | funres 6608 |
. . . 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 9409 |
. . 3
⊢ (𝜑 → (𝐹 supp 𝑍) ∈ Fin) |
| 18 | | imafi 9353 |
. . 3
⊢ ((Fun
(1st ↾ (V × V)) ∧ (𝐹 supp 𝑍) ∈ Fin) → ((1st
↾ (V × V)) “ (𝐹 supp 𝑍)) ∈ Fin) |
| 19 | 15, 17, 18 | syl2anc 584 |
. 2
⊢ (𝜑 → ((1st ↾
(V × V)) “ (𝐹
supp 𝑍)) ∈
Fin) |
| 20 | | ovexd 7466 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝑦𝐹𝐶) ∈ V) |
| 21 | 20, 4 | fmptd 7134 |
. . 3
⊢ (𝜑 → 𝐺:𝐴⟶V) |
| 22 | | eldif 3961 |
. . . 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 5724 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ (𝐺‘𝑦) = 𝑍) → 〈𝑦, 𝐶〉 ∈ (𝐴 × 𝐵)) |
| 27 | | df-ov 7434 |
. . . . . . . . . . 11
⊢ (𝑦𝐹𝐶) = (𝐹‘〈𝑦, 𝐶〉) |
| 28 | | ovexd 7466 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ (𝐺‘𝑦) = 𝑍) → (𝑦𝐹𝐶) ∈ V) |
| 29 | 1, 2, 23, 28 | fvmptd3 7039 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ (𝐺‘𝑦) = 𝑍) → (𝐺‘𝑦) = (𝑦𝐹𝐶)) |
| 30 | | simpr 484 |
. . . . . . . . . . . . 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 7771 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 × 𝐵) ∈ V) |
| 37 | | elsuppfn 8195 |
. . . . . . . . . . . 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 484 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ (𝐺‘𝑦) = 𝑍) ∧ 𝑧 = 〈𝑦, 𝐶〉) → 𝑧 = 〈𝑦, 𝐶〉) |
| 42 | 41 | fveq2d 6910 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ (𝐺‘𝑦) = 𝑍) ∧ 𝑧 = 〈𝑦, 𝐶〉) → ((1st ↾ (V
× V))‘𝑧) =
((1st ↾ (V × V))‘〈𝑦, 𝐶〉)) |
| 43 | | xpss 5701 |
. . . . . . . . . . . 12
⊢ (𝐴 × 𝐵) ⊆ (V × V) |
| 44 | 26 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ (𝐺‘𝑦) = 𝑍) ∧ 𝑧 = 〈𝑦, 𝐶〉) → 〈𝑦, 𝐶〉 ∈ (𝐴 × 𝐵)) |
| 45 | 43, 44 | sselid 3981 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ (𝐺‘𝑦) = 𝑍) ∧ 𝑧 = 〈𝑦, 𝐶〉) → 〈𝑦, 𝐶〉 ∈ (V ×
V)) |
| 46 | 45 | fvresd 6926 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ (𝐺‘𝑦) = 𝑍) ∧ 𝑧 = 〈𝑦, 𝐶〉) → ((1st ↾ (V
× V))‘〈𝑦,
𝐶〉) = (1st
‘〈𝑦, 𝐶〉)) |
| 47 | 23 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ (𝐺‘𝑦) = 𝑍) ∧ 𝑧 = 〈𝑦, 𝐶〉) → 𝑦 ∈ 𝐴) |
| 48 | 25 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ (𝐺‘𝑦) = 𝑍) ∧ 𝑧 = 〈𝑦, 𝐶〉) → 𝐶 ∈ 𝐵) |
| 49 | | op1stg 8026 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ 𝐴 ∧ 𝐶 ∈ 𝐵) → (1st ‘〈𝑦, 𝐶〉) = 𝑦) |
| 50 | 47, 48, 49 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ (𝐺‘𝑦) = 𝑍) ∧ 𝑧 = 〈𝑦, 𝐶〉) → (1st
‘〈𝑦, 𝐶〉) = 𝑦) |
| 51 | 42, 46, 50 | 3eqtrd 2781 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ (𝐺‘𝑦) = 𝑍) ∧ 𝑧 = 〈𝑦, 𝐶〉) → ((1st ↾ (V
× V))‘𝑧) =
𝑦) |
| 52 | 40, 51 | rspcedeq1vd 3629 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ (𝐺‘𝑦) = 𝑍) → ∃𝑧 ∈ (𝐹 supp 𝑍)((1st ↾ (V ×
V))‘𝑧) = 𝑦) |
| 53 | | fofn 6822 |
. . . . . . . . . . . . 13
⊢
(1st :V–onto→V → 1st Fn V) |
| 54 | | fnresin 32636 |
. . . . . . . . . . . . 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 4008 |
. . . . . . . . . . . . . 14
⊢ (V
× V) ⊆ V |
| 57 | | sseqin2 4223 |
. . . . . . . . . . . . . 14
⊢ ((V
× V) ⊆ V ↔ (V ∩ (V × V)) = (V ×
V)) |
| 58 | 56, 57 | mpbi 230 |
. . . . . . . . . . . . 13
⊢ (V ∩
(V × V)) = (V × V) |
| 59 | 58 | fneq2i 6666 |
. . . . . . . . . . . 12
⊢
((1st ↾ (V × V)) Fn (V ∩ (V × V))
↔ (1st ↾ (V × V)) Fn (V ×
V)) |
| 60 | 55, 59 | mpbi 230 |
. . . . . . . . . . 11
⊢
(1st ↾ (V × V)) Fn (V × V) |
| 61 | 60 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → (1st ↾ (V
× V)) Fn (V × V)) |
| 62 | | suppssdm 8202 |
. . . . . . . . . . . 12
⊢ (𝐹 supp 𝑍) ⊆ dom 𝐹 |
| 63 | 34 | fndmd 6673 |
. . . . . . . . . . . 12
⊢ (𝜑 → dom 𝐹 = (𝐴 × 𝐵)) |
| 64 | 62, 63 | sseqtrid 4026 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐹 supp 𝑍) ⊆ (𝐴 × 𝐵)) |
| 65 | 64, 43 | sstrdi 3996 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹 supp 𝑍) ⊆ (V × V)) |
| 66 | 61, 65 | fvelimabd 6982 |
. . . . . . . . 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 257 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ (𝐺‘𝑦) = 𝑍) → 𝑦 ∈ ((1st ↾ (V ×
V)) “ (𝐹 supp 𝑍))) |
| 69 | 68 | ex 412 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (¬ (𝐺‘𝑦) = 𝑍 → 𝑦 ∈ ((1st ↾ (V ×
V)) “ (𝐹 supp 𝑍)))) |
| 70 | 69 | con1d 145 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (¬ 𝑦 ∈ ((1st ↾ (V ×
V)) “ (𝐹 supp 𝑍)) → (𝐺‘𝑦) = 𝑍)) |
| 71 | 70 | impr 454 |
. . . 4
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ ((1st ↾ (V ×
V)) “ (𝐹 supp 𝑍)))) → (𝐺‘𝑦) = 𝑍) |
| 72 | 22, 71 | sylan2b 594 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ ((1st ↾ (V ×
V)) “ (𝐹 supp 𝑍)))) → (𝐺‘𝑦) = 𝑍) |
| 73 | 21, 72 | suppss 8219 |
. 2
⊢ (𝜑 → (𝐺 supp 𝑍) ⊆ ((1st ↾ (V
× V)) “ (𝐹 supp
𝑍))) |
| 74 | | suppssfifsupp 9420 |
. 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 𝑍) |