Step | Hyp | Ref
| Expression |
1 | | fsuppcurry1.g |
. . . 4
ā¢ šŗ = (š„ ā šµ ā¦ (š¶š¹š„)) |
2 | | oveq2 7401 |
. . . . 5
ā¢ (š„ = š¦ ā (š¶š¹š„) = (š¶š¹š¦)) |
3 | 2 | cbvmptv 5254 |
. . . 4
ā¢ (š„ ā šµ ā¦ (š¶š¹š„)) = (š¦ ā šµ ā¦ (š¶š¹š¦)) |
4 | 1, 3 | eqtri 2759 |
. . 3
ā¢ šŗ = (š¦ ā šµ ā¦ (š¶š¹š¦)) |
5 | | fsuppcurry1.b |
. . . 4
ā¢ (š ā šµ ā š) |
6 | 5 | mptexd 7210 |
. . 3
ā¢ (š ā (š¦ ā šµ ā¦ (š¶š¹š¦)) ā V) |
7 | 4, 6 | eqeltrid 2836 |
. 2
ā¢ (š ā šŗ ā V) |
8 | 1 | funmpt2 6576 |
. . 3
ā¢ Fun šŗ |
9 | 8 | a1i 11 |
. 2
ā¢ (š ā Fun šŗ) |
10 | | fsuppcurry1.z |
. 2
ā¢ (š ā š ā š) |
11 | | fo2nd 7978 |
. . . . 5
ā¢
2nd :VāontoāV |
12 | | fofun 6793 |
. . . . 5
ā¢
(2nd :VāontoāV ā Fun 2nd ) |
13 | 11, 12 | ax-mp 5 |
. . . 4
ā¢ Fun
2nd |
14 | | funres 6579 |
. . . 4
ā¢ (Fun
2nd ā Fun (2nd ā¾ (V Ć
V))) |
15 | 13, 14 | mp1i 13 |
. . 3
ā¢ (š ā Fun (2nd
ā¾ (V Ć V))) |
16 | | fsuppcurry1.1 |
. . . 4
ā¢ (š ā š¹ finSupp š) |
17 | 16 | fsuppimpd 9352 |
. . 3
ā¢ (š ā (š¹ supp š) ā Fin) |
18 | | imafi 9158 |
. . 3
ā¢ ((Fun
(2nd ā¾ (V Ć V)) ā§ (š¹ supp š) ā Fin) ā ((2nd
ā¾ (V Ć V)) ā (š¹ supp š)) ā Fin) |
19 | 15, 17, 18 | syl2anc 584 |
. 2
ā¢ (š ā ((2nd ā¾
(V Ć V)) ā (š¹
supp š)) ā
Fin) |
20 | | ovexd 7428 |
. . . 4
ā¢ ((š ā§ š¦ ā šµ) ā (š¶š¹š¦) ā V) |
21 | 20, 4 | fmptd 7098 |
. . 3
ā¢ (š ā šŗ:šµā¶V) |
22 | | eldif 3954 |
. . . 4
ā¢ (š¦ ā (šµ ā ((2nd ā¾ (V Ć
V)) ā (š¹ supp š))) ā (š¦ ā šµ ā§ Ā¬ š¦ ā ((2nd ā¾ (V Ć
V)) ā (š¹ supp š)))) |
23 | | fsuppcurry1.c |
. . . . . . . . . . . 12
ā¢ (š ā š¶ ā š“) |
24 | 23 | ad2antrr 724 |
. . . . . . . . . . 11
ā¢ (((š ā§ š¦ ā šµ) ā§ Ā¬ (šŗāš¦) = š) ā š¶ ā š“) |
25 | | simplr 767 |
. . . . . . . . . . 11
ā¢ (((š ā§ š¦ ā šµ) ā§ Ā¬ (šŗāš¦) = š) ā š¦ ā šµ) |
26 | 24, 25 | opelxpd 5707 |
. . . . . . . . . 10
ā¢ (((š ā§ š¦ ā šµ) ā§ Ā¬ (šŗāš¦) = š) ā āØš¶, š¦ā© ā (š“ Ć šµ)) |
27 | | df-ov 7396 |
. . . . . . . . . . 11
ā¢ (š¶š¹š¦) = (š¹āāØš¶, š¦ā©) |
28 | | ovexd 7428 |
. . . . . . . . . . . . 13
ā¢ (((š ā§ š¦ ā šµ) ā§ Ā¬ (šŗāš¦) = š) ā (š¶š¹š¦) ā V) |
29 | 1, 2, 25, 28 | fvmptd3 7007 |
. . . . . . . . . . . 12
ā¢ (((š ā§ š¦ ā šµ) ā§ Ā¬ (šŗāš¦) = š) ā (šŗāš¦) = (š¶š¹š¦)) |
30 | | simpr 485 |
. . . . . . . . . . . . 13
ā¢ (((š ā§ š¦ ā šµ) ā§ Ā¬ (šŗāš¦) = š) ā Ā¬ (šŗāš¦) = š) |
31 | 30 | neqned 2946 |
. . . . . . . . . . . 12
ā¢ (((š ā§ š¦ ā šµ) ā§ Ā¬ (šŗāš¦) = š) ā (šŗāš¦) ā š) |
32 | 29, 31 | eqnetrrd 3008 |
. . . . . . . . . . 11
ā¢ (((š ā§ š¦ ā šµ) ā§ Ā¬ (šŗāš¦) = š) ā (š¶š¹š¦) ā š) |
33 | 27, 32 | eqnetrrid 3015 |
. . . . . . . . . 10
ā¢ (((š ā§ š¦ ā šµ) ā§ Ā¬ (šŗāš¦) = š) ā (š¹āāØš¶, š¦ā©) ā š) |
34 | | fsuppcurry1.f |
. . . . . . . . . . . 12
ā¢ (š ā š¹ Fn (š“ Ć šµ)) |
35 | | fsuppcurry1.a |
. . . . . . . . . . . . 13
ā¢ (š ā š“ ā š) |
36 | 35, 5 | xpexd 7721 |
. . . . . . . . . . . 12
ā¢ (š ā (š“ Ć šµ) ā V) |
37 | | elsuppfn 8138 |
. . . . . . . . . . . 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 485 |
. . . . . . . . . . 11
ā¢ ((((š ā§ š¦ ā šµ) ā§ Ā¬ (šŗāš¦) = š) ā§ š§ = āØš¶, š¦ā©) ā š§ = āØš¶, š¦ā©) |
42 | 41 | fveq2d 6882 |
. . . . . . . . . 10
ā¢ ((((š ā§ š¦ ā šµ) ā§ Ā¬ (šŗāš¦) = š) ā§ š§ = āØš¶, š¦ā©) ā ((2nd ā¾ (V
Ć V))āš§) =
((2nd ā¾ (V Ć V))āāØš¶, š¦ā©)) |
43 | | xpss 5685 |
. . . . . . . . . . . 12
ā¢ (š“ Ć šµ) ā (V Ć V) |
44 | 26 | adantr 481 |
. . . . . . . . . . . 12
ā¢ ((((š ā§ š¦ ā šµ) ā§ Ā¬ (šŗāš¦) = š) ā§ š§ = āØš¶, š¦ā©) ā āØš¶, š¦ā© ā (š“ Ć šµ)) |
45 | 43, 44 | sselid 3976 |
. . . . . . . . . . 11
ā¢ ((((š ā§ š¦ ā šµ) ā§ Ā¬ (šŗāš¦) = š) ā§ š§ = āØš¶, š¦ā©) ā āØš¶, š¦ā© ā (V Ć V)) |
46 | 45 | fvresd 6898 |
. . . . . . . . . 10
ā¢ ((((š ā§ š¦ ā šµ) ā§ Ā¬ (šŗāš¦) = š) ā§ š§ = āØš¶, š¦ā©) ā ((2nd ā¾ (V
Ć V))āāØš¶,
š¦ā©) = (2nd
āāØš¶, š¦ā©)) |
47 | 24 | adantr 481 |
. . . . . . . . . . 11
ā¢ ((((š ā§ š¦ ā šµ) ā§ Ā¬ (šŗāš¦) = š) ā§ š§ = āØš¶, š¦ā©) ā š¶ ā š“) |
48 | 25 | adantr 481 |
. . . . . . . . . . 11
ā¢ ((((š ā§ š¦ ā šµ) ā§ Ā¬ (šŗāš¦) = š) ā§ š§ = āØš¶, š¦ā©) ā š¦ ā šµ) |
49 | | op2ndg 7970 |
. . . . . . . . . . 11
ā¢ ((š¶ ā š“ ā§ š¦ ā šµ) ā (2nd āāØš¶, š¦ā©) = š¦) |
50 | 47, 48, 49 | syl2anc 584 |
. . . . . . . . . 10
ā¢ ((((š ā§ š¦ ā šµ) ā§ Ā¬ (šŗāš¦) = š) ā§ š§ = āØš¶, š¦ā©) ā (2nd
āāØš¶, š¦ā©) = š¦) |
51 | 42, 46, 50 | 3eqtrd 2775 |
. . . . . . . . 9
ā¢ ((((š ā§ š¦ ā šµ) ā§ Ā¬ (šŗāš¦) = š) ā§ š§ = āØš¶, š¦ā©) ā ((2nd ā¾ (V
Ć V))āš§) =
š¦) |
52 | 40, 51 | rspcedeq1vd 3614 |
. . . . . . . 8
ā¢ (((š ā§ š¦ ā šµ) ā§ Ā¬ (šŗāš¦) = š) ā āš§ ā (š¹ supp š)((2nd ā¾ (V Ć
V))āš§) = š¦) |
53 | | fofn 6794 |
. . . . . . . . . . . . 13
ā¢
(2nd :VāontoāV ā 2nd Fn V) |
54 | | fnresin 31718 |
. . . . . . . . . . . . 13
ā¢
(2nd Fn V ā (2nd ā¾ (V Ć V)) Fn (V
ā© (V Ć V))) |
55 | 11, 53, 54 | mp2b 10 |
. . . . . . . . . . . 12
ā¢
(2nd ā¾ (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 6636 |
. . . . . . . . . . . 12
ā¢
((2nd ā¾ (V Ć V)) Fn (V ā© (V Ć V))
ā (2nd ā¾ (V Ć V)) Fn (V Ć
V)) |
60 | 55, 59 | mpbi 229 |
. . . . . . . . . . 11
ā¢
(2nd ā¾ (V Ć V)) Fn (V Ć V) |
61 | 60 | a1i 11 |
. . . . . . . . . 10
ā¢ (š ā (2nd ā¾ (V
Ć V)) Fn (V Ć V)) |
62 | | suppssdm 8144 |
. . . . . . . . . . . 12
ā¢ (š¹ supp š) ā dom š¹ |
63 | 34 | fndmd 6643 |
. . . . . . . . . . . 12
ā¢ (š ā dom š¹ = (š“ Ć šµ)) |
64 | 62, 63 | sseqtrid 4030 |
. . . . . . . . . . 11
ā¢ (š ā (š¹ supp š) ā (š“ Ć šµ)) |
65 | 64, 43 | sstrdi 3990 |
. . . . . . . . . 10
ā¢ (š ā (š¹ supp š) ā (V Ć V)) |
66 | 61, 65 | fvelimabd 6951 |
. . . . . . . . 9
ā¢ (š ā (š¦ ā ((2nd ā¾ (V Ć
V)) ā (š¹ supp š)) ā āš§ ā (š¹ supp š)((2nd ā¾ (V Ć
V))āš§) = š¦)) |
67 | 66 | ad2antrr 724 |
. . . . . . . 8
ā¢ (((š ā§ š¦ ā šµ) ā§ Ā¬ (šŗāš¦) = š) ā (š¦ ā ((2nd ā¾ (V Ć
V)) ā (š¹ supp š)) ā āš§ ā (š¹ supp š)((2nd ā¾ (V Ć
V))āš§) = š¦)) |
68 | 52, 67 | mpbird 256 |
. . . . . . 7
ā¢ (((š ā§ š¦ ā šµ) ā§ Ā¬ (šŗāš¦) = š) ā š¦ ā ((2nd ā¾ (V Ć
V)) ā (š¹ supp š))) |
69 | 68 | ex 413 |
. . . . . 6
ā¢ ((š ā§ š¦ ā šµ) ā (Ā¬ (šŗāš¦) = š ā š¦ ā ((2nd ā¾ (V Ć
V)) ā (š¹ supp š)))) |
70 | 69 | con1d 145 |
. . . . 5
ā¢ ((š ā§ š¦ ā šµ) ā (Ā¬ š¦ ā ((2nd ā¾ (V Ć
V)) ā (š¹ supp š)) ā (šŗāš¦) = š)) |
71 | 70 | impr 455 |
. . . 4
ā¢ ((š ā§ (š¦ ā šµ ā§ Ā¬ š¦ ā ((2nd ā¾ (V Ć
V)) ā (š¹ supp š)))) ā (šŗāš¦) = š) |
72 | 22, 71 | sylan2b 594 |
. . 3
ā¢ ((š ā§ š¦ ā (šµ ā ((2nd ā¾ (V Ć
V)) ā (š¹ supp š)))) ā (šŗāš¦) = š) |
73 | 21, 72 | suppss 8161 |
. 2
ā¢ (š ā (šŗ supp š) ā ((2nd ā¾ (V
Ć V)) ā (š¹ supp
š))) |
74 | | suppssfifsupp 9361 |
. 2
ā¢ (((šŗ ā V ā§ Fun šŗ ā§ š ā š) ā§ (((2nd ā¾ (V Ć
V)) ā (š¹ supp š)) ā Fin ā§ (šŗ supp š) ā ((2nd ā¾ (V
Ć V)) ā (š¹ supp
š)))) ā šŗ finSupp š) |
75 | 7, 9, 10, 19, 73, 74 | syl32anc 1378 |
1
ā¢ (š ā šŗ finSupp š) |