Step | Hyp | Ref
| Expression |
1 | | fsuppcurry2.g |
. . . 4
⢠šŗ = (š„ ā š“ ⦠(š„š¹š¶)) |
2 | | oveq1 7421 |
. . . . 5
⢠(š„ = š¦ ā (š„š¹š¶) = (š¦š¹š¶)) |
3 | 2 | cbvmptv 5255 |
. . . 4
⢠(š„ ā š“ ⦠(š„š¹š¶)) = (š¦ ā š“ ⦠(š¦š¹š¶)) |
4 | 1, 3 | eqtri 2755 |
. . 3
⢠šŗ = (š¦ ā š“ ⦠(š¦š¹š¶)) |
5 | | fsuppcurry2.a |
. . . 4
⢠(š ā š“ ā š) |
6 | 5 | mptexd 7230 |
. . 3
⢠(š ā (š¦ ā š“ ⦠(š¦š¹š¶)) ā V) |
7 | 4, 6 | eqeltrid 2832 |
. 2
⢠(š ā šŗ ā V) |
8 | 1 | funmpt2 6586 |
. . 3
⢠Fun šŗ |
9 | 8 | a1i 11 |
. 2
⢠(š ā Fun šŗ) |
10 | | fsuppcurry2.z |
. 2
⢠(š ā š ā š) |
11 | | fo1st 8005 |
. . . . 5
ā¢
1st :VāontoāV |
12 | | fofun 6806 |
. . . . 5
ā¢
(1st :VāontoāV ā Fun 1st ) |
13 | 11, 12 | ax-mp 5 |
. . . 4
⢠Fun
1st |
14 | | funres 6589 |
. . . 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 9383 |
. . 3
⢠(š ā (š¹ supp š) ā Fin) |
18 | | imafi 9189 |
. . 3
⢠((Fun
(1st ā¾ (V Ć V)) ā§ (š¹ supp š) ā Fin) ā ((1st
ā¾ (V Ć V)) ā (š¹ supp š)) ā Fin) |
19 | 15, 17, 18 | syl2anc 583 |
. 2
⢠(š ā ((1st ā¾
(V Ć V)) ā (š¹
supp š)) ā
Fin) |
20 | | ovexd 7449 |
. . . 4
⢠((š ā§ š¦ ā š“) ā (š¦š¹š¶) ā V) |
21 | 20, 4 | fmptd 7118 |
. . 3
⢠(š ā šŗ:š“ā¶V) |
22 | | eldif 3954 |
. . . 4
⢠(š¦ ā (š“ ā ((1st ā¾ (V Ć
V)) ā (š¹ supp š))) ā (š¦ ā š“ ⧠¬ š¦ ā ((1st ā¾ (V Ć
V)) ā (š¹ supp š)))) |
23 | | simplr 768 |
. . . . . . . . . . 11
⢠(((š ā§ š¦ ā š“) ⧠¬ (šŗāš¦) = š) ā š¦ ā š“) |
24 | | fsuppcurry2.c |
. . . . . . . . . . . 12
⢠(š ā š¶ ā šµ) |
25 | 24 | ad2antrr 725 |
. . . . . . . . . . 11
⢠(((š ā§ š¦ ā š“) ⧠¬ (šŗāš¦) = š) ā š¶ ā šµ) |
26 | 23, 25 | opelxpd 5711 |
. . . . . . . . . 10
⢠(((š ā§ š¦ ā š“) ⧠¬ (šŗāš¦) = š) ā āØš¦, š¶ā© ā (š“ Ć šµ)) |
27 | | df-ov 7417 |
. . . . . . . . . . 11
⢠(š¦š¹š¶) = (š¹āāØš¦, š¶ā©) |
28 | | ovexd 7449 |
. . . . . . . . . . . . 13
⢠(((š ā§ š¦ ā š“) ⧠¬ (šŗāš¦) = š) ā (š¦š¹š¶) ā V) |
29 | 1, 2, 23, 28 | fvmptd3 7022 |
. . . . . . . . . . . 12
⢠(((š ā§ š¦ ā š“) ⧠¬ (šŗāš¦) = š) ā (šŗāš¦) = (š¦š¹š¶)) |
30 | | simpr 484 |
. . . . . . . . . . . . 13
⢠(((š ā§ š¦ ā š“) ⧠¬ (šŗāš¦) = š) ā ¬ (šŗāš¦) = š) |
31 | 30 | neqned 2942 |
. . . . . . . . . . . 12
⢠(((š ā§ š¦ ā š“) ⧠¬ (šŗāš¦) = š) ā (šŗāš¦) ā š) |
32 | 29, 31 | eqnetrrd 3004 |
. . . . . . . . . . 11
⢠(((š ā§ š¦ ā š“) ⧠¬ (šŗāš¦) = š) ā (š¦š¹š¶) ā š) |
33 | 27, 32 | eqnetrrid 3011 |
. . . . . . . . . 10
⢠(((š ā§ š¦ ā š“) ⧠¬ (šŗāš¦) = š) ā (š¹āāØš¦, š¶ā©) ā š) |
34 | | fsuppcurry2.f |
. . . . . . . . . . . 12
⢠(š ā š¹ Fn (š“ Ć šµ)) |
35 | | fsuppcurry2.b |
. . . . . . . . . . . . 13
⢠(š ā šµ ā š) |
36 | 5, 35 | xpexd 7745 |
. . . . . . . . . . . 12
⢠(š ā (š“ Ć šµ) ā V) |
37 | | elsuppfn 8167 |
. . . . . . . . . . . 12
⢠((š¹ Fn (š“ Ć šµ) ā§ (š“ Ć šµ) ā V ā§ š ā š) ā (āØš¦, š¶ā© ā (š¹ supp š) ā (āØš¦, š¶ā© ā (š“ Ć šµ) ā§ (š¹āāØš¦, š¶ā©) ā š))) |
38 | 34, 36, 10, 37 | syl3anc 1369 |
. . . . . . . . . . 11
⢠(š ā (āØš¦, š¶ā© ā (š¹ supp š) ā (āØš¦, š¶ā© ā (š“ Ć šµ) ā§ (š¹āāØš¦, š¶ā©) ā š))) |
39 | 38 | ad2antrr 725 |
. . . . . . . . . 10
⢠(((š ā§ š¦ ā š“) ⧠¬ (šŗāš¦) = š) ā (āØš¦, š¶ā© ā (š¹ supp š) ā (āØš¦, š¶ā© ā (š“ Ć šµ) ā§ (š¹āāØš¦, š¶ā©) ā š))) |
40 | 26, 33, 39 | mpbir2and 712 |
. . . . . . . . 9
⢠(((š ā§ š¦ ā š“) ⧠¬ (šŗāš¦) = š) ā āØš¦, š¶ā© ā (š¹ supp š)) |
41 | | simpr 484 |
. . . . . . . . . . 11
⢠((((š ā§ š¦ ā š“) ⧠¬ (šŗāš¦) = š) ā§ š§ = āØš¦, š¶ā©) ā š§ = āØš¦, š¶ā©) |
42 | 41 | fveq2d 6895 |
. . . . . . . . . 10
⢠((((š ā§ š¦ ā š“) ⧠¬ (šŗāš¦) = š) ā§ š§ = āØš¦, š¶ā©) ā ((1st ā¾ (V
Ć V))āš§) =
((1st ā¾ (V Ć V))āāØš¦, š¶ā©)) |
43 | | xpss 5688 |
. . . . . . . . . . . 12
⢠(š“ Ć šµ) ā (V Ć V) |
44 | 26 | adantr 480 |
. . . . . . . . . . . 12
⢠((((š ā§ š¦ ā š“) ⧠¬ (šŗāš¦) = š) ā§ š§ = āØš¦, š¶ā©) ā āØš¦, š¶ā© ā (š“ Ć šµ)) |
45 | 43, 44 | sselid 3976 |
. . . . . . . . . . 11
⢠((((š ā§ š¦ ā š“) ⧠¬ (šŗāš¦) = š) ā§ š§ = āØš¦, š¶ā©) ā āØš¦, š¶ā© ā (V Ć
V)) |
46 | 45 | fvresd 6911 |
. . . . . . . . . 10
⢠((((š ā§ š¦ ā š“) ⧠¬ (šŗāš¦) = š) ā§ š§ = āØš¦, š¶ā©) ā ((1st ā¾ (V
Ć V))āāØš¦,
š¶ā©) = (1st
āāØš¦, š¶ā©)) |
47 | 23 | adantr 480 |
. . . . . . . . . . 11
⢠((((š ā§ š¦ ā š“) ⧠¬ (šŗāš¦) = š) ā§ š§ = āØš¦, š¶ā©) ā š¦ ā š“) |
48 | 25 | adantr 480 |
. . . . . . . . . . 11
⢠((((š ā§ š¦ ā š“) ⧠¬ (šŗāš¦) = š) ā§ š§ = āØš¦, š¶ā©) ā š¶ ā šµ) |
49 | | op1stg 7997 |
. . . . . . . . . . 11
⢠((š¦ ā š“ ā§ š¶ ā šµ) ā (1st āāØš¦, š¶ā©) = š¦) |
50 | 47, 48, 49 | syl2anc 583 |
. . . . . . . . . 10
⢠((((š ā§ š¦ ā š“) ⧠¬ (šŗāš¦) = š) ā§ š§ = āØš¦, š¶ā©) ā (1st
āāØš¦, š¶ā©) = š¦) |
51 | 42, 46, 50 | 3eqtrd 2771 |
. . . . . . . . 9
⢠((((š ā§ š¦ ā š“) ⧠¬ (šŗāš¦) = š) ā§ š§ = āØš¦, š¶ā©) ā ((1st ā¾ (V
Ć V))āš§) =
š¦) |
52 | 40, 51 | rspcedeq1vd 3614 |
. . . . . . . 8
⢠(((š ā§ š¦ ā š“) ⧠¬ (šŗāš¦) = š) ā āš§ ā (š¹ supp š)((1st ā¾ (V Ć
V))āš§) = š¦) |
53 | | fofn 6807 |
. . . . . . . . . . . . 13
ā¢
(1st :VāontoāV ā 1st Fn V) |
54 | | fnresin 32381 |
. . . . . . . . . . . . 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 4002 |
. . . . . . . . . . . . . 14
⢠(V
Ć V) ā V |
57 | | sseqin2 4211 |
. . . . . . . . . . . . . 14
⢠((V
Ć V) ā V ā (V ā© (V Ć V)) = (V Ć
V)) |
58 | 56, 57 | mpbi 229 |
. . . . . . . . . . . . 13
⢠(V ā©
(V Ć V)) = (V Ć V) |
59 | 58 | fneq2i 6646 |
. . . . . . . . . . . 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 8173 |
. . . . . . . . . . . 12
⢠(š¹ supp š) ā dom š¹ |
63 | 34 | fndmd 6653 |
. . . . . . . . . . . 12
⢠(š ā dom š¹ = (š“ Ć šµ)) |
64 | 62, 63 | sseqtrid 4030 |
. . . . . . . . . . 11
⢠(š ā (š¹ supp š) ā (š“ Ć šµ)) |
65 | 64, 43 | sstrdi 3990 |
. . . . . . . . . 10
⢠(š ā (š¹ supp š) ā (V Ć V)) |
66 | 61, 65 | fvelimabd 6966 |
. . . . . . . . 9
⢠(š ā (š¦ ā ((1st ā¾ (V Ć
V)) ā (š¹ supp š)) ā āš§ ā (š¹ supp š)((1st ā¾ (V Ć
V))āš§) = š¦)) |
67 | 66 | ad2antrr 725 |
. . . . . . . 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 593 |
. . 3
⢠((š ā§ š¦ ā (š“ ā ((1st ā¾ (V Ć
V)) ā (š¹ supp š)))) ā (šŗāš¦) = š) |
73 | 21, 72 | suppss 8190 |
. 2
⢠(š ā (šŗ supp š) ā ((1st ā¾ (V
Ć V)) ā (š¹ supp
š))) |
74 | | suppssfifsupp 9392 |
. 2
⢠(((šŗ ā V ā§ Fun šŗ ā§ š ā š) ā§ (((1st ā¾ (V Ć
V)) ā (š¹ supp š)) ā Fin ā§ (šŗ supp š) ā ((1st ā¾ (V
Ć V)) ā (š¹ supp
š)))) ā šŗ finSupp š) |
75 | 7, 9, 10, 19, 73, 74 | syl32anc 1376 |
1
⢠(š ā šŗ finSupp š) |