Step | Hyp | Ref
| Expression |
1 | | fsuppcurry2.g |
. . . 4
ā¢ šŗ = (š„ ā š“ ā¦ (š„š¹š¶)) |
2 | | oveq1 7365 |
. . . . 5
ā¢ (š„ = š¦ ā (š„š¹š¶) = (š¦š¹š¶)) |
3 | 2 | cbvmptv 5219 |
. . . 4
ā¢ (š„ ā š“ ā¦ (š„š¹š¶)) = (š¦ ā š“ ā¦ (š¦š¹š¶)) |
4 | 1, 3 | eqtri 2761 |
. . 3
ā¢ šŗ = (š¦ ā š“ ā¦ (š¦š¹š¶)) |
5 | | fsuppcurry2.a |
. . . 4
ā¢ (š ā š“ ā š) |
6 | 5 | mptexd 7175 |
. . 3
ā¢ (š ā (š¦ ā š“ ā¦ (š¦š¹š¶)) ā V) |
7 | 4, 6 | eqeltrid 2838 |
. 2
ā¢ (š ā šŗ ā V) |
8 | 1 | funmpt2 6541 |
. . 3
ā¢ Fun šŗ |
9 | 8 | a1i 11 |
. 2
ā¢ (š ā Fun šŗ) |
10 | | fsuppcurry2.z |
. 2
ā¢ (š ā š ā š) |
11 | | fo1st 7942 |
. . . . 5
ā¢
1st :VāontoāV |
12 | | fofun 6758 |
. . . . 5
ā¢
(1st :VāontoāV ā Fun 1st ) |
13 | 11, 12 | ax-mp 5 |
. . . 4
ā¢ Fun
1st |
14 | | funres 6544 |
. . . 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 9316 |
. . 3
ā¢ (š ā (š¹ supp š) ā Fin) |
18 | | imafi 9122 |
. . 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 7393 |
. . . 4
ā¢ ((š ā§ š¦ ā š“) ā (š¦š¹š¶) ā V) |
21 | 20, 4 | fmptd 7063 |
. . 3
ā¢ (š ā šŗ:š“ā¶V) |
22 | | eldif 3921 |
. . . 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 5672 |
. . . . . . . . . 10
ā¢ (((š ā§ š¦ ā š“) ā§ Ā¬ (šŗāš¦) = š) ā āØš¦, š¶ā© ā (š“ Ć šµ)) |
27 | | df-ov 7361 |
. . . . . . . . . . 11
ā¢ (š¦š¹š¶) = (š¹āāØš¦, š¶ā©) |
28 | | ovexd 7393 |
. . . . . . . . . . . . 13
ā¢ (((š ā§ š¦ ā š“) ā§ Ā¬ (šŗāš¦) = š) ā (š¦š¹š¶) ā V) |
29 | 1, 2, 23, 28 | fvmptd3 6972 |
. . . . . . . . . . . 12
ā¢ (((š ā§ š¦ ā š“) ā§ Ā¬ (šŗāš¦) = š) ā (šŗāš¦) = (š¦š¹š¶)) |
30 | | simpr 486 |
. . . . . . . . . . . . 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 7686 |
. . . . . . . . . . . 12
ā¢ (š ā (š“ Ć šµ) ā V) |
37 | | elsuppfn 8103 |
. . . . . . . . . . . 12
ā¢ ((š¹ Fn (š“ Ć šµ) ā§ (š“ Ć šµ) ā V ā§ š ā š) ā (āØš¦, š¶ā© ā (š¹ supp š) ā (āØš¦, š¶ā© ā (š“ Ć šµ) ā§ (š¹āāØš¦, š¶ā©) ā š))) |
38 | 34, 36, 10, 37 | syl3anc 1372 |
. . . . . . . . . . 11
ā¢ (š ā (āØš¦, š¶ā© ā (š¹ supp š) ā (āØš¦, š¶ā© ā (š“ Ć šµ) ā§ (š¹āāØš¦, š¶ā©) ā š))) |
39 | 38 | ad2antrr 725 |
. . . . . . . . . 10
ā¢ (((š ā§ š¦ ā š“) ā§ Ā¬ (šŗāš¦) = š) ā (āØš¦, š¶ā© ā (š¹ supp š) ā (āØš¦, š¶ā© ā (š“ Ć šµ) ā§ (š¹āāØš¦, š¶ā©) ā š))) |
40 | 26, 33, 39 | mpbir2and 712 |
. . . . . . . . 9
ā¢ (((š ā§ š¦ ā š“) ā§ Ā¬ (šŗāš¦) = š) ā āØš¦, š¶ā© ā (š¹ supp š)) |
41 | | simpr 486 |
. . . . . . . . . . 11
ā¢ ((((š ā§ š¦ ā š“) ā§ Ā¬ (šŗāš¦) = š) ā§ š§ = āØš¦, š¶ā©) ā š§ = āØš¦, š¶ā©) |
42 | 41 | fveq2d 6847 |
. . . . . . . . . 10
ā¢ ((((š ā§ š¦ ā š“) ā§ Ā¬ (šŗāš¦) = š) ā§ š§ = āØš¦, š¶ā©) ā ((1st ā¾ (V
Ć V))āš§) =
((1st ā¾ (V Ć V))āāØš¦, š¶ā©)) |
43 | | xpss 5650 |
. . . . . . . . . . . 12
ā¢ (š“ Ć šµ) ā (V Ć V) |
44 | 26 | adantr 482 |
. . . . . . . . . . . 12
ā¢ ((((š ā§ š¦ ā š“) ā§ Ā¬ (šŗāš¦) = š) ā§ š§ = āØš¦, š¶ā©) ā āØš¦, š¶ā© ā (š“ Ć šµ)) |
45 | 43, 44 | sselid 3943 |
. . . . . . . . . . 11
ā¢ ((((š ā§ š¦ ā š“) ā§ Ā¬ (šŗāš¦) = š) ā§ š§ = āØš¦, š¶ā©) ā āØš¦, š¶ā© ā (V Ć
V)) |
46 | 45 | fvresd 6863 |
. . . . . . . . . 10
ā¢ ((((š ā§ š¦ ā š“) ā§ Ā¬ (šŗāš¦) = š) ā§ š§ = āØš¦, š¶ā©) ā ((1st ā¾ (V
Ć V))āāØš¦,
š¶ā©) = (1st
āāØš¦, š¶ā©)) |
47 | 23 | adantr 482 |
. . . . . . . . . . 11
ā¢ ((((š ā§ š¦ ā š“) ā§ Ā¬ (šŗāš¦) = š) ā§ š§ = āØš¦, š¶ā©) ā š¦ ā š“) |
48 | 25 | adantr 482 |
. . . . . . . . . . 11
ā¢ ((((š ā§ š¦ ā š“) ā§ Ā¬ (šŗāš¦) = š) ā§ š§ = āØš¦, š¶ā©) ā š¶ ā šµ) |
49 | | op1stg 7934 |
. . . . . . . . . . 11
ā¢ ((š¦ ā š“ ā§ š¶ ā šµ) ā (1st āāØš¦, š¶ā©) = š¦) |
50 | 47, 48, 49 | syl2anc 585 |
. . . . . . . . . 10
ā¢ ((((š ā§ š¦ ā š“) ā§ Ā¬ (šŗāš¦) = š) ā§ š§ = āØš¦, š¶ā©) ā (1st
āāØš¦, š¶ā©) = š¦) |
51 | 42, 46, 50 | 3eqtrd 2777 |
. . . . . . . . 9
ā¢ ((((š ā§ š¦ ā š“) ā§ Ā¬ (šŗāš¦) = š) ā§ š§ = āØš¦, š¶ā©) ā ((1st ā¾ (V
Ć V))āš§) =
š¦) |
52 | 40, 51 | rspcedeq1vd 3585 |
. . . . . . . 8
ā¢ (((š ā§ š¦ ā š“) ā§ Ā¬ (šŗāš¦) = š) ā āš§ ā (š¹ supp š)((1st ā¾ (V Ć
V))āš§) = š¦) |
53 | | fofn 6759 |
. . . . . . . . . . . . 13
ā¢
(1st :VāontoāV ā 1st Fn V) |
54 | | fnresin 31586 |
. . . . . . . . . . . . 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 3969 |
. . . . . . . . . . . . . 14
ā¢ (V
Ć V) ā V |
57 | | sseqin2 4176 |
. . . . . . . . . . . . . 14
ā¢ ((V
Ć V) ā V ā (V ā© (V Ć V)) = (V Ć
V)) |
58 | 56, 57 | mpbi 229 |
. . . . . . . . . . . . 13
ā¢ (V ā©
(V Ć V)) = (V Ć V) |
59 | 58 | fneq2i 6601 |
. . . . . . . . . . . 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 8109 |
. . . . . . . . . . . 12
ā¢ (š¹ supp š) ā dom š¹ |
63 | 34 | fndmd 6608 |
. . . . . . . . . . . 12
ā¢ (š ā dom š¹ = (š“ Ć šµ)) |
64 | 62, 63 | sseqtrid 3997 |
. . . . . . . . . . 11
ā¢ (š ā (š¹ supp š) ā (š“ Ć šµ)) |
65 | 64, 43 | sstrdi 3957 |
. . . . . . . . . 10
ā¢ (š ā (š¹ supp š) ā (V Ć V)) |
66 | 61, 65 | fvelimabd 6916 |
. . . . . . . . 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 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 8126 |
. 2
ā¢ (š ā (šŗ supp š) ā ((1st ā¾ (V
Ć V)) ā (š¹ supp
š))) |
74 | | suppssfifsupp 9325 |
. 2
ā¢ (((šŗ ā V ā§ Fun šŗ ā§ š ā š) ā§ (((1st ā¾ (V Ć
V)) ā (š¹ supp š)) ā Fin ā§ (šŗ supp š) ā ((1st ā¾ (V
Ć V)) ā (š¹ supp
š)))) ā šŗ finSupp š) |
75 | 7, 9, 10, 19, 73, 74 | syl32anc 1379 |
1
ā¢ (š ā šŗ finSupp š) |